1. E : Type
  rec(T.tree_con(E;T)) = rec(T.tree_con(E;T))

By:	Unfold `tree_con` 0 THEN Refine RULE H   rec(z1.t1) = rec(z2.t2)  Type{i} RULE H BY recEquality y RULE H BY Let ; = CallLisp(REC-EQUALITY) RULE H H, y:Type{i}  t1[y/z1] = t2[y/z2]  Type{i} [mk_var_arg `y']

None

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html