1. E : Type
2. x1 : E
  inl(x1) = inl(x1)  rec(T.E+(TT))

By:	Refine RULE H   a1 = a2  rec(z.t) RULE H BY rec_memberEquality level{i} RULE H H  a1 = a2  t[rec(z.t)/z] RULE H H  rec(z.t) = rec(z.t)  Type{i} [mk_le_term_arg level{i}]

None

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