At: g eq wf 1 2
1. V1: Type
2. V2: Type
3. T: Type
4. G1: Grammar(V1;T)
5. G2: Grammar(V2;T)
6. l: (Void+T)*
((
l.[S] 
l)(l) 
(l.[S] l)(l)) 
Prop
By:
Reduce 0
THEN
Inst
Thm* 
l:(Void+T)*. l (V+T)*
[V1;T;l]
THEN
Inst
Thm* l:(Void+T)*. l (V+T)*
[V2;T;l]
Generated subgoals:None
About:
