Nuprl - Proof: tree subtype2 1 2 1 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: tree subtype2 1 2 1 1 2

1. E : Type
2. Tree(E)
3. y2 : Tree(E)

y2 = y2

rec(T.E+(T

T))

By:	Fold `tree_con` 0 THEN Fold `tree` 0

Generated subgoals:

None

About:

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