{σ : Type} →
  {m : Type → Type} →
    {α : Type} →
      (motive : Option ((α × σ) × MLList m (α × σ)) → Sort u_1) →
        (__do_lift : Option ((α × σ) × MLList m (α × σ))) →
          (Unit → motive none) →
            ((x : α) → (s : σ) → (xs : MLList m (α × σ)) → motive (some ((x, s), xs))) → motive __do_lift