open Preamble

open Relations

open Bool

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Deqsets

open Sets

open Nat

open List

open Listb

open Div_and_mod

open Jmeq

open Russell

open Util

(** val eqb_elim :
    Deqsets.deqSet -> __ -> __ -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let eqb_elim d x y t f =
  (match Deqsets.eqb d x y with
   | Bool.True -> (fun _ -> t __)
   | Bool.False -> (fun _ -> f __)) __