| ypr_fsup : ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ypr h g G1 L1 T1 G2 L2 T2
| ypr_lpr : ∀L2. ⦃G1, L1⦄ ⊢ ➡ L2 → ypr h g G1 L1 T1 G1 L2 T1
| ypr_cpr : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡ T2 → ypr h g G1 L1 T1 G1 L1 T2
| ypr_fsup : ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ypr h g G1 L1 T1 G2 L2 T2
| ypr_lpr : ∀L2. ⦃G1, L1⦄ ⊢ ➡ L2 → ypr h g G1 L1 T1 G1 L2 T1
| ypr_cpr : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡ T2 → ypr h g G1 L1 T1 G1 L1 T2
-| ypr_ssta : â\88\80T2,l. â¦\83G1, L1â¦\84 â\8a¢ T1 â\80¢[h, g] â¦\83l+1, T2â¦\84 → ypr h g G1 L1 T1 G1 L1 T2
+| ypr_ssta : â\88\80T2,l. â¦\83G1, L1â¦\84 â\8a¢ T1 â\96ª[h, g] l+1 â\86\92 â¦\83G1, L1â¦\84 â\8a¢ T1 â\80¢[h, g] T2 → ypr h g G1 L1 T1 G1 L1 T2