{m : Type u → Type v} →
  {ps : Std.Do.PostShape} →
    {motive : Std.Do.WP m ps → Sort u_1} →
      ((wp : {α : Type u} → m α → Std.Do.PredTrans ps α) → motive { wp := wp }) → (t : Std.Do.WP m ps) → motive t