Def a' extends a == a'a = a

Thm* a,a':Assignment. a' extends a Type{i}

Def Assignment == Var

Thm* Assignment Type

Def == Unit+Unit+Unit

Thm* Type

Def a'a(x) == case (a(x)): 3 (a'(x)); 3 3; 3 (a'(x));

Thm* a',a:Assignment. a'a Assignment

Def 3 == inr(inl())

Thm* 3

Thm* Var Type

Def A == A False

Thm* A:Prop. (A) Prop

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