X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_tri.ma;h=4fb5225e9e7105f08679666ab6f55aca46daaa35;hp=b5be40624809826d9b1765f679af410696ae4612;hb=21de0d35017656c5a55528390b54b0b2ae395b44;hpb=68e028d053806177e218ee1a5f8778d3011bef83

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_tri.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_tri.ma
index b5be40624..4fb5225e9 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_tri.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_tri.ma
@@ -25,7 +25,7 @@ definition ntri (A:Type[0]) (n1) (n2) (a1) (a2) (a3): A ≝
   | ninj  p1 ⇒ match n2 with [ nzero ⇒ a3 | ninj p2 ⇒ ptri A p1 p2 a1 a2 a3 ]
   ].
 
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
 
 lemma ntri_zero_bi (A) (a1) (a2) (a3):
       a2 = ntri A (𝟎) (𝟎) a1 a2 a3.
@@ -43,7 +43,7 @@ lemma ntri_inj_bi (A) (a1) (a2) (a3) (p1) (p2):
       ptri A (p1) (p2) a1 a2 a3 = ntri A (p1) (p2) a1 a2 a3.
 // qed.
 
-(* Advanced rewrites ********************************************************)
+(* Advanced constructions ***************************************************)
 
 (*** tri_eq *)
 lemma ntri_eq (A) (a1) (a2) (a3) (n): a2 = ntri A n n a1 a2 a3.