Theorem: RegularProduction.lhs_eq_production_lhs (FormalSystems/Chomsky/Regular/RegularGrammar.lean)

State before:
α✝¹ : Type
Z : Finset α✝¹
α✝ : Type
V : Finset α✝
p : RegularProduction Z V
⊢ Production.lhs p = [Sum.inl (lhs p)]
Tactic:
rfl
State after:
no goals