(* Properties with restricted refinement for local environments *************)
lemma lsubr_cpxs_trans: ∀h,G. lsub_trans … (cpxs h G) lsubr.
(* Properties with restricted refinement for local environments *************)
lemma lsubr_cpxs_trans: ∀h,G. lsub_trans … (cpxs h G) lsubr.