no goals
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <+~ l₂
t : List α
⊢ List.diff l₁ t <+~ List.diff l₂ t
induction t generalizing l₁ l₂ h <;> simp [*, Subperm.erase]