PrintForm Definitions languages Sections AutomataTheory Doc

At: lang union wf 1 1 1 1

1. Alph: Type
2. M: Alph*Prop
3. N: LangOver(Alph)

(l.M(l) N(l)) Alph*Prop

By: Unfold `languages` 3

Generated subgoal:

13. N: Alph*Prop
(l.M(l) N(l)) Alph*Prop


About:
memberfunctionlistproplambdaorapplyuniverse