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.