∀ {α : Type u_1} {β : α → Type u_2} [inst : BEq α] {l₂ : List α} (t : List ((a : α) × β a)),
  (List.filter (fun p => !l₂.contains p.fst) t).length + (List.filter (fun p => l₂.contains p.fst) t).length =
      t.length →
    ¬(List.filter (fun p => !l₂.contains p.fst) t).length + 1 + (List.filter (fun p => l₂.contains p.fst) t).length =
          t.length + 1 →
      False