∀ {α : Type u} {motive : (a a_1 : List (α × Bool)) → FreeGroup.Red.Step a a_1 → Prop},
  (∀ {L₁ L₂ : List (α × Bool)} {x : α} {b : Bool}, motive (L₁ ++ (x, b) :: (x, !b) :: L₂) (L₁ ++ L₂) ⋯) →
    ∀ {a a_1 : List (α × Bool)} (t : FreeGroup.Red.Step a a_1), motive a a_1 t