d ≤ dt → dt ≤ d + e → L1 ⋕[U, d] L2.
#L1 #L2 #U #dt * #HL12 #IH #T #d #e #HTU #Hddt #Hdtde @conj // -HL12
#U0 elim (IH U0) -IH #H12 #H21 @conj
d ≤ dt → dt ≤ d + e → L1 ⋕[U, d] L2.
#L1 #L2 #U #dt * #HL12 #IH #T #d #e #HTU #Hddt #Hdtde @conj // -HL12
#U0 elim (IH U0) -IH #H12 #H21 @conj