Theorem: Ctx.set_get_ne (STLC.lean)

State before:
ty : Ty
ctx : Ctx
x y : Nat
h : autoParam (x ≠ y) _auto✝
⊢ ctx[x ↦ ty] y = ctx y
Tactic:
simp [set, h.symm]
State after:
no goals