At: assert st eq 1 1 1 1
1. s1: SimpleType
2. u: SimpleType
Type{i'}
3. w: s1:{v:SimpleType| u(v) }
s2:SimpleType. st_eq(s1;s2) 
s1 = s2
4. x3: Label
5. s2: SimpleType
6. u1: SimpleTypeType{i'}
7. w1: s2:{v:SimpleType| u1(v) }st_eq(tree_leaf(inl(x3));s2) tree_leaf(inl(x3)) = s2
8. x2: Label
9. x3 =
x2
x3 = x2
By:
EqLblFwd
THEN
HypSubst -1 0
Generated subgoals:None
About:
