X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Freverse_complexity%2Fhierarchy.ma;h=cae93c2560172486e10ba8d11c8c135a1c46098b;hb=cd2f5b59215ea771ac137b9a7b115a05175f45d5;hp=d833a5164e2949d119e1ffeb2d4b471b4fbaf6f6;hpb=5b5dca0c118dfbe3ba8f0514ef07549544eb7810;p=helm.git

diff --git a/matita/matita/lib/reverse_complexity/hierarchy.ma b/matita/matita/lib/reverse_complexity/hierarchy.ma
index d833a5164..cae93c256 100644
--- 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.