lemma cnv_inv_appl_cpts (h) (a) (nv) (nt) (p) (G) (L):
∀V1. ❪G,L❫ ⊢ V1 ![h,a] → ∀V2. ❪G,L❫ ⊢ V1 ⬆*[h,nv] V2 →
∀T1. ❪G,L❫ ⊢ T1 ![h,a] → ∀T2. ❪G,L❫ ⊢ T1 ⬆*[h,nt] T2 →
lemma cnv_inv_appl_cpts (h) (a) (nv) (nt) (p) (G) (L):
∀V1. ❪G,L❫ ⊢ V1 ![h,a] → ∀V2. ❪G,L❫ ⊢ V1 ⬆*[h,nv] V2 →
∀T1. ❪G,L❫ ⊢ T1 ![h,a] → ∀T2. ❪G,L❫ ⊢ T1 ⬆*[h,nt] T2 →