X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Fcpg.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Fcpg.ma;h=72656dd1ad04c852b33433f4790c709635316a59;hb=647b419e96770d90a82d7a9e5e8843566a9f93ee;hp=6d36b466c54fc65fbfbcf8c947fc93147c759f77;hpb=f308429a0fde273605a2330efc63268b4ac36c99;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma
index 6d36b466c..72656dd1a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma
@@ -15,7 +15,7 @@
 include "ground_2/steps/rtc_max.ma".
 include "ground_2/steps/rtc_plus.ma".
 include "basic_2/notation/relations/predty_7.ma".
-include "static_2/syntax/sort.ma".
+include "static_2/syntax/sh.ma".
 include "static_2/syntax/lenv.ma".
 include "static_2/syntax/genv.ma".
 include "static_2/relocation/lifts.ma".
@@ -25,7 +25,7 @@ include "static_2/relocation/lifts.ma".
 (* avtivate genv *)
 inductive cpg (Rt:relation rtc) (h): rtc → relation4 genv lenv term term ≝
 | cpg_atom : ∀I,G,L. cpg Rt h (𝟘𝟘) G L (⓪{I}) (⓪{I})
-| cpg_ess  : ∀G,L,s. cpg Rt h (𝟘𝟙) G L (⋆s) (⋆(next h s))
+| cpg_ess  : ∀G,L,s. cpg Rt h (𝟘𝟙) G L (⋆s) (⋆(⫯[h]s))
 | cpg_delta: ∀c,G,L,V1,V2,W2. cpg Rt h c G L V1 V2 →
              ⬆*[1] V2 ≘ W2 → cpg Rt h c G (L.ⓓV1) (#0) W2
 | cpg_ell  : ∀c,G,L,V1,V2,W2. cpg Rt h c G L V1 V2 →
@@ -70,7 +70,7 @@ qed.
 
 fact cpg_inv_atom1_aux: ∀Rt,c,h,G,L,T1,T2. ⦃G,L⦄ ⊢ T1 ⬈[Rt,c,h] T2 → ∀J. T1 = ⓪{J} →
                         ∨∨ T2 = ⓪{J} ∧ c = 𝟘𝟘 
-                         | ∃∃s. J = Sort s & T2 = ⋆(next h s) & c = 𝟘𝟙
+                         | ∃∃s. J = Sort s & T2 = ⋆(⫯[h]s) & c = 𝟘𝟙
                          | ∃∃cV,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬈[Rt,cV,h] V2 & ⬆*[1] V2 ≘ T2 &
                                          L = K.ⓓV1 & J = LRef 0 & c = cV
                          | ∃∃cV,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬈[Rt,cV,h] V2 & ⬆*[1] V2 ≘ T2 &
@@ -96,7 +96,7 @@ qed-.
 
 lemma cpg_inv_atom1: ∀Rt,c,h,J,G,L,T2. ⦃G,L⦄ ⊢ ⓪{J} ⬈[Rt,c,h] T2 →
                      ∨∨ T2 = ⓪{J} ∧ c = 𝟘𝟘 
-                      | ∃∃s. J = Sort s & T2 = ⋆(next h s) & c = 𝟘𝟙
+                      | ∃∃s. J = Sort s & T2 = ⋆(⫯[h]s) & c = 𝟘𝟙
                       | ∃∃cV,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬈[Rt,cV,h] V2 & ⬆*[1] V2 ≘ T2 &
                                       L = K.ⓓV1 & J = LRef 0 & c = cV
                       | ∃∃cV,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬈[Rt,cV,h] V2 & ⬆*[1] V2 ≘ T2 &
@@ -106,7 +106,7 @@ lemma cpg_inv_atom1: ∀Rt,c,h,J,G,L,T2. ⦃G,L⦄ ⊢ ⓪{J} ⬈[Rt,c,h] T2 →
 /2 width=3 by cpg_inv_atom1_aux/ qed-.
 
 lemma cpg_inv_sort1: ∀Rt,c,h,G,L,T2,s. ⦃G,L⦄ ⊢ ⋆s ⬈[Rt,c,h] T2 →
-                     ∨∨ T2 = ⋆s ∧ c = 𝟘𝟘 | T2 = ⋆(next h s) ∧ c = 𝟘𝟙.
+                     ∨∨ T2 = ⋆s ∧ c = 𝟘𝟘 | T2 = ⋆(⫯[h]s) ∧ c = 𝟘𝟙.
 #Rt #c #h #G #L #T2 #s #H
 elim (cpg_inv_atom1 … H) -H * /3 width=1 by or_introl, conj/
 [ #s0 #H destruct /3 width=1 by or_intror, conj/