cases p <;> rfl
α✝¹ : Type
Z : Finset α✝¹
α✝ : Type
V : Finset α✝
p : RegularProduction Z V
⊢ Production.rhs p = Word.mk (Sum.inr <$> Option.toList (getRhs p).1) * Word.mk (Sum.inl <$> Option.toList (getRhs p).2)
no goals