Who Cites sumdeq?
sumdeq	Def sumdeq(a;b)(p,q) Def == InjCase(p; pa. InjCase(q; qa. 1of(a)(pa,qa); qb. false); pb. Def == InjCase(q; qa. false; qb. 1of(b)(pb,qb)))
	Thm* A,B:Type, a:EqDecider(A), b:EqDecider(B). sumdeq(a;b)  (A+B)(A+B)
pi1	Def 1of(t) == t.1
	Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p)  A

Syntax:

sumdeq(a;b)

has structure:

sumdeq(a; b)

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