Who Cites union-deq?
union-deq	Def union-deq(A;B;a;b) == <sumdeq(a;b),sum-deq(A;B;a;b)>
sum-deq	Def sum-deq(A;B;a;b) Def == (A,B,a,b,p,q. Def == (InjCase(q; x. InjCase(p Def == (InjCase(q; x. InjCase; x1. b/eq,b1. Def == (InjCase(q; x. InjCase; x1. a/e1,a1. Def == (InjCase(q; x. InjCase; x1. <%.(%1.%1(x1,x)/%4,%5. Def == (InjCase(q; x. InjCase; x1. <%.(%4 Def == (InjCase(q; x. InjCase; x1. <%.(((%1.%1) Def == (InjCase(q; x. InjCase; x1. <%.((((%1.*) Def == (InjCase(q; x. InjCase; x1. <%.(((((%1.%1(x)) Def == (InjCase(q; x. InjCase; x1. <%.((((((%1.%1(x1)) Def == (InjCase(q; x. InjCase; x1. <%.(((((((%1.%1(B)) Def == (InjCase(q; x. InjCase; x1. <%.((((((((%1.%1(A)) Def == (InjCase(q; x. InjCase; x1. <%.((((((((A,B,x1,x,%. (%1.%1) Def == (InjCase(q; x. InjCase; x1. <%.((((((((A,B,x1,x,%. ((%1.(%2.*)(*)) Def == (InjCase(q; x. InjCase; x1. <%.((((((((A,B,x1,x,%. ((%)))))))))) Def == (InjCase(q; x. InjCase; x1. <%.(a1) Def == (InjCase(q; x. InjCase; x1. ,%.*> Def == (InjCase(q; x. InjCase; y. b/eq,b1. Def == (InjCase(q; x. InjCase; y. a/e1,a1. Def == (InjCase(q; x. InjCase; y. <%.(%1.any((%1(*)))) Def == (InjCase(q; x. InjCase; y. <%.((%1.%1(x)) Def == (InjCase(q; x. InjCase; y. <%.(((%1.%1(y)) Def == (InjCase(q; x. InjCase; y. <%.((((%1.%1(B)) Def == (InjCase(q; x. InjCase; y. <%.(((((%1.%1(A)) Def == (InjCase(q; x. InjCase; y. <%.(((((A,B,y,x,%. Def == (InjCase(q; x. InjCase; y. <%.((((((%1. Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase(%1 Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %2. any(%2) Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %3. (%4.any(%4)) Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %3. ((%4.(%5.(%6. Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %3. ((%4.(%5.(any(%6)) Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %3. ((%4.(%5.(*)) Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %3. ((%4.(*)) Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %3. ((%)))) Def == (InjCase(q; x. InjCase; y. <%.(((((((%1.%1)(inr(%.*)))))))) Def == (InjCase(q; x. InjCase; y. ,%.*>) Def == (; y. Def == (InjCase(p Def == (InjCase; x. b/eq,b1. Def == (InjCase; x. a/e1,a1. Def == (InjCase; x. <%.(%1.any((%1(*)))) Def == (InjCase; x. <%.((%1.%1(y)) Def == (InjCase; x. <%.(((%1.%1(x)) Def == (InjCase; x. <%.((((%1.%1(B)) Def == (InjCase; x. <%.(((((%1.%1(A)) Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase(%1 Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %2. any(%2) Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. (%4.any(%4)) Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. ((%4.(%5.(%6. Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. ((%4.(%5.(any(%6)) Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. ((%4.(%5.(*)) Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. ((%4.(*)) Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. ((%)))) Def == (InjCase; x. <%.(((((A,B,x,y,%. ((%1.%1)(inr(%.*)))))))) Def == (InjCase; x. ,%.*> Def == (InjCase; y1. b/eq,b1. Def == (InjCase; y1. a/e1,a1. Def == (InjCase; y1. <%.(%1.%1(y1,y)/%4,%5. Def == (InjCase; y1. <%.(%4 Def == (InjCase; y1. <%.(((%1.%1) Def == (InjCase; y1. <%.((((%1.*) Def == (InjCase; y1. <%.(((((%1.%1(y)) Def == (InjCase; y1. <%.((((((%1.%1(y1)) Def == (InjCase; y1. <%.(((((((%1.%1(B)) Def == (InjCase; y1. <%.((((((((%1.%1(A)) Def == (InjCase; y1. <%.((((((((A,B,y1,y,%. (%1.%1) Def == (InjCase; y1. <%.((((((((A,B,y1,y,%. ((%1.(%2.*)(*))(%)))))))))) Def == (InjCase; y1. <%.(b1) Def == (InjCase; y1. ,%.*>))) Def == (A Def == ,B Def == ,a Def == ,b)
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:

union-deq(A;B;a;b)

has structure:

union-deq(A; B; a; b)

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