Removed duplicated notation and interaction with the user.

[helm.git] / matita / matita / lib / basics / finset.ma

diff --git a/matita/matita/lib/basics/finset.ma b/matita/matita/lib/basics/finset.ma
index a8ee13a074ad558fbd733c1f2b7718a9d0177c96..85f4ef3ba24264bc6d284c77c5f87518beda2344 100644 (file)
--- a/matita/matita/lib/basics/finset.ma
+++ b/matita/matita/lib/basics/finset.ma
@@ -102,6 +102,8 @@ definition FinSum ≝ λA,B:FinSet.
    (enum_sum A B (enum A) (enum B)) 
    (enumAB_unique … (enum_unique A) (enum_unique B)).
 
+include alias "basics/types.ma".
+
 unification hint  0 ≔ C1,C2; 
     T1 ≟ FinSetcarr C1,
     T2 ≟ FinSetcarr C2,