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