X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Flib%2Fstar.ma;h=5e748c5ea74ca8a369f09c40251f8e272c1054fe;hp=e1580c46eb241c25a832c74897ace7810c02445f;hb=6604a232815858a6c75dd25ac45abd68438077ff;hpb=888840f6b3a71d3d686b53b702d362ab90ab0038

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/star.ma b/matita/matita/contribs/lambdadelta/ground/lib/star.ma
index e1580c46e..5e748c5ea 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/star.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/star.ma
@@ -149,7 +149,7 @@ lemma SN_to_NF: ∀A,R,S. NF_dec A R S →
 * #a0 #Ha10 #Ha01 elim (IHa1 … Ha10 Ha01) -IHa1 -Ha01 /3 width=3 by star_compl, ex2_intro/
 qed-.
 
-(* Relations on unboxed pairs ***********************************************)
+(* Relations with unboxed pairs *********************************************)
 
 lemma bi_TC_strip: ∀A,B,R. bi_confluent A B R →
                    ∀a0,a1,b0,b1. R a0 b0 a1 b1 → ∀a2,b2. bi_TC … R a0 b0 a2 b2 →
@@ -190,7 +190,7 @@ lemma bi_TC_decomp_l: ∀A,B. ∀R:bi_relation A B.
 ]
 qed-.
 
-(* Relations on unboxed triples *********************************************)
+(* Relations with unboxed triples *******************************************)
 
 definition tri_star: ∀A,B,C,R. tri_relation A B C ≝
                      λA,B,C,R. tri_RC A B C (tri_TC … R).