X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fbroken_lib%2Freverse_complexity%2Fhierarchy.ma;h=f288e98cabae096fb1101a37448d7079b0fe7b21;hb=7b256ffa065924e251bef43449401144c35a7e08;hp=a621b55a52a936946b137ec6fb5b45b225dd2267;hpb=d4a074601a61f35ab146a1b97014768683e7ee65;p=helm.git

diff --git a/matita/matita/broken_lib/reverse_complexity/hierarchy.ma b/matita/matita/broken_lib/reverse_complexity/hierarchy.ma
index a621b55a5..f288e98ca 100644
--- a/matita/matita/broken_lib/reverse_complexity/hierarchy.ma
+++ b/matita/matita/broken_lib/reverse_complexity/hierarchy.ma
@@ -46,6 +46,8 @@ lemma Max0r : ∀n. max n 0 = n.
 #n >commutative_max //
 qed.
 
+alias id "max" = "cic:/matita/arithmetics/nat/max#def:2".
+alias id "mk_Aop" = "cic:/matita/arithmetics/bigops/Aop#con:0:1:2".
 definition MaxA ≝ 
   mk_Aop nat 0 max Max0 Max0r (λa,b,c.sym_eq … (Max_assoc a b c)).