(* Properties with degree-based equivalence for local environments **********)
(* Basic_2A1: uses: csx_lleq_conf *)
lemma csx_lfdeq_conf: ∀h,o,G,L1,T. ⦃G, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ →
(* Properties with degree-based equivalence for local environments **********)
(* Basic_2A1: uses: csx_lleq_conf *)
lemma csx_lfdeq_conf: ∀h,o,G,L1,T. ⦃G, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ →