(* Basic_1: was just: pr3_iso_appls_beta *)
lemma cpxs_fwd_beta_vector (p) (G) (L):
∀Vs,V,W,T,X2. ❪G,L❫ ⊢ ⒶVs.ⓐV.ⓛ[p]W.T ⬈* X2 →
(* Basic_1: was just: pr3_iso_appls_beta *)
lemma cpxs_fwd_beta_vector (p) (G) (L):
∀Vs,V,W,T,X2. ❪G,L❫ ⊢ ⒶVs.ⓐV.ⓛ[p]W.T ⬈* X2 →