-lemma cpg_inv_appl1_simple: ∀c,h,G,L,V1,T1,U. ⦃G, L⦄ ⊢ ⓐV1.T1 ⬈[c, h] U → 𝐒⦃T1⦄ →
- ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ T1 ⬈[cT, h] T2 &
- U = ⓐV2.T2 & c = ((↓cV)∨cT).
-#c #h #G #L #V1 #T1 #U #H #HT1 elim (cpg_inv_appl1 … H) -H *
+lemma cpg_inv_appl1_simple (Rs) (Rk) (c) (G) (L):
+ ∀V1,T1,U. ❨G,L❩ ⊢ ⓐV1.T1 ⬈[Rs,Rk,c] U → 𝐒❨T1❩ →
+ ∃∃cV,cT,V2,T2. ❨G,L❩ ⊢ V1 ⬈[Rs,Rk,cV] V2 & ❨G,L❩ ⊢ T1 ⬈[Rs,Rk,cT] T2 & U = ⓐV2.T2 & c = ((↕*cV)∨cT).
+#Rs #Rk #c #G #L #V1 #T1 #U #H #HT1 elim (cpg_inv_appl1 … H) -H *