open Preamble

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open List

open Sets

open Deqsets

(** val isnilb : 'a1 List.list -> Bool.bool **)
let rec isnilb = function
| List.Nil -> Bool.True
| List.Cons (hd0, tl) -> Bool.False

(** val memb : Deqsets.deqSet -> __ -> __ List.list -> Bool.bool **)
let rec memb s x = function
| List.Nil -> Bool.False
| List.Cons (a, tl) -> Bool.orb (Deqsets.eqb s x a) (memb s x tl)

(** val uniqueb : Deqsets.deqSet -> __ List.list -> Bool.bool **)
let rec uniqueb s = function
| List.Nil -> Bool.True
| List.Cons (a, tl) -> Bool.andb (Bool.notb (memb s a tl)) (uniqueb s tl)

(** val unique_append :
    Deqsets.deqSet -> __ List.list -> __ List.list -> __ List.list **)
let rec unique_append s l1 l2 =
  match l1 with
  | List.Nil -> l2
  | List.Cons (a, tl) ->
    let r = unique_append s tl l2 in
    (match memb s a r with
     | Bool.True -> r
     | Bool.False -> List.Cons (a, r))

(** val exists : ('a1 -> Bool.bool) -> 'a1 List.list -> Bool.bool **)
let rec exists p = function
| List.Nil -> Bool.False
| List.Cons (h, t) -> Bool.orb (p h) (exists p t)