lemma llor_total: ∀L1,L2,T,d. |L1| = |L2| → ∃L. L1 ⩖[T, d] L2 ≡ L.
#L1 @(lenv_ind_alt … L1) -L1
[ #L2 #T #d #H >(length_inv_zero_sn … H) -L2 /2 width=2 by ex_intro/
lemma llor_total: ∀L1,L2,T,d. |L1| = |L2| → ∃L. L1 ⩖[T, d] L2 ≡ L.
#L1 @(lenv_ind_alt … L1) -L1
[ #L2 #T #d #H >(length_inv_zero_sn … H) -L2 /2 width=2 by ex_intro/