/3 width=6 by cpre_mono/
]
qed-.
-
-(* Advanced inversion lemmas with t-bound rt-equivalence for terms **********)
-
-lemma cnv_inv_appl_SO_cpes (a) (h) (G) (L):
- ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] →
- ∃∃n,p,W,U. a = Ⓣ → n = 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
- ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W.U.
-#a #h #G #L #V #T #H
-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-.