∀ (motive : (ps : Std.Do.PostShape) → Std.Do.ExceptConds ps → Std.Do.ExceptConds ps → Sort u_2) (σ : Type u_1)
  (ps : Std.Do.PostShape) (x y : Std.Do.ExceptConds (Std.Do.PostShape.arg σ ps))
  (h_1 : (x y : Std.Do.ExceptConds Std.Do.PostShape.pure) → motive Std.Do.PostShape.pure x y)
  (h_2 :
    (σ : 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)
  (h_3 :
    (ε : 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),
  (match Std.Do.PostShape.arg σ ps, x, y with
    | Std.Do.PostShape.pure, x, y => h_1 x y
    | Std.Do.PostShape.arg σ ps, x, y => h_2 σ ps x y
    | Std.Do.PostShape.except ε ps, x, y => h_3 ε ps x y) =
    h_2 σ ps x y