- improved Makefile esp. with the "trim" function

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / sd.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma
index 63143b19b00e7f2012fe6fcdd492ac9e4c069de4..d6737a8ba73a519239d7db788aeee253a8aa67a6 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma
@@ -82,7 +82,7 @@ definition sd_SO: ∀h. nat → sd h ≝ λh,k. mk_sd h (deg_SO h k) ….
 qed.
 
 let rec sd_l (h:sh) (k:nat) (l:nat) on l : sd h ≝
-   match l with 
+   match l with
    [ O   ⇒ sd_O h
    | S l ⇒ match l with
            [ O ⇒ sd_SO h k