a(x) == case (a(x)): 3
(a'(x)); 3
3; 3
(a'(x));
Thm* 
a',a:Assignment. a'a 
Assignment
== inr(inl(
))
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''
