-lemma cpg_inv_atom1_drops: ∀Rt,c,h,I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ⬈[Rt, c, h] T2 →
- ∨∨ T2 = ⓪{I} ∧ c = 𝟘𝟘
- | ∃∃s. T2 = ⋆(next h s) & I = Sort s & c = 𝟘𝟙
- | ∃∃cV,i,K,V,V2. ⬇*[i] L ≘ K.ⓓV & ⦃G, K⦄ ⊢ V ⬈[Rt, cV, h] V2 &
- ⬆*[⫯i] V2 ≘ T2 & I = LRef i & c = cV
- | ∃∃cV,i,K,V,V2. ⬇*[i] L ≘ K.ⓛV & ⦃G, K⦄ ⊢ V ⬈[Rt, cV, h] V2 &
- ⬆*[⫯i] V2 ≘ T2 & I = LRef i & c = cV + 𝟘𝟙.
-#Rt #c #h * #n #G #L #T2 #H
+lemma cpg_inv_atom1_drops (Rs) (Rk) (c) (G) (L):
+ ∀I,T2. ❨G,L❩ ⊢ ⓪[I] ⬈[Rs,Rk,c] T2 →
+ ∨∨ ∧∧ T2 = ⓪[I] & c = 𝟘𝟘
+ | ∃∃s1,s2. Rs s1 s2 & T2 = ⋆s2 & I = Sort s1 & c = 𝟘𝟙
+ | ∃∃cV,i,K,V,V2. ⇩[i] L ≘ K.ⓓV & ❨G,K❩ ⊢ V ⬈[Rs,Rk,cV] V2 & ⇧[↑i] V2 ≘ T2 & I = LRef i & c = cV
+ | ∃∃cV,i,K,V,V2. ⇩[i] L ≘ K.ⓛV & ❨G,K❩ ⊢ V ⬈[Rs,Rk,cV] V2 & ⇧[↑i] V2 ≘ T2 & I = LRef i & c = cV + 𝟘𝟙.
+#Rs #Rk #c #G #L * #x #T2 #H