rewrite [anyPair_cons_zero]
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
x : Array α
⊢ anyPair (cons a x) BEq.beq 0 (Nat.succ (size x)) = false ↔
    any x (BEq.beq a) 0 (size x) = false ∧ anyPair x BEq.beq 0 (size x) = false
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (any x (BEq.beq a) 0 (size x) || anyPair x BEq.beq 0 (size x)) = false ↔
    any x (BEq.beq a) 0 (size x) = false ∧ anyPair x BEq.beq 0 (size x) = false