∀ {α : Type u_1} [inst_1 : DecidableEq α] ⦃g : Equiv.Perm α⦄ (a b c w : α)
  (h_2 : 2 ≤ List.count w [b, c, g a, g (g a)]),
  (List.findIdxs (fun x => decide (x = w)) [b, c, g a, g (g a)])[1] < [b, c, g a, g (g a)].length