Def b2i(b) == if b 1 else 0 fi

Thm* b:. b2i(b)

Def AB == B < A

Thm* i,j:. ij Prop

Def == Unit+Unit

Thm* Type

Def if b t else f fi == dec(b ; t; f)

Thm* b:, A:Type, p,q:A. if b p else q fi A

Def A == A False

Thm* (A) Prop