update in standard library

[helm.git] / matita / matita / lib / reverse_complexity / speedup.ma

diff --git a/matita/matita/lib/reverse_complexity/speedup.ma b/matita/matita/lib/reverse_complexity/speedup.ma
index f1e56d5600f9d11cfae0898ce2d14918febc1466..52b7db0ddc9e9ab800eae0a09bf40bd8ab3dbfc7 100644 (file)
--- 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
+