#R1 #R2 #HR #L1 #L2 #T * /4 width=7 by lexs_co, ex2_intro/
qed-.
+lemma lfxs_isid: ∀R1,R2,L1,L2,T1,T2.
+ (∀f. L1 ⊢ 𝐅*⦃T1⦄ ≡ f → 𝐈⦃f⦄) →
+ (∀f. 𝐈⦃f⦄ → L1 ⊢ 𝐅*⦃T2⦄ ≡ f) →
+ L1 ⦻*[R1, T1] L2 → L1 ⦻*[R2, T2] L2.
+#R1 #R2 #L1 #L2 #T1 #T2 #H1 #H2 *
+/4 width=7 by lexs_co_isid, ex2_intro/
+qed-.
+
(* Basic inversion lemmas ***************************************************)
lemma lfxs_inv_atom_sn: ∀R,Y2,T. ⋆ ⦻*[R, T] Y2 → Y2 = ⋆.
/2 width=3 by ex1_2_intro/
qed-.
-(* Basic_2A1: removed theorems 24:
+(* Basic_2A1: removed theorems 25:
llpx_sn_sort llpx_sn_skip llpx_sn_lref llpx_sn_free llpx_sn_gref
llpx_sn_bind llpx_sn_flat
llpx_sn_inv_bind llpx_sn_inv_flat
llpx_sn_fwd_lref llpx_sn_fwd_pair_sn llpx_sn_fwd_length
llpx_sn_fwd_bind_sn llpx_sn_fwd_bind_dx llpx_sn_fwd_flat_sn llpx_sn_fwd_flat_dx
llpx_sn_refl llpx_sn_Y llpx_sn_bind_O llpx_sn_ge_up llpx_sn_ge llpx_sn_co
- llpx_sn_fwd_drop_sn llpx_sn_fwd_drop_dx
+ llpx_sn_fwd_drop_sn llpx_sn_fwd_drop_dx
+ llpx_sn_dec
*)