X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Farith.ma;h=b854c356909aef97473e8bc883bc0965517da022;hb=08cb57944c0df08611d4f35d286e46c0d13e4813;hp=8afc445b8f4343d68494ce3e774ebc8beb196c9c;hpb=9245402674a791dfdb943902f8288d742088c854;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/arith.ma
index 8afc445b8..b854c3569 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/arith.ma
@@ -103,7 +103,7 @@ qed.
 
 (* Note: this is "if eqb n1 n2 then a2 else if leb n1 n2 then a1 else a3" *)
 let rec tri (A:Type[0]) n1 n2 a1 a2 a3 on n1 : A ≝
-  match n1 with 
+  match n1 with
   [ O    ⇒ match n2 with [ O ⇒ a2 | S n2 ⇒ a1 ]
   | S n1 ⇒ match n2 with [ O ⇒ a3 | S n2 ⇒ tri A n1 n2 a1 a2 a3 ]
   ].