| WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
| WELet v ve ebody => weakTypeToTypeOfKind φ v ★ >>= fun tv =>
| WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
| WELet v ve ebody => weakTypeToTypeOfKind φ v ★ >>= fun tv =>