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

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_tri.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_tri.ma
index 617849d8f..e60f3f969 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/pnat_tri.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_tri.ma
@@ -22,7 +22,7 @@ rec definition ptri (A:Type[0]) p1 p2 a1 a2 a3 on p1 : A ≝
   | psucc p1 ⇒ match p2 with [ punit ⇒ a3 | psucc p2 ⇒ ptri A p1 p2 a1 a2 a3 ]
   ].
 
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
 
 lemma ptri_unit_bi (A) (a1) (a2) (a3):
       a2 = ptri A (𝟏) (𝟏) a1 a2 a3.
@@ -40,7 +40,7 @@ lemma ptri_succ_bi (A) (a1) (a2) (a3) (p1) (p2):
       ptri A (p1) (p2) a1 a2 a3 = ptri A (↑p1) (↑p2) a1 a2 a3.
 // qed.
 
-(* Advanced rewrites ********************************************************)
+(* Advanced constructions ***************************************************)
 
 lemma ptri_eq (A) (a1) (a2) (a3) (p): a2 = ptri A p p a1 a2 a3.
 #A #a1 #a2 #a3 #p elim p -p //