open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Relations

open Bool

open Div_and_mod

open Jmeq

open Russell

open Nat

open Types

open List

open Util

(** val if_elim :
    Bool.bool -> 'a1 -> 'a1 -> (__ -> 'a2) -> (__ -> 'a2) -> 'a2 **)
let if_elim clearme e1 e2 x x0 =
  (match clearme with
   | Bool.True -> (fun e3 e4 _ auto auto' -> auto __)
   | Bool.False -> (fun e3 e4 _ auto auto' -> auto' __)) e1 e2 __ x x0