| WECast e co => let (t1,t2) := weakCoercionTypes co in
weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
weakExprToStrongExpr Γ Δ φ ψ ξ ig t1' lev e >>= fun e' =>
| WECast e co => let (t1,t2) := weakCoercionTypes co in
weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
weakExprToStrongExpr Γ Δ φ ψ ξ ig t1' lev e >>= fun e' =>