∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} (motive : Relation.Join FreeAddGroup.Red L₁ L₂ → Prop)
  (x : Relation.Join FreeAddGroup.Red L₁ L₂),
  (∀ (_L₃ : List (α × Bool)) (H13 : FreeAddGroup.Red L₁ _L₃) (H23 : FreeAddGroup.Red L₂ _L₃), motive ⋯) → motive x