-(* Basic_1: was just: nf2_iso_appls_lref *)
-lemma cpxs_fwd_cnx_vector: ∀h,o,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ →
- ∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.T ⬈*[h, o] U → ⒶVs.T ≂ U.
-#h #o #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *)
-#V #Vs #IHVs #U #H
-elim (cpxs_inv_appl1 … H) -H *
-[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair/
-| #a #W0 #T0 #HT0 #HU
- lapply (IHVs … HT0) -IHVs -HT0 #HT0
- elim (tsts_inv_bind_applv_simple … HT0) //
-| #a #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU
- lapply (IHVs … HT0) -IHVs -HT0 #HT0
- elim (tsts_inv_bind_applv_simple … HT0) //
-]
-qed-.
-
-lemma cpxs_fwd_sort_vector: ∀h,o,G,L,s,Vs,U. ⦃G, L⦄ ⊢ ⒶVs.⋆s ⬈*[h, o] U →
- ⒶVs.⋆s ≂ U ∨ ⦃G, L⦄ ⊢ ⒶVs.⋆(next h s) ⬈*[h, o] U.
+lemma cpxs_fwd_sort_vector: ∀h,o,G,L,s,Vs,U. ⦃G, L⦄ ⊢ ⒶVs.⋆s ⬈*[h] U →
+ ⒶVs.⋆s ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⒶVs.⋆(next h s) ⬈*[h] U.