X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Flib%2Flstar_2a.ma;h=dc3ed1ef34ff6c81ef09525f6953c9833ff90cf7;hp=ba513ae859d49cc7e0147893ab01b72d9d5b2202;hb=ae626612bff9c3746dd7647bbada791c737e348c;hpb=4d232392091ee233afc26ecf3120dd5f5c6a33c8

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/lstar_2a.ma b/matita/matita/contribs/lambdadelta/ground/lib/lstar_2a.ma
index ba513ae85..dc3ed1ef3 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/lstar_2a.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/lstar_2a.ma
@@ -15,7 +15,7 @@
 include "ground/lib/ltc.ma".
 include "ground/arith/nat_plus.ma".
 
-(* NAT-LABELED REFLEXIVE AND TRANSITIVE CLOSURE FOR FOR λδ-2A ***************)
+(* NAT-LABELED REFLEXIVE AND TRANSITIVE CLOSURE FOR λδ-2A *******************)
 
 definition lstar_aux (B) (R:relation B) (l): relation B ≝
            λb1,b2. ∨∨ (∧∧ l = 𝟎 & b1 = b2) | (∧∧ l = 𝟏  & R b1 b2).