- ∃∃L,T2. ⦃G1, L1, U2⦄ ⊐ ⦃G2, L, T2⦄ & L2 ≡[h, o, T1] L & T1 ≡[h, o] T2.
-#h #o #G1 #G2 #L1 #L2 #U1 #T1 #H elim H -G1 -G2 -L1 -L2 -U1 -T1
-[ #I #G #L #W #X #H >(tdeq_inv_lref1 … H) -H
+ ∃∃L,T2. ⦃G1, L1, U2⦄ ⊐[b] ⦃G2, L, T2⦄ & L2 ≡[h, o, T1] L & T1 ≡[h, o] T2.
+#h #o #b #G1 #G2 #L1 #L2 #U1 #T1 #H elim H -G1 -G2 -L1 -L2 -U1 -T1
+[ #I #G #L #W #X #H >(tdeq_inv_lref1 … H) -X