-lemma cpg_inv_atom1_drops: ∀Rt,c,h,I,G,L,T2. ❪G,L❫ ⊢ ⓪[I] ⬈[Rt,c,h] T2 →
- ∨∨ T2 = ⓪[I] ∧ c = 𝟘𝟘
- | ∃∃s. T2 = ⋆(⫯[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