∀ {α : Type u_1} {xss : Array (Array α)} {p : α → Bool} {a : α},
  Array.find? p xss.flatten = some a ↔
    p a = true ∧
      ∃ as ys zs bs,
        xss = as.push (ys.push a ++ zs) ++ bs ∧ (∀ ws ∈ as, ∀ x ∈ ws, (!p x) = true) ∧ ∀ x ∈ ys, (!p x) = true