+(* Basic_2A1: uses: llpx_sn_sort *)
+lemma lfxs_sort_length (R): ∀L1,L2. |L1| = |L2| → ∀s. L1 ⪤*[R, ⋆s] L2.
+#R #L1 elim L1 -L1
+[ #Y #H #s >(length_inv_zero_sn … H) -H //
+| #K1 #I1 #IH #Y #H #s
+ elim (length_inv_succ_sn … H) -H #I2 #K2 #HK12 #H destruct
+ /3 width=1 by lfxs_sort/
+]
+qed.
+
+(* Basic_2A1: uses: llpx_sn_gref *)
+lemma lfxs_gref_length (R): ∀L1,L2. |L1| = |L2| → ∀l. L1 ⪤*[R, §l] L2.
+#R #L1 elim L1 -L1
+[ #Y #H #s >(length_inv_zero_sn … H) -H //
+| #K1 #I1 #IH #Y #H #s
+ elim (length_inv_succ_sn … H) -H #I2 #K2 #HK12 #H destruct
+ /3 width=1 by lfxs_gref/
+]
+qed.
+
+lemma lfxs_unit_length (R): ∀L1,L2. |L1| = |L2| → ∀I. L1.ⓤ{I} ⪤*[R, #0] L2.ⓤ{I}.
+/3 width=3 by lfxs_unit, lexs_length_isid/ qed.
+