X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Fsh_props.ma;h=53c4cfcfc9367a582f31e616a1a1bca878850bba;hp=4302026d4db8138d9e778b7aef8748bb7571f36f;hb=98e786e1a6bd7b621e37ba7cd4098d4a0a6f8278;hpb=5d9f7ae4bad2b5926f615141c12942b9a8eb23fb

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/sh_props.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/sh_props.ma
index 4302026d4..53c4cfcfc 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/sh_props.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/sh_props.ma
@@ -12,18 +12,19 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "static_2/syntax/sh.ma".
+include "static_2/syntax/sh_nexts.ma".
 
 (* SORT HIERARCHY ***********************************************************)
 
 (* acyclicity condition *)
 record sh_acyclic (h): Prop ≝
 {
-  nexts_inj: ∀s,n1,n2. (next h)^n1 s = (next h)^n2 s → n1 = n2
+(**) (* use extensional equivalence *) 
+  sh_nexts_inj: ∀s,n1,n2. ⇡*[h,n1]s = ⇡*[h,n2]s → n1 = n2
 }.
 
 (* decidability condition *)
 record sh_decidable (h): Prop ≝
 {
-  nexts_dec: ∀s1,s2. Decidable (∃n. (next h)^n s1 = s2)
+  sh_nexts_dec: ∀s1,s2. Decidable (∃n. ⇡*[h,n]s1 = s2)
 }.