{motive : Std.Do.PostShape → Sort u_1} →
  motive Std.Do.PostShape.pure →
    ((σ : Type u) → (a : Std.Do.PostShape) → motive a → motive (Std.Do.PostShape.arg σ a)) →
      ((ε : Type u) → (a : Std.Do.PostShape) → motive a → motive (Std.Do.PostShape.except ε a)) →
        (t : Std.Do.PostShape) → motive t