update in lib

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

diff --git a/matita/matita/lib/reverse_complexity/hierarchy.ma b/matita/matita/lib/reverse_complexity/hierarchy.ma
index d833a5164e2949d119e1ffeb2d4b471b4fbaf6f6..cae93c2560172486e10ba8d11c8c135a1c46098b 100644 (file)
--- a/matita/matita/lib/reverse_complexity/hierarchy.ma
+++ b/matita/matita/lib/reverse_complexity/hierarchy.ma
@@ -6,6 +6,7 @@ include "arithmetics/bounded_quantifiers.ma".
 include "arithmetics/pidgeon_hole.ma". 
 include "basics/sets.ma".
 include "basics/types.ma".
+include "basics/core_notation/card_1.ma".
 
 (************************************ MAX *************************************)
 notation "Max_{ ident i < n | p } f"
@@ -468,4 +469,4 @@ cut (O (λx:ℕ.sU x x (s x)) s) [%{1} %{0} #n //]
   |%{1} %{0} #n #_ >commutative_times <times_n_1
    @monotonic_sU // >size_f_size >size_of_size //
   ]
-qed.
\ No newline at end of file
+qed.