PrintForm Definitions grammar 1 Sections AutomataTheory Doc

At: void union lang

V,T:Type, L:LangOver(V+T). L LangOver(Void+T)
By:
Unfold `languages` 0
THEN
UnivCD
Generated subgoal:

11. V: Type
2. T: Type
3. L: (V+T)*Prop
L (Void+T)*Prop

About:
alluniverseunionmembervoidfunctionlistprop