(* *)
(**************************************************************************)
-include "basic_2/rt_transition/lfpx_lfdeq.ma".
+include "basic_2/rt_transition/lpx_rdeq.ma".
include "basic_2/rt_computation/csx_drops.ma".
-(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
+(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
(* Advanced properties ******************************************************)
lemma csx_inv_lref_pair: ∀h,o,I,G,L,K,V,i. ⬇*[i] L ≘ K.ⓑ{I}V →
⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃#i⦄ → ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄.
#h #o #I #G #L #K #V #i #HLK #Hi
-elim (lifts_total V (ð\9d\90\94â\9d´â«¯i❵))
+elim (lifts_total V (ð\9d\90\94â\9d´â\86\91i❵))
/4 width=9 by csx_inv_lifts, csx_cpx_trans, cpx_delta_drops, drops_isuni_fwd_drop2/
qed-.