weakTypeToType'' φ t1 ★ >>= fun t1' =>
weakTypeToType'' φ t2 ★ >>= fun t2' =>
weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' =>
weakTypeToType'' φ t1 ★ >>= fun t1' =>
weakTypeToType'' φ t2 ★ >>= fun t2' =>
weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' =>