- | ECast Γ Δ ξ t1 t2 γ l e => fun ite => WECast (strongExprToWeakExpr ftv fcv fev e ite) (coercionToWeakCoercion _ _ _ _ _ γ)
- | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => fun ite => WECoApp (strongExprToWeakExpr ftv fcv fev e ite) (coercionToWeakCoercion _ _ _ _ _ γ)
+ | ECast Γ Δ ξ t1 t2 γ l e => fun ite => WECast (strongExprToWeakExpr ftv fcv fev e ite)
+ (coercionToWeakCoercion _ _ _ _ _ ftv ite γ)
+ | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => fun ite => WECoApp (strongExprToWeakExpr ftv fcv fev e ite)
+ (coercionToWeakCoercion _ _ _ _ _ ftv ite γ)