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