One-way liveness in Mathlib's NFA model

The relation-product language is exactly the language of the ordinary h-state NFA whose transitions are the relations in the input. This connects the imported lower bound to Mathlib's one-way automata and regular languages.

theorem Complexity.FiniteAutomaton.livenessNFA_evalFrom (h : ℕ) (w : List (Alphabet h)) (S : Set (Fin h)) (q : Fin h) : q ∈ (livenessNFA h).evalFrom S w ↔ ∃ p ∈ S, w.prod.holds p q

theorem Complexity.FiniteAutomaton.livenessNFA_accepts_proof (h : ℕ) : (livenessNFA h).accepts = oneWayLiveness h