dsimp [Nodup]
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
x : Array α
⊢ Nodup (cons a x) ↔ ¬a ∈ x ∧ Nodup x
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
x : Array α
⊢ anyPair (cons a x) BEq.beq 0 (Nat.succ (size x)) = false ↔ ¬a ∈ x ∧ anyPair x BEq.beq 0 (size x) = false