+(* Basic_2A1: uses: lleq_sort *)
+lemma lfdeq_sort_length (h) (o): ∀L1,L2. |L1| = |L2| → ∀s. L1 ≛[h, o, ⋆s] L2.
+/2 width=1 by lfxs_sort_length/ qed.
+
+(* Basic_2A1: uses: lleq_gref *)
+lemma lfdeq_gref_length (h) (o): ∀L1,L2. |L1| = |L2| → ∀l. L1 ≛[h, o, §l] L2.
+/2 width=1 by lfxs_gref_length/ qed.
+
+lemma lfdeq_unit_length (h) (o): ∀L1,L2. |L1| = |L2| →
+ ∀I. L1.ⓤ{I} ≛[h, o, #0] L2.ⓤ{I}.
+/2 width=1 by lfxs_unit_length/ qed.
+