X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fpts_dummy%2Fterms.ma;h=dc066c8823343eeb59cb31281e6d041cb36a52f0;hb=143c97a8fe657eb7b041dec2747b0e67b5899762;hp=554f8099cb453ac0719b17fb082ceddc3a2272ad;hpb=46e87acb755894f9234191d675eeb5db4f5b930b;p=helm.git

diff --git a/matita/matita/lib/pts_dummy/terms.ma b/matita/matita/lib/pts_dummy/terms.ma
index 554f8099c..dc066c882 100644
--- a/matita/matita/lib/pts_dummy/terms.ma
+++ b/matita/matita/lib/pts_dummy/terms.ma
@@ -9,8 +9,8 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "basics/list.ma".
-include "lambda/lambda_notation.ma".
+include "basics/lists/list.ma".
+include "pts_dummy/lambda_notation.ma".
 
 inductive T : Type[0] ≝
   | Sort: nat → T     (* starts from 0 *)
@@ -30,7 +30,7 @@ let rec Appl F l on l ≝ match l with
    ].
 
 lemma appl_append: ∀N,l,M. Appl M (l @ [N]) = App (Appl M l) N.
-#N #l elim l -l // #hd #tl #IHl #M >IHl //
+#N #l elim l -l // #hd #tl #IHl #M >IHl normalize //
 qed.
 
 (*