| EVar : ∀ Γ Δ ξ ev, Expr Γ Δ ξ (ξ ev)
| ELit : ∀ Γ Δ ξ lit l, Expr Γ Δ ξ (literalType lit@@l)
| EApp : ∀ Γ Δ ξ t1 t2 l, Expr Γ Δ ξ (t2--->t1 @@ l) -> Expr Γ Δ ξ (t2 @@ l) -> Expr Γ Δ ξ (t1 @@ l)
| EVar : ∀ Γ Δ ξ ev, Expr Γ Δ ξ (ξ ev)
| ELit : ∀ Γ Δ ξ lit l, Expr Γ Δ ξ (literalType lit@@l)
| EApp : ∀ Γ Δ ξ t1 t2 l, Expr Γ Δ ξ (t2--->t1 @@ l) -> Expr Γ Δ ξ (t2 @@ l) -> Expr Γ Δ ξ (t1 @@ l)