-lemma lfeq_fwd_bind_sn: ∀p,I,L1,L2,V,T. L1 ≡[ⓑ{p,I}V.T] L2 → L1 ≡[V] L2.
-/2 width=4 by lfxs_fwd_bind_sn/ qed-.
-
-lemma lfeq_fwd_bind_dx: ∀p,I,L1,L2,V,T.
- L1 ≡[ⓑ{p,I}V.T] L2 → L1.ⓑ{I}V ≡[T] L2.ⓑ{I}V.
-/2 width=2 by lfxs_fwd_bind_dx/ qed-.
-
-lemma lfeq_fwd_flat_sn: ∀I,L1,L2,V,T. L1 ≡[ⓕ{I}V.T] L2 → L1 ≡[V] L2.
-/2 width=3 by lfxs_fwd_flat_sn/ qed-.
-
-lemma lfeq_fwd_flat_dx: ∀I,L1,L2,V,T. L1 ≡[ⓕ{I}V.T] L2 → L1 ≡[T] L2.
-/2 width=3 by lfxs_fwd_flat_dx/ qed-.
-
-lemma lfeq_fwd_pair_sn: ∀I,L1,L2,V,T. L1 ≡[②{I}V.T] L2 → L1 ≡[V] L2.
-/2 width=3 by lfxs_fwd_pair_sn/ qed-.
-
-(* Advanceded forward lemmas with generic extension on referred entries *****)
+(* Basic_2A1: was: llpx_sn_lrefl *)
+(* Note: this should have been lleq_fwd_llpx_sn *)
+lemma lfeq_fwd_lfxs: ∀R. c_reflexive … R →
+ ∀L1,L2,T. L1 ≡[T] L2 → L1 ⪤*[R, T] L2.
+#R #HR #L1 #L2 #T * #f #Hf #HL12
+/4 width=7 by lexs_co, cext2_co, ex2_intro/
+qed-.