1. E : Type
2. y1 : Tree(E)
3. y2 : Tree(E)
  inr(<y1,y2>) = inr(<y1,y2>)  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}]

1	y1 = y1  rec(T.E+(TT))	1 step
2	y2 = y2  rec(T.E+(TT))	1 step

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