| ELam Γ' _ _ tv _ _ cv e => fun ite => bind tv' = typeToWeakType tv ite
; bind ev' = mkWeakExprVar tv'
; bind e' = exprToWeakExpr (update_χ χ cv ev') e ite
| ELam Γ' _ _ tv _ _ cv e => fun ite => bind tv' = typeToWeakType tv ite
; bind ev' = mkWeakExprVar tv'
; bind e' = exprToWeakExpr (update_χ χ cv ev') e ite