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

State before:
env : VEnv
U : Nat
Δ₁ Δ₂ : VLCtx
⊢ VLCtx.fvars [] = VLCtx.fvars []
Tactic:
simp
State after:
no goals

State before:
env : VEnv
U : Nat
Δ₁ Δ₂ : VLCtx
fv : FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
h1 : IsDefEq env U Δ₁✝ Δ₂✝
h2 : ∀ (fv_1 : FVarId), some fv = some fv_1 → ¬fv_1 ∈ VLCtx.fvars Δ₁✝
a✝ : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
⊢ VLCtx.fvars ((some fv, d₁✝) :: Δ₁✝) = VLCtx.fvars ((some fv, d₂✝) :: Δ₂✝)
Tactic:
simp [h1.fvars]
State after:
no goals