X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Freverse_complexity%2Fspeedup.ma;h=52b7db0ddc9e9ab800eae0a09bf40bd8ab3dbfc7;hb=98e786e1a6bd7b621e37ba7cd4098d4a0a6f8278;hp=f1e56d5600f9d11cfae0898ce2d14918febc1466;hpb=db020b4218272e2e35641ce3bc3b0a9b3afda899;p=helm.git

diff --git a/matita/matita/lib/reverse_complexity/speedup.ma b/matita/matita/lib/reverse_complexity/speedup.ma
index f1e56d560..52b7db0dd 100644
--- a/matita/matita/lib/reverse_complexity/speedup.ma
+++ b/matita/matita/lib/reverse_complexity/speedup.ma
@@ -1,4 +1,5 @@
 include "reverse_complexity/bigops_compl.ma".
+include "basics/core_notation/napart_2.ma".
 
 (********************************* the speedup ********************************)
 
@@ -569,4 +570,4 @@ lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
   @Hmono @(mono_h_of2 … Hr Hmono … ltin)
  ]
 qed.
-  
\ No newline at end of file
+