(motive : (ps : Std.Do.PostShape) → Std.Do.ExceptConds ps → Std.Do.ExceptConds ps → Sort u_2) →
  (ps : Std.Do.PostShape) →
    (x y : Std.Do.ExceptConds ps) →
      ((x y : Std.Do.ExceptConds Std.Do.PostShape.pure) → motive Std.Do.PostShape.pure x y) →
        ((σ : Type u_1) →
            (ps : Std.Do.PostShape) →
              (x y : Std.Do.ExceptConds (Std.Do.PostShape.arg σ ps)) → motive (Std.Do.PostShape.arg σ ps) x y) →
          ((ε : Type u_1) →
              (ps : Std.Do.PostShape) →
                (x y : Std.Do.ExceptConds (Std.Do.PostShape.except ε ps)) → motive (Std.Do.PostShape.except ε ps) x y) →
            motive ps x y