∀ {α : Type u_1} {motive_1 : (a a_1 : Lists α) → a.Equiv a_1 → Prop}
  {motive_2 : (a a_1 : Lists' α true) → a.Subset a_1 → Prop},
  (∀ (l : Lists α), motive_1 l l ⋯) →
    (∀ {l₁ l₂ : Lists' α true} (a : l₁.Subset l₂) (a_1 : l₂.Subset l₁),
        motive_2 l₁ l₂ a → motive_2 l₂ l₁ a_1 → motive_1 ⟨true, l₁⟩ ⟨true, l₂⟩ ⋯) →
      (∀ {l : Lists' α true}, motive_2 Lists'.nil l ⋯) →
        (∀ {a a' : Lists α} {l l' : Lists' α true} (a_1 : a.Equiv a') (a_2 : a' ∈ l'.toList) (a_3 : l.Subset l'),
            motive_1 a a' a_1 → motive_2 l l' a_3 → motive_2 (Lists'.cons a l) l' ⋯) →
          ∀ {a a_1 : Lists α} (t : a.Equiv a_1), motive_1 a a_1 t