Theorem: Lean4Lean.IsFVarUpSet.trivial (Lean4Lean/Verify/Typing/Lemmas.lean)

State before:
val✝ : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
x✝ : (fun x => True) val✝
⊢ VLocalDecl.OnVars (fun i => ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → (fun x => True) fv) d
Tactic:
cases d <;> simp [VLocalDecl.OnVars, VExpr.OnVars]
State after:
no goals