Theorem: Ctx.set_ne_comm (STLC.lean)

State before:
ty₂ ty₁ : Ty
ctx : Ctx
x₁ x₂ : Nat
h : autoParam (x₁ ≠ x₂) _auto✝
⊢ ctx[x₁ ↦ ty₁][x₂ ↦ ty₂] = ctx[x₂ ↦ ty₂][x₁ ↦ ty₁]
Tactic:
funext
State after:
case h
ty₂ ty₁ : Ty
ctx : Ctx
x₁ x₂ : Nat
h : autoParam (x₁ ≠ x₂) _auto✝
x✝ : Nat
⊢ ctx[x₁ ↦ ty₁][x₂ ↦ ty₂] x✝ = ctx[x₂ ↦ ty₂][x₁ ↦ ty₁] x✝

State before:
case h
ty₂ ty₁ : Ty
ctx : Ctx
x₁ x₂ : Nat
h : autoParam (x₁ ≠ x₂) _auto✝
x✝ : Nat
⊢ ctx[x₁ ↦ ty₁][x₂ ↦ ty₂] x✝ = ctx[x₂ ↦ ty₂][x₁ ↦ ty₁] x✝
Tactic:
simp [set]
State after:
case h
ty₂ ty₁ : Ty
ctx : Ctx
x₁ x₂ : Nat
h : autoParam (x₁ ≠ x₂) _auto✝
x✝ : Nat
⊢ (if x✝ = x₂ then some ty₂ else if x✝ = x₁ then some ty₁ else ctx x✝) =
    if x✝ = x₁ then some ty₁ else if x✝ = x₂ then some ty₂ else ctx x✝

State before:
case h
ty₂ ty₁ : Ty
ctx : Ctx
x₁ x₂ : Nat
h : autoParam (x₁ ≠ x₂) _auto✝
x✝ : Nat
⊢ (if x✝ = x₂ then some ty₂ else if x✝ = x₁ then some ty₁ else ctx x✝) =
    if x✝ = x₁ then some ty₁ else if x✝ = x₂ then some ty₂ else ctx x✝
Tactic:
split <;> split <;> simp_all
State after:
no goals