q == case p: 3
3
; 3
case q: 3 3; 3 3; 3 3;; 3 q;
Thm* 
p,q:
. p q 
== inr(inl(
))
Thm* 3
== inr(inr())
Thm* 3
case0; 3 case1; 3 case2;
== InjCase(x; zero. case0; one_or_two. InjCase(one_or_two; one. case1; two. case2))
Thm* t:Type{i}, t':Type{j}, t'':Type{k}, c:t, c':t', c'':t''.
case 3: 3 c; 3 c'; 3 c''; t
Thm* t:Type{i}, t':Type{j}, t'':Type{k}, c:t, c':t', c'':t''.
case 3: 3 c'; 3 c''; 3 c; t''
Thm* t:Type{i}, t':Type{j}, t'':Type{k}, c:t, c':t', c'':t''.
case 3: 3 c; 3 c'; 3 c''; t''
