simp only [not_or, and_assoc]
case cons
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ ¬(b ∈ x ∨ b = a) ∧ Nodup x ∧ ¬a ∈ x ↔ (¬b ∈ x ∧ Nodup x) ∧ ¬(a = b ∨ a ∈ x)
case cons
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ ¬b ∈ x ∧ ¬b = a ∧ Nodup x ∧ ¬a ∈ x ↔ ¬b ∈ x ∧ Nodup x ∧ ¬a = b ∧ ¬a ∈ x