(* Forward lemmas involving same top term constructor ***********************)
-lemma cpxs_fwd_cnx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ∀U. ⦃G, L⦄ ⊢ T ➡*[h, g] U → T ≃ U.
+lemma cpxs_fwd_cnx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ∀U. ⦃G, L⦄ ⊢ T ➡*[h, g] U → T ≃ U.
#h #g #G #L #T #HT #U #H
>(cpxs_inv_cnx1 … H HT) -G -L -T //
qed-.
elim (IHn … Hnl) -IHn
[ #H lapply (tstc_inv_atom1 … H) -H #H >H -H /2 width=1 by or_intror/
| generalize in match Hnl; -Hnl @(nat_ind_plus … n) -n
- /4 width=3 by cpxs_strap2, cpx_sort, or_intror/
+ /4 width=3 by cpxs_strap2, cpx_st, or_intror/
| >iter_SO >iter_n_Sm //
]
]