K1 ⋕[V, 0] K2 → L1 ⋕[T, d] L2.
#L1 #L2 #T #d0 #H @(lleq_ind_alt … H) -L1 -L2 -T -d0
/2 width=1 by lleq_gref, lleq_free, lleq_sort/
K1 ⋕[V, 0] K2 → L1 ⋕[T, d] L2.
#L1 #L2 #T #d0 #H @(lleq_ind_alt … H) -L1 -L2 -T -d0
/2 width=1 by lleq_gref, lleq_free, lleq_sort/