∃∃J1,K1. K1 ⪤*[RN, RP, g] K2 & RP K1 J1 J2 & X = K1.ⓘ{J1}.
/2 width=7 by lexs_inv_push2_aux/ qed-.
(* Basic_2A1: includes lpx_sn_inv_pair *)
lemma lexs_inv_next: ∀RN,RP,f,I1,I2,L1,L2.
∃∃J1,K1. K1 ⪤*[RN, RP, g] K2 & RP K1 J1 J2 & X = K1.ⓘ{J1}.
/2 width=7 by lexs_inv_push2_aux/ qed-.
(* Basic_2A1: includes lpx_sn_inv_pair *)
lemma lexs_inv_next: ∀RN,RP,f,I1,I2,L1,L2.