Theorem: Lean4Lean.VLCtx.find?_eq_some (Lean4Lean/Verify/VLCtx.lean)

State before:
fv : FVarId
Δ : VLCtx
⊢ (∃ x, find? Δ (Sum.inr fv) = some x) ↔ fv ∈ fvars Δ
Tactic:
rw [← Option.isSome_iff_exists, ← lookup_isSome, Option.isSome_iff_exists, lookup_eq_some]
State after:
no goals