-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] &
- ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G, L⦄ ⊢ T ➡*[↓a, h] ⓛ{p}W.U.
-#a #h #G #L #V #T #H
-elim (cnv_inv_appl_pred … H) -H #p #W #U #HV #HT #HVW #HTU
-/3 width=7 by cpms_div, ex4_3_intro/
-qed-.
-
-lemma cnv_inv_cast_cpes (a) (h) (G) (L):
- ∀U,T. ⦃G, L⦄ ⊢ ⓝU.T ![a, h] →
- ∧∧ ⦃G, L⦄ ⊢ U ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] & ⦃G, L⦄ ⊢ U ⬌*[h,0,1] T.
-#a #h #G #L #U #T #H
+lemma cnv_inv_cast_cpes (h) (a) (G) (L):
+ ∀U,T. ❨G,L❩ ⊢ ⓝU.T ![h,a] →
+ ∧∧ ❨G,L❩ ⊢ U ![h,a] & ❨G,L❩ ⊢ T ![h,a] & ❨G,L❩ ⊢ U ⬌*[h,0,1] T.
+#h #a #G #L #U #T #H