∀d,e,U1. L1 ⊢ T1 [d, e] ≫* U1 →
∃∃U2. L2 ⊢ U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2.
#L1 #L2 #HL12 #T1 #T2 * #T #HT1 #HT2 #d #e #U1 #HTU1
∀d,e,U1. L1 ⊢ T1 [d, e] ≫* U1 →
∃∃U2. L2 ⊢ U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2.
#L1 #L2 #HL12 #T1 #T2 * #T #HT1 #HT2 #d #e #U1 #HTU1