{α : Type u_1} →
  (motive : (x : Bool) → Lists' α x → Sort u_2) →
    (x : Bool) →
      (x_1 : Lists' α x) →
        ((a : α) → motive false (Lists'.atom a)) →
          (Unit → motive true Lists'.nil) →
            ((b : Bool) → (a : Lists' α b) → (l : Lists' α true) → motive true (a.cons' l)) → motive x x_1