Bool : Type
True : Bool
False : Bool

CBool : Type
CBool = (t: Type) t -> t -> t

CBool.to_bool (x : CBool) : Bool
CBool.to_bool x = (x Bool True False)

CTrue : CBool
CTrue = @p @t @f t

CFalse : CBool
CFalse = @p @t @f f

And (a: CBool) (b: CBool) : CBool
And a b = @p @t @f (a p (b p t f) f)

CNat : Type
CNat = (n: Type) (n -> n) -> n -> n

Add (a: CNat) (b: CNat) : CNat
Add a b = @n @s @z (a n s (b n s z))

CMul (a: CNat) (b: CNat) : CNat
CMul a b = @n @s (a n (b n s))

Suc (a: CNat) : CNat
Suc a = @n @s @z (s (a n s z))

CEqual (t: Type) (a: t) (b: t) : Type
CEqual t a b = (p: t -> Type) (p a) -> (p b)

CRefl (t: Type) (x: t) : (CEqual t x x)
CRefl t x = @p @px px

N0 : CNat
N0 = @n @s @z z

N2 : CNat
N2 = @n @s @z (s (s z))

N3 : CNat
N3 = @n @s @z (s (s (s z)))

N4 : CNat
N4 = @n @s @z (s (s (s (s z))))

N5 : CNat
N5 = @n @s @z (s (s (s (s (s z)))))

N10 : CNat
N10 = (CMul N2 N5)

N10b : CNat
N10b = (CMul N5 N2)

N15 : CNat
N15 = (Add N10 N5)

N15b : CNat
N15b = (Add N10b N5)

N18 : CNat
N18 = (Add N15 N3)

N18b : CNat
N18b = (Add N15b N3)

N19 : CNat
N19 = (Add N15 N4)

N19b : CNat
N19b = (Add N15b N4)

N20 : CNat
N20 = (CMul N2 N10)

N20b : CNat
N20b = (CMul N2 N10b)

N21 : CNat
N21 = (Suc N20)

N21b : CNat
N21b = (Suc N20b)

N22 : CNat
N22 = (Suc N21)

N22b : CNat
N22b = (Suc N21b)

N23 : CNat
N23 = (Suc N22)

N23b : CNat
N23b = (Suc N22b)

N100 : CNat
N100 = (CMul N10 N10)

N100b : CNat
N100b = (CMul N10b N10b)

N10k : CNat
N10k = (CMul N100 N100)

N10kb : CNat
N10kb = (CMul N100b N100b)

N100k : CNat
N100k = (CMul N10k N10)

N100kb : CNat
N100kb = (CMul N10kb N10b)

N1M : CNat
N1M = (CMul N10k N100)

N1Mb : CNat
N1Mb = (CMul N10kb N100b)

N5M : CNat
N5M = (CMul N1M N5)

N5Mb : CNat
N5Mb = (CMul N1Mb N5)

N10M : CNat
N10M = (CMul N5M N2)

N10Mb : CNat
N10Mb = (CMul N5Mb N2)

CTree : Type
CTree = (t: Type) (t -> t -> t) -> t -> t

CLeaf : CTree
CLeaf = @t @n @l l

CNode (t1: CTree) (t2: CTree) : CTree
CNode t1 t2 = @t @n @l (n (t1 t n l) (t2 t n l))

FullCTree (n: CNat) : CTree
FullCTree n = (n CTree @t(CNode t t) CLeaf)

Num : CNat
Num = N2

Force (n: CNat) : Bool
Force n = (n Bool @x(x) True)

Main : (CEqual CNat N1M N1Mb)
Main = (CRefl CNat N1M)