Theorem: Lean4Lean.VEnv.IsDefEqCtx.closed (Lean4Lean/Theory/Typing/Lemmas.lean)

State before:
env : VEnv
henv : Ordered env
Γ₀ : List VExpr
U : Nat
Γ₁ Γ₂ : List VExpr
H : CtxClosed Γ₀
Γ₁✝ Γ₂✝ : List VExpr
A₁✝ A₂✝ : VExpr
u✝ : VLevel
h1 : IsDefEqCtx env U Γ₀ Γ₁✝ Γ₂✝
h2 : IsDefEq env U Γ₁✝ A₁✝ A₂✝ (sort u✝)
c1 : CtxClosed Γ₁✝
c2 : CtxClosed Γ₂✝
⊢ (fun Γ A => ClosedN A (List.length Γ)) Γ₂✝ A₂✝
Tactic:
simpa [h1.length_eq] using h2.symm.closedN henv c1
State after:
no goals