3 data Nat : * => { zero : Nat | suc : Nat -> Nat }
5 one : Nat => (suc zero)
7 three : Nat => (suc two)
10 data Tree : [A : *] -> * =>
11 { leaf : Tree A | node : Tree A -> A -> Tree A -> Tree A }
18 record Unit : * => tt { }
20 le [n : Nat] : Nat -> * => (
25 (\n f m => Nat-Elim m (\_ => *) Empty (\m' _ => f m'))
29 { bot : Lift | lift : Nat -> Lift | top : Lift }
31 le' [l1 : Lift] : Lift -> * => (
36 (\n1 l2 => Lift-Elim l2 (\_ => *) Empty (\n2 => le n1 n2) Unit)
37 (\l2 => Lift-Elim l2 (\_ => *) Empty (\_ => Empty) Unit)
40 data OList : [low : Lift] [upp : Lift] -> * =>
41 { nil : le' low upp -> OList low upp
42 | cons : [n : Nat] -> OList (lift n) upp -> le' low (lift n) -> OList low upp
47 record Prod : [A : *] [B : A -> *] -> * =>
48 prod {fst : A, snd : B fst}