theorem List.set_set_perm {α : Type u_1} {as : List α} {i j : Nat} (h₁ : i < as.length) (h₂ : j < as.length) : ((as.set i as[j]).set j as[i]).Perm as