+
+(* Properties with restricted refinement for local environments *************)
+
+lemma csx_lsubr_conf (h) (G) (L1):
+ ∀T. ❪G,L1❫ ⊢ ⬈*𝐒[h] T → ∀L2. L1 ⫃ L2 → ❪G,L2❫ ⊢ ⬈*𝐒[h] T.
+#h #G #L1 #T #H
+@(csx_ind … H) -T #T1 #_ #IH #L2 #HL12
+@csx_intro #T2 #HT12 #HnT12
+/3 width=3 by lsubr_cpx_trans/
+qed-.