lemma cnv_inv_appl_cpes (h) (a) (G) (L):
∀V,T. ❪G,L❫ ⊢ ⓐV.T ![h,a] →
∃∃n,p,W,U. ad a n & ❪G,L❫ ⊢ V ![h,a] & ❪G,L❫ ⊢ T ![h,a] &
lemma cnv_inv_appl_cpes (h) (a) (G) (L):
∀V,T. ❪G,L❫ ⊢ ⓐV.T ![h,a] →
∃∃n,p,W,U. ad a n & ❪G,L❫ ⊢ V ![h,a] & ❪G,L❫ ⊢ T ![h,a] &