(* *)
(**************************************************************************)
-include "static_2/relocation/lifts_tdeq.ma".
+include "static_2/relocation/lifts_teqx.ma".
include "basic_2/rt_transition/cpx_drops.ma".
include "basic_2/rt_transition/cnx.ma".
lemma cnx_lifts: ∀h,G. d_liftable1 … (cnx h G).
#h #G #K #T #HT #b #f #L #HLK #U #HTU #U0 #H
elim (cpx_inv_lifts_sn … H … HLK … HTU) -b -L #T0 #HTU0 #HT0
-lapply (HT … HT0) -G -K /2 width=6 by tdeq_lifts_bi/
+lapply (HT … HT0) -G -K /2 width=6 by teqx_lifts_bi/
qed-.
(* Inversion lemmas with generic slicing ************************************)
#h #I #G #L #K #V #i #HLK #H
elim (lifts_total V (𝐔❴↑i❵)) #W #HVW
lapply (H W ?) -H /2 width=7 by cpx_delta_drops/ -HLK
-#H lapply (tdeq_inv_lref1 … H) -H #H destruct
+#H lapply (teqx_inv_lref1 … H) -H #H destruct
/2 width=5 by lifts_inv_lref2_uni_lt/
qed-.
lemma cnx_inv_lifts: ∀h,G. d_deliftable1 … (cnx h G).
#h #G #L #U #HU #b #f #K #HLK #T #HTU #T0 #H
elim (cpx_lifts_sn … H … HLK … HTU) -b -K #U0 #HTU0 #HU0
-lapply (HU … HU0) -G -L /2 width=6 by tdeq_inv_lifts_bi/
+lapply (HU … HU0) -G -L /2 width=6 by teqx_inv_lifts_bi/
qed-.