theorem lveq_inj_void_sn_ge: ∀K1,K2. |K2| ≤ |K1| →
∀n1,n2. K1 ≋ⓧ*[n1, n2] K2 →
∀m1,m2. K1.ⓧ ≋ⓧ*[m1, m2] K2 →
- â\88§â\88§ ⫯n1 = m1 & 0 = m2 & 0 = n2.
+ â\88§â\88§ â\86\91n1 = m1 & 0 = m2 & 0 = n2.
#L1 #L2 #HL #n1 #n2 #Hn #m1 #m2 #Hm
elim (lveq_fwd_length … Hn) -Hn #H1 #H2 destruct
elim (lveq_fwd_length … Hm) -Hm #H1 #H2 destruct
theorem lveq_inj_void_dx_le: ∀K1,K2. |K1| ≤ |K2| →
∀n1,n2. K1 ≋ⓧ*[n1, n2] K2 →
∀m1,m2. K1 ≋ⓧ*[m1, m2] K2.ⓧ →
- â\88§â\88§ ⫯n2 = m2 & 0 = m1 & 0 = n1.
+ â\88§â\88§ â\86\91n2 = m2 & 0 = m1 & 0 = n1.
/3 width=5 by lveq_inj_void_sn_ge, lveq_sym/ qed-. (* auto: 2x lveq_sym *)