Inductive nat : Type :=
| O: nat
| S: nat -> nat.

Inductive bool : Type :=
| true: bool
| false: bool.

Recursive eqnat (x:nat) (y:nat) [0] : _ :=
  match x with
    | (match y with
         | true
 	 | \y. false
      )
    | \x. match y with
      	    | false
	    | \y. eqnat x y
.

Inductive term : Type -> Type :=
| Encap: V (A: Type). A -> term A
| App: V (A: Type). V (B: Type). term (A -> B) -> term A -> term B
| Ifte: V (A: Type). term bool -> term A -> term A -> term A.

Implicite Encap [1].
Implicite App [2].
Implicite Ifte [1].


Recursive execterm A (t: term A) [1] : _ :=
   match t with
     | \A0. \x. x
     | \A0. \B. \tab. \ta. (execterm _ tab) (execterm _ ta)
     | \A0. \tb. \t1. \t2. 
                match (execterm _ tb) with
                  | execterm _ t1
                  | execterm _ t2
.

Implicite execterm [1].

Typecheck (Encap O).

Typecheck (App (Encap eqnat) (Encap O)).

Typecheck (App (App (Encap eqnat) (Encap O)) (Encap O)).

Definition t := (Ifte (App (App (Encap eqnat) (Encap O)) (Encap O)) (Encap O) (Encap (S O))).

Typecheck t.

Simpl t.

Simpl (execterm t).

Show Definitions.