+
+(* Advanced forward lemmas **************************************************)
+
+fact csx_fwd_bind_dx_unit_aux (G) (L):
+ ∀U. ❨G,L❩ ⊢ ⬈*𝐒 U →
+ ∀p,I,J,V,T. U = ⓑ[p,I]V.T → ❨G,L.ⓤ[J]❩ ⊢ ⬈*𝐒 T.
+#G #L #U #H elim H -H #U0 #_ #IH #p #I #J #V #T #H destruct
+@csx_intro #T2 #HLT2 #HT2
+@(IH (ⓑ[p, I]V.T2)) -IH /2 width=4 by cpx_bind_unit/ -HLT2 #H
+elim (teqx_inv_pair … H) -H /2 width=1 by/
+qed-.
+
+lemma csx_fwd_bind_dx_unit (G) (L):
+ ∀p,I,V,T. ❨G,L❩ ⊢ ⬈*𝐒 ⓑ[p,I]V.T →
+ ∀J. ❨G,L.ⓤ[J]❩ ⊢ ⬈*𝐒 T.
+/2 width=6 by csx_fwd_bind_dx_unit_aux/ qed-.
+
+lemma csx_fwd_bind_unit (G) (L):
+ ∀p,I,V,T. ❨G,L❩ ⊢ ⬈*𝐒 ⓑ[p,I]V.T →
+ ∀J. ∧∧ ❨G,L❩ ⊢ ⬈*𝐒 V & ❨G,L.ⓤ[J]❩ ⊢ ⬈*𝐒 T.
+/3 width=4 by csx_fwd_pair_sn, csx_fwd_bind_dx_unit, conj/ qed-.
+
+(* Properties with restricted refinement for local environments *************)
+
+lemma csx_lsubr_conf (G) (L1):
+ ∀T. ❨G,L1❩ ⊢ ⬈*𝐒 T → ∀L2. L1 ⫃ L2 → ❨G,L2❩ ⊢ ⬈*𝐒 T.
+#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-.