- weakTypeToTypeOfKind φ' te ★ >>= fun τ' =>
- weakExprToStrongExpr _ (weakCE Δ) φ'
- (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) ig _ (weakL lev) e
- >>= fun e' => castExpr we "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e')
+ weakTypeToTypeOfKind φ2 te ★ >>= fun τ' =>
+ weakExprToStrongExpr _ (weakCE_(n:=O) Δ) φ2
+ (fun x => (ψ x) >>= fun y =>
+ OK (weakCV_ y)) (weakLT_○ξ) ig _ (weakL_ lev) e
+ >>= fun e' => castExpr we "WETyLam2" _ _
+ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev 0 e')