Theorem: Lean4Lean.VLCtx.IsDefEq.symm (Lean4Lean/Verify/Typing/Lemmas.lean)

State before:
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
h1 : IsDefEq env U Δ₁✝ Δ₂✝
h2 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h3 : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
⊢ ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₂✝
Tactic:
simpa [h1.fvars] using h2
State after:
no goals