-elim (cnv_inv_appl_SO … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU
-/3 width=7 by cpms_div, ex5_4_intro/
-qed-.
-
-lemma cnv_inv_appl_true_cpes (h) (G) (L):
- ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![h] →
- ∃∃p,W,U. ⦃G,L⦄ ⊢ V ![h] & ⦃G,L⦄ ⊢ T ![h] &
- ⦃G,L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G,L⦄ ⊢ T ➡*[1,h] ⓛ{p}W.U.
-#h #G #L #V #T #H
-elim (cnv_inv_appl_SO_cpes … H) -H #n #p #W #U #Hn
->Hn -n [| // ] #HV #HT #HVW #HTU
-/2 width=5 by ex4_3_intro/
+elim (cnv_inv_appl_pred … H) -H #p #W #U #HV #HT #HVW #HTU
+/3 width=7 by cpms_div, ex4_3_intro/