Theorem: Lean4Lean.VLCtx.WF.fvars_nodup (Lean4Lean/Verify/Typing/Lemmas.lean)

State before:
env : VEnv
U : Nat
fv : FVarId
snd✝ : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U Δ
h : ∀ (fv_1 : FVarId), some fv = some fv_1 → ¬fv_1 ∈ fvars Δ
right✝ : VLocalDecl.WF env U (VLCtx.toCtx Δ) snd✝
⊢ List.Nodup (fvars ((some fv, snd✝) :: Δ))
Tactic:
suffices fv ∉ fvars Δ from (fvars_nodup hΔ).cons (fun _ h e => this (e ▸ h))
State after:
env : VEnv
U : Nat
fv : FVarId
snd✝ : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U Δ
h : ∀ (fv_1 : FVarId), some fv = some fv_1 → ¬fv_1 ∈ fvars Δ
right✝ : VLocalDecl.WF env U (VLCtx.toCtx Δ) snd✝
⊢ ¬fv ∈ fvars Δ

State before:
env : VEnv
U : Nat
fv : FVarId
snd✝ : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U Δ
h : ∀ (fv_1 : FVarId), some fv = some fv_1 → ¬fv_1 ∈ fvars Δ
right✝ : VLocalDecl.WF env U (VLCtx.toCtx Δ) snd✝
⊢ ¬fv ∈ fvars Δ
Tactic:
simpa using h
State after:
no goals