include "basic_2/i_static/tc_lfxs_fqup.ma".
include "basic_2/rt_computation/lfpxs.ma".
-(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****)
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
(* Advanced properties ******************************************************)
-(* Basic_2A1: uses: lpxs_refl *)
lemma lfpxs_refl: ∀h,G,T. reflexive … (lfpxs h G T).
/2 width=1 by tc_lfxs_refl/ qed.
⦃G, L1.ⓑ{I}V⦄ ⊢ ⬈*[h, T] L2.ⓑ{I}V.
/2 width=2 by tc_lfxs_fwd_bind_dx/ qed-.
+lemma lfpxs_fwd_bind_dx_void: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈*[h, ⓑ{p,I}V.T] L2 →
+ ⦃G, L1.ⓧ⦄ ⊢ ⬈*[h, T] L2.ⓧ.
+/2 width=4 by tc_lfxs_fwd_bind_dx_void/ qed-.
+
(* Advanced eliminators *****************************************************)
(* Basic_2A1: uses: lpxs_ind *)