PrintForm
grammar
1
Sections
AutomataTheory
Doc
At:
void
union
lang
1
1.
V:
Type
2.
T:
Type
3.
L:
(V+T)*
Prop
L
(Void+T)*
Prop
By:
FunExtensionality
Generated subgoal:
1
4.
x:
(Void+T)*
L(x)
Prop
About:
L(x) 
Prop
Prop L (Void+T)*Prop L(x) Prop
