+lemma lfxs_trans_next: ∀R1,R2,R3. lfxs_transitive R1 R2 R3 → lfxs_transitive_next R1 R2 R3.
+#R1 #R2 #R3 #HR #f #L1 #T #Hf #g #I1 #K1 #n #HLK #Hgf #I #H
+generalize in match HLK; -HLK elim H -I1 -I
+[ #I #_ #L2 #_ #I2 #H
+ lapply (ext2_inv_unit_sn … H) -H #H destruct
+ /2 width=1 by ext2_unit/
+| #I #V1 #V #HV1 #HLK1 #L2 #HL12 #I2 #H
+ elim (ext2_inv_pair_sn … H) -H #V2 #HV2 #H destruct
+ elim (frees_inv_drops_next … Hf … HLK1 … Hgf) -f -HLK1 #f #Hf #Hfg
+ /5 width=5 by ext2_pair, sle_lexs_trans, ex2_intro/
+]
+qed.
+