lemma cnv_inv_appl_pred_cpes (a) (h) (G) (L):
∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![yinj a,h] →
∃∃p,W,U. ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] &
lemma cnv_inv_appl_pred_cpes (a) (h) (G) (L):
∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![yinj a,h] →
∃∃p,W,U. ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] &