- degree assignment, static type assignment, iterated static type

[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..8345cbe42ac0d0cf72756ea2059a278306672389 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/star.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/star.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