∀ (b x : Bool) (l : List Bool) (h : List.count b (x :: l) + 2 ≤ List.count (!b) (x :: l)),
  (List.findIdxs (fun x => decide (x = !b)) (x :: l))[0] + 1 ≤ List.findIdx (fun x => decide (x = !b)) (x :: l) →
    (List.findIdxs (fun x => decide (x = !b)) (x :: l))[0].succ ≤ (x :: l).length