partial commit in static_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / syntax / sh_props.ma

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 4302026d4db8138d9e778b7aef8748bb7571f36f..53c4cfcfc9367a582f31e616a1a1bca878850bba 100644 (file)
--- 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)
 }.