Theorem: Lean4Lean.TrLCtx.wf (Lean4Lean/Verify/LocalContext.lean)

State before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv✝ : FVarId
map✝ : PersistentHashMap FVarId LocalDecl
arr✝ : PersistentArray (Option LocalDecl)
Δ✝ : VLCtx
d✝ : LocalDecl
d'✝ : VLocalDecl
a✝¹ : LocalDecl.fvarId d✝ = fv✝
h2 : PersistentHashMap.find? map✝ fv✝ = none
a✝ : LocalDecl.index d✝ = arr✝.size
h4 : TrLCtx env Us { fvarIdToDecl := map✝, decls := arr✝ } Δ✝
h5 : TrLocalDecl env Us Δ✝ d✝ d'✝
⊢ ∀ (fv : FVarId), some fv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ✝
Tactic:
simpa [← h4.find?_eq_some]
State after:
no goals