X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fpnat_plus.ma;h=8fd6b5c47034a1cf6783ab55845b669dce8e9513;hp=1babf8eea5ea43544d48c15efe6894d50c7fca4d;hb=4d232392091ee233afc26ecf3120dd5f5c6a33c8;hpb=da0775e27b362e91ea1453a800bc403781cc2ca3 diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma index 1babf8eea..8fd6b5c47 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma @@ -43,7 +43,7 @@ qed. lemma pplus_comm: commutative … pplus. #p elim p -p // -qed-. (**) (* gets in the way with auto *) +qed-. (* * gets in the way with auto *) lemma pplus_assoc: associative … pplus. #p #q #r elim r -r //