apply Iff.intro
α : Type u_1
inst✝ : DecidableEq α
xs : List α
⊢ differs xs = true ↔ DifferentList xs
case mp
α : Type u_1
inst✝ : DecidableEq α
xs : List α
⊢ differs xs = true → DifferentList xs

case mpr
α : Type u_1
inst✝ : DecidableEq α
xs : List α
⊢ DifferentList xs → differs xs = true