-fact csn_fwd_flat_dx_aux: ∀L,U. L ⊢ ⬊* U → ∀I,V,T. U = ⓕ{I} V. T → L ⊢ ⬊* T.
-#L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
+fact csn_fwd_pair_sn_aux: ∀h,g,L,U. ⦃h, L⦄ ⊢ ⬊*[g] U →
+ ∀I,V,T. U = ②{I}V.T → ⦃h, L⦄ ⊢ ⬊*[g] V.
+#h #g #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
+@csn_intro #V2 #HLV2 #HV2
+@(IH (②{I}V2.T)) -IH // /2 width=1/ -HLV2 #H destruct /2 width=1/
+qed-.
+
+(* Basic_1: was just: sn3_gen_head *)
+lemma csn_fwd_pair_sn: ∀h,g,I,L,V,T. ⦃h, L⦄ ⊢ ⬊*[g] ②{I}V.T → ⦃h, L⦄ ⊢ ⬊*[g] V.
+/2 width=5 by csn_fwd_pair_sn_aux/ qed-.
+
+fact csn_fwd_bind_dx_aux: ∀h,g,L,U. ⦃h, L⦄ ⊢ ⬊*[g] U →
+ ∀a,I,V,T. U = ⓑ{a,I}V.T → ⦃h, L.ⓑ{I}V⦄ ⊢ ⬊*[g] T.
+#h #g #L #U #H elim H -H #U0 #_ #IH #a #I #V #T #H destruct