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''
