Theorem: Lean4Lean.VEnv.addDefEq_le (Lean4Lean/Theory/Typing/Lemmas.lean)

State before:
df✝ : VDefEq
env : VEnv
df : VDefEq
h : env.defeqs df
⊢ (addDefEq env df✝).defeqs df
Tactic:
simp [addDefEq, h]
State after:
no goals