Theorem: Lean4Lean.InScope.fvars_cons (Lean4Lean/Verify/Typing/Lemmas.lean)

State before:
Δ : VLCtx
e : Expr
k : Nat
ofv : Option FVarId
d : VLocalDecl
a : FVarId
h : a ∈ VLCtx.fvars Δ
⊢ a ∈ VLCtx.fvars ((ofv, d) :: Δ)
Tactic:
cases ofv <;> simp [h]
State after:
no goals