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)

is mentioned

In prior sections: mb event system 2

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html