Who Cites Three case?
Three_case	Def case x: 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''

Syntax:

case x: 3 case0; 3 case1; 3 case2;

has structure:

Three_case(x; case2; case0; case1)

About: