-lemma ygt_strap2: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L, T⦄ →
- h ⊢ ⦃L, T⦄ >[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄.
-#h #g #L1 #L #L2 #T1 #T #T2 #H1 #H2 elim H2 -L2 -T2
-[ /3 width=4 by ygt_inj, yprs_strap2/ | /2 width=3/ ]
+lemma ygt_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ →
+ ⦃G, L, T⦄ >[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 elim H2 -G2 -L2 -T2
+[ /3 width=5 by ygt_inj, yprs_strap2/ | /2 width=3/ ]