3
== Unit+Unit+Unit
== inl(
)
== inr(inl())
== inr(inr()) 
case0; 3 case1; 3 case2; == InjCase(x; zero. case0; one_or_two. InjCase(one_or_two; one. case1; two. case2))
x:. True
3 = 3x,y:. Dec(x = y)| def | three | 3 == 3 |
| def | Three | == Unit+Unit+Unit |
| def | Three_0 | 3 == inl() |
| def | Three_1 | 3 == inr(inl()) |
| def | Three_2 | 3 == inr(inr()) |
| def | Three_case | case x: 3 case0; 3 case1; 3 case2; == InjCase(x; zero. case0; one_or_two. InjCase(one_or_two; one. case1; two. case2)) |
| THM | Three_ind_ext | x:. True |
| THM | Three_eq_contradiction_ext | 3 = 3 |
| THM | decidable__equal_Three | x,y:. Dec(x = y) |