true ? 0; 1
     : nat
if true as x return (x ? nat; bool) then 0 else true
     : true ? nat; bool
Defining 'proj1' as keyword
fun e : nat * nat => proj1 e
     : nat * nat -> nat
Defining 'decomp' as keyword
decomp (true, true) as t, u in (t, u)
     : bool * bool
!(0 = 0)
     : Prop
forall n : nat, n = 0
     : Prop
!(0 = 0)
     : Prop
forall n : nat, #(n = n)
     : Prop
forall n n0 : nat, ##(n = n0)
     : Prop
forall n n0 : nat, ###(n = n0)
     : Prop
3 + 3
     : Z
3 + 3
     : znat
[1; 2; 4]
     : list nat
(1; 2, 4)
     : nat * nat * nat
Defining 'ifzero' as keyword
ifzero 3
     : bool
Defining 'pred' as keyword
pred 3
     : nat
fun n : nat => pred n
     : nat -> nat
fun n : nat => pred n
     : nat -> nat
Defining 'ifn' as keyword
Defining 'is' as keyword
fun x : nat => ifn x is succ n then n else 0
     : nat -> nat
1-
     : bool
-4
     : Z
Nil
     : forall A : Type, list A
NIL:list nat
     : list nat