no goals
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
h : a ∈ l₁
⊢ List.insert a l₁ ~ List.insert a l₂
simpa [h, p.subset h] using p
no goals
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
h : ¬a ∈ l₁
⊢ List.insert a l₁ ~ List.insert a l₂
simpa [h, mt p.mem_iff.2 h] using p.cons a