+ weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' =>
+ castExpr we "ECase" (τ@@lev) (ECase Γ Δ ξ' lev tc tbranches' avars' escrut' tree)
+(*
+ weakExprToStrongExpr Γ Δ φ ψ ξ ig tscrut' lev escrut >>= fun escrut' =>
+ castExpr we "ECaseScrut" (caseType tc avars' @@ lev) (EVar Γ Δ ξ' vscrut) >>= fun evscrut' =>
+ castExpr we "ECase" (τ@@lev)
+ (ELet Γ Δ ξ tscrut' tbranches' lev (vscrut:CoreVar) escrut'
+ (ECase Γ Δ ξ' lev tc tbranches' avars' evscrut' tree))
+*)