| ETyApp : ∀ Γ Δ κ σ τ ξ l, Expr Γ Δ ξ (HaskTAll κ σ) l -> Expr Γ Δ ξ (substT σ τ) l
| ECoLam : forall Γ Δ κ σ (σ₁ σ₂:HaskType Γ κ) ξ l, Expr Γ (σ₁∼∼∼σ₂::Δ) ξ σ l -> Expr Γ Δ ξ (σ₁∼∼σ₂ ⇒ σ) l
| ECoApp : forall Γ Δ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ ξ l, Expr Γ Δ ξ (σ₁ ∼∼ σ₂ ⇒ σ) l -> Expr Γ Δ ξ σ l
| ETyApp : ∀ Γ Δ κ σ τ ξ l, Expr Γ Δ ξ (HaskTAll κ σ) l -> Expr Γ Δ ξ (substT σ τ) l
| ECoLam : forall Γ Δ κ σ (σ₁ σ₂:HaskType Γ κ) ξ l, Expr Γ (σ₁∼∼∼σ₂::Δ) ξ σ l -> Expr Γ Δ ξ (σ₁∼∼σ₂ ⇒ σ) l
| ECoApp : forall Γ Δ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ ξ l, Expr Γ Δ ξ (σ₁ ∼∼ σ₂ ⇒ σ) l -> Expr Γ Δ ξ σ l