Nuprl - Proof: sumdeq-property

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sumdeq-property

A,B:Type, a:EqDecider(A), b:EqDecider(B), p,q:A+B. p = q

sumdeq(a;b)(p,q)

By:	UnivCD THEN Unfold `sumdeq` 0 THEN Reduce 0 THEN Analyze 6 THEN Analyze 5 THEN Analyze 4 THEN Analyze 3 THEN Reduce 0 THEN Try (Analyze THEN BackThruSomeHyp THEN Trivial) THEN Try (BackThruSomeHyp THEN ObviousFrom [-1]) THEN Try (ObviousFrom [-1])

Generated subgoals:

None

About:

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