no goals
α : Type u_1
a b : α
x✝ : Nat
⊢ set (set [] x✝ a) x✝ b = set [] x✝ b
simp
no goals
α : Type u_1
a b head✝ : α
tail✝ : List α
⊢ set (set (head✝ :: tail✝) 0 a) 0 b = set (head✝ :: tail✝) 0 b
simp [set]
no goals
α : Type u_1
a b head✝ : α
tail✝ : List α
n✝ : Nat
⊢ set (set (head✝ :: tail✝) (n✝ + 1) a) (n✝ + 1) b = set (head✝ :: tail✝) (n✝ + 1) b
simp [set, set_set]