{α : Type u_1} →
  (motive : Lists α → Lists α → Sort u_2) →
    (x x_1 : Lists α) →
      ((l₁ l₂ : Lists' α false) → motive ⟨false, l₁⟩ ⟨false, l₂⟩) →
        ((l₁ : Lists' α false) → (l₂ : Lists' α true) → motive ⟨false, l₁⟩ ⟨true, l₂⟩) →
          ((l₁ : Lists' α true) → (l₂ : Lists' α false) → motive ⟨true, l₁⟩ ⟨false, l₂⟩) →
            ((l₁ l₂ : Lists' α true) → motive ⟨true, l₁⟩ ⟨true, l₂⟩) → motive x x_1