X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Fcpg_drops.ma;h=977ec175d1728520f85d8fb8fde5cc712a6feaa2;hp=71d38a1ba0fbd4e1652a2c6e73aaa6ef07ec32bd;hb=647b419e96770d90a82d7a9e5e8843566a9f93ee;hpb=f308429a0fde273605a2330efc63268b4ac36c99

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma
index 71d38a1ba..977ec175d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma
@@ -63,7 +63,7 @@ qed-.
 
 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 = 𝟘𝟙
+                            | ∃∃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 &