∃∃J1,K1. K1 ≡[g] K2 & X = K1.ⓘ{J1}.
#g #J2 #X #K2 #H elim (lexs_inv_push2 … H) -H /2 width=4 by ex2_2_intro/
qed-.
(* Basic_2A1: includes: lreq_inv_pair *)
∃∃J1,K1. K1 ≡[g] K2 & X = K1.ⓘ{J1}.
#g #J2 #X #K2 #H elim (lexs_inv_push2 … H) -H /2 width=4 by ex2_2_intro/
qed-.
(* Basic_2A1: includes: lreq_inv_pair *)