- lambdadelta: first commutation property on lazy equivalence for

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / star.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/star.ma b/matita/matita/contribs/lambdadelta/ground_2/star.ma
index da13e67452f37b6f59fcab87d6242da363c52a45..29131d108513acea78f62802cff0f02ab9ffdd3b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/star.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/star.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basics/star.ma".
+include "basics/star1.ma".
 include "ground_2/xoa_props.ma".
 include "ground_2/notation.ma".
 
@@ -122,7 +122,7 @@ definition NF: ∀A. relation A → relation A → predicate A ≝
 
 definition NF_dec: ∀A. relation A → relation A → Prop ≝
                    λA,R,S. ∀a1. NF A R S a1 ∨
-                   ∃∃a2. R … a1 a2 & (S a2 a1 → ⊥). 
+                   ∃∃a2. R … a1 a2 & (S a2 a1 → ⊥).
 
 inductive SN (A) (R,S:relation A): predicate A ≝
 | SN_intro: ∀a1. (∀a2. R a1 a2 → (S a2 a1 → ⊥) → SN A R S a2) → SN A R S a1