25 (** val isnilb : 'a1 List.list -> Bool.bool **)
26 let rec isnilb = function
27 | List.Nil -> Bool.True
28 | List.Cons (hd0, tl) -> Bool.False
30 (** val memb : Deqsets.deqSet -> __ -> __ List.list -> Bool.bool **)
31 let rec memb s x = function
32 | List.Nil -> Bool.False
33 | List.Cons (a, tl) -> Bool.orb (Deqsets.eqb s x a) (memb s x tl)
35 (** val uniqueb : Deqsets.deqSet -> __ List.list -> Bool.bool **)
36 let rec uniqueb s = function
37 | List.Nil -> Bool.True
38 | List.Cons (a, tl) -> Bool.andb (Bool.notb (memb s a tl)) (uniqueb s tl)
40 (** val unique_append :
41 Deqsets.deqSet -> __ List.list -> __ List.list -> __ List.list **)
42 let rec unique_append s l1 l2 =
45 | List.Cons (a, tl) ->
46 let r = unique_append s tl l2 in
47 (match memb s a r with
49 | Bool.False -> List.Cons (a, r))
51 (** val exists : ('a1 -> Bool.bool) -> 'a1 List.list -> Bool.bool **)
52 let rec exists p = function
53 | List.Nil -> Bool.False
54 | List.Cons (h, t) -> Bool.orb (p h) (exists p t)