+| ECast Γ Δ ξ t1 t2 γ l e => fun ite => FIXME
+(* WECast (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite)*)
+
+| ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => fun ite => FIXME
+(* WECoApp (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite)*)