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