{α : Type u_1} →
  (as bs : List α) →
    (motive : Decidable (as = bs) → Sort u_2) →
      (x : Decidable (as = bs)) →
        ((habs : as = bs) → motive (isTrue habs)) → ((nabs : ¬as = bs) → motive (isFalse nabs)) → motive x