apply Iff.trans List.pairwise_append
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ List.Nodup (as.data ++ [a]) ↔ Nodup as ∧ ¬a ∈ as
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ (List.Pairwise (fun x x_1 => x ≠ x_1) as.data ∧
      List.Pairwise (fun x x_1 => x ≠ x_1) [a] ∧ ∀ (a_1 : α), a_1 ∈ as.data → ∀ (b : α), b ∈ [a] → a_1 ≠ b) ↔
    Nodup as ∧ ¬a ∈ as