{α β : Type} →
  (motive : Lean.Widget.StrictOrLazy α β → Sort u_1) →
    (x : Lean.Widget.StrictOrLazy α β) →
      ((x : α) → motive (Lean.Widget.StrictOrLazy.strict x)) →
        ((x : β) → motive (Lean.Widget.StrictOrLazy.lazy x)) → motive x