]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/library/Fsub/util.ma
Much ado about nothing:
[helm.git] / helm / software / matita / library / Fsub / util.ma
index 8b111e3f2425637f1fc75086a96265cb78ff6db7..582114c690a60afb840fa51b0eaaac2801c899ea 100644 (file)
@@ -35,7 +35,7 @@ let rec max m n \def
      [true \Rightarrow n
      |false \Rightarrow m]. 
 
-inductive in_list (A : Set) : A \to (list A) \to Prop \def
+inductive in_list (A : Type) : A \to (list A) \to Prop \def
   | in_Base : \forall x:A.\forall l:(list A).
               (in_list A x (x :: l))
   | in_Skip : \forall x,y:A.\forall l:(list A).