Nuprl - Proof: tree subtype2 1 2 1 1 1

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

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

y1 = y1

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