+(* Basic properties *********************************************************)
+
+lemma lfxs_atom: ∀R,I. ⋆ ⪤*[R, ⓪{I}] ⋆.
+#R * /3 width=3 by frees_sort, frees_atom, frees_gref, lexs_atom, ex2_intro/
+qed.
+
+(* Basic_2A1: uses: llpx_sn_sort *)
+lemma lfxs_sort: ∀R,I1,I2,L1,L2,s.
+ L1 ⪤*[R, ⋆s] L2 → L1.ⓘ{I1} ⪤*[R, ⋆s] L2.ⓘ{I2}.
+#R #I1 #I2 #L1 #L2 #s * #f #Hf #H12
+lapply (frees_inv_sort … Hf) -Hf
+/4 width=3 by frees_sort, lexs_push, isid_push, ex2_intro/
+qed.
+
+lemma lfxs_pair: ∀R,I,L1,L2,V1,V2. L1 ⪤*[R, V1] L2 →
+ R L1 V1 V2 → L1.ⓑ{I}V1 ⪤*[R, #0] L2.ⓑ{I}V2.
+#R #I1 #I2 #L1 #L2 #V1 *
+/4 width=3 by ext2_pair, frees_pair, lexs_next, ex2_intro/
+qed.
+
+lemma lfxs_unit: ∀R,f,I,L1,L2. 𝐈⦃f⦄ → L1 ⪤*[cext2 R, cfull, f] L2 →
+ L1.ⓤ{I} ⪤*[R, #0] L2.ⓤ{I}.
+/4 width=3 by frees_unit, lexs_next, ext2_unit, ex2_intro/ qed.
+
+lemma lfxs_lref: ∀R,I1,I2,L1,L2,i.
+ L1 ⪤*[R, #i] L2 → L1.ⓘ{I1} ⪤*[R, #⫯i] L2.ⓘ{I2}.
+#R #I1 #I2 #L1 #L2 #i * /3 width=3 by lexs_push, frees_lref, ex2_intro/
+qed.
+
+(* Basic_2A1: uses: llpx_sn_gref *)
+lemma lfxs_gref: ∀R,I1,I2,L1,L2,l.
+ L1 ⪤*[R, §l] L2 → L1.ⓘ{I1} ⪤*[R, §l] L2.ⓘ{I2}.
+#R #I1 #I2 #L1 #L2 #l * #f #Hf #H12
+lapply (frees_inv_gref … Hf) -Hf
+/4 width=3 by frees_gref, lexs_push, isid_push, ex2_intro/
+qed.
+
+lemma lfxs_bind_repl_dx: ∀R,I,I1,L1,L2,T.
+ L1.ⓘ{I} ⪤*[R, T] L2.ⓘ{I1} →
+ ∀I2. cext2 R L1 I I2 →
+ L1.ⓘ{I} ⪤*[R, T] L2.ⓘ{I2}.
+#R #I #I1 #L1 #L2 #T * #f #Hf #HL12 #I2 #HR
+/3 width=5 by lexs_pair_repl, ex2_intro/