\forall h. PRed P1 (scut (prin h) q1) S P2 q2 S
| pred_b_dx: \forall p1,p2,Q1,Q2,S. PRed Q1 p1 S Q2 p2 S \to
\forall h. PRed Q1 (scut p1 (prin h)) S Q2 p2 S
\forall h. PRed P1 (scut (prin h) q1) S P2 q2 S
| pred_b_dx: \forall p1,p2,Q1,Q2,S. PRed Q1 p1 S Q2 p2 S \to
\forall h. PRed Q1 (scut p1 (prin h)) S Q2 p2 S