open Preamble

open CostLabel

open Coqlib

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Positive

open Identifiers

open Exp

open Arithmetic

open Vector

open Div_and_mod

open Util

open FoldStuff

open BitVector

open Jmeq

open Russell

open List

open Setoids

open Monad

open Option

open Extranat

open Bool

open Relations

open Nat

open Integers

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open AST

open Csyntax

open TypeComparison

val ptr_type : Csyntax.type0 -> Nat.nat Types.option -> Csyntax.type0

type classify_add_cases =
| Add_case_ii of AST.intsize * AST.signedness
| Add_case_pi of Nat.nat Types.option * Csyntax.type0 * AST.intsize
   * AST.signedness
| Add_case_ip of Nat.nat Types.option * AST.intsize * AST.signedness
   * Csyntax.type0
| Add_default of Csyntax.type0 * Csyntax.type0

val classify_add_cases_rect_Type4 :
  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
  Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
  (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
  -> classify_add_cases -> 'a1

val classify_add_cases_rect_Type5 :
  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
  Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
  (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
  -> classify_add_cases -> 'a1

val classify_add_cases_rect_Type3 :
  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
  Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
  (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
  -> classify_add_cases -> 'a1

val classify_add_cases_rect_Type2 :
  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
  Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
  (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
  -> classify_add_cases -> 'a1

val classify_add_cases_rect_Type1 :
  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
  Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
  (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
  -> classify_add_cases -> 'a1

val classify_add_cases_rect_Type0 :
  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
  Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
  (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
  -> classify_add_cases -> 'a1

val classify_add_cases_inv_rect_Type4 :
  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
  (Nat.nat Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 ->
  __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> __ -> __ -> __
  -> 'a1) -> 'a1

val classify_add_cases_inv_rect_Type3 :
  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
  (Nat.nat Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 ->
  __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> __ -> __ -> __
  -> 'a1) -> 'a1

val classify_add_cases_inv_rect_Type2 :
  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
  (Nat.nat Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 ->
  __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> __ -> __ -> __
  -> 'a1) -> 'a1

val classify_add_cases_inv_rect_Type1 :
  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
  (Nat.nat Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 ->
  __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> __ -> __ -> __
  -> 'a1) -> 'a1

val classify_add_cases_inv_rect_Type0 :
  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
  (Nat.nat Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 ->
  __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> __ -> __ -> __
  -> 'a1) -> 'a1

val classify_add_cases_discr :
  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> classify_add_cases
  -> __

val classify_add_cases_jmdiscr :
  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> classify_add_cases
  -> __

val classify_add : Csyntax.type0 -> Csyntax.type0 -> classify_add_cases

type classify_sub_cases =
| Sub_case_ii of AST.intsize * AST.signedness
| Sub_case_pi of Nat.nat Types.option * Csyntax.type0 * AST.intsize
   * AST.signedness
| Sub_case_pp of Nat.nat Types.option * Nat.nat Types.option * Csyntax.type0
   * Csyntax.type0
| Sub_default of Csyntax.type0 * Csyntax.type0

val classify_sub_cases_rect_Type4 :
  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
  Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
  'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
  Csyntax.type0 -> classify_sub_cases -> 'a1

val classify_sub_cases_rect_Type5 :
  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
  Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
  'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
  Csyntax.type0 -> classify_sub_cases -> 'a1

val classify_sub_cases_rect_Type3 :
  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
  Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
  'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
  Csyntax.type0 -> classify_sub_cases -> 'a1

val classify_sub_cases_rect_Type2 :
  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
  Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
  'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
  Csyntax.type0 -> classify_sub_cases -> 'a1

val classify_sub_cases_rect_Type1 :
  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
  Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
  'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
  Csyntax.type0 -> classify_sub_cases -> 'a1

val classify_sub_cases_rect_Type0 :
  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
  Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
  'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
  Csyntax.type0 -> classify_sub_cases -> 'a1

val classify_sub_cases_inv_rect_Type4 :
  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
  (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
  -> __ -> __ -> __ -> 'a1) -> 'a1

val classify_sub_cases_inv_rect_Type3 :
  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
  (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
  -> __ -> __ -> __ -> 'a1) -> 'a1

val classify_sub_cases_inv_rect_Type2 :
  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
  (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
  -> __ -> __ -> __ -> 'a1) -> 'a1

val classify_sub_cases_inv_rect_Type1 :
  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
  (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
  -> __ -> __ -> __ -> 'a1) -> 'a1

val classify_sub_cases_inv_rect_Type0 :
  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
  (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
  -> __ -> __ -> __ -> 'a1) -> 'a1

val classify_sub_cases_discr :
  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> classify_sub_cases
  -> __

val classify_sub_cases_jmdiscr :
  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> classify_sub_cases
  -> __

val classify_sub : Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases

type classify_aop_cases =
| Aop_case_ii of AST.intsize * AST.signedness
| Aop_default of Csyntax.type0 * Csyntax.type0

val classify_aop_cases_rect_Type4 :
  (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
  -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1

val classify_aop_cases_rect_Type5 :
  (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
  -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1

val classify_aop_cases_rect_Type3 :
  (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
  -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1

val classify_aop_cases_rect_Type2 :
  (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
  -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1

val classify_aop_cases_rect_Type1 :
  (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
  -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1

val classify_aop_cases_rect_Type0 :
  (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
  -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1

val classify_aop_cases_inv_rect_Type4 :
  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
  -> __ -> __ -> __ -> 'a1) -> 'a1

val classify_aop_cases_inv_rect_Type3 :
  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
  -> __ -> __ -> __ -> 'a1) -> 'a1

val classify_aop_cases_inv_rect_Type2 :
  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
  -> __ -> __ -> __ -> 'a1) -> 'a1

val classify_aop_cases_inv_rect_Type1 :
  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
  -> __ -> __ -> __ -> 'a1) -> 'a1

val classify_aop_cases_inv_rect_Type0 :
  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
  -> __ -> __ -> __ -> 'a1) -> 'a1

val classify_aop_cases_discr :
  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> classify_aop_cases
  -> __

val classify_aop_cases_jmdiscr :
  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> classify_aop_cases
  -> __

val classify_aop : Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases

type classify_cmp_cases =
| Cmp_case_ii of AST.intsize * AST.signedness
| Cmp_case_pp of Nat.nat Types.option * Csyntax.type0
| Cmp_default of Csyntax.type0 * Csyntax.type0

val classify_cmp_cases_rect_Type4 :
  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1

val classify_cmp_cases_rect_Type5 :
  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1

val classify_cmp_cases_rect_Type3 :
  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1

val classify_cmp_cases_rect_Type2 :
  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1

val classify_cmp_cases_rect_Type1 :
  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1

val classify_cmp_cases_rect_Type0 :
  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1

val classify_cmp_cases_inv_rect_Type4 :
  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
  -> __ -> __ -> __ -> 'a1) -> 'a1

val classify_cmp_cases_inv_rect_Type3 :
  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
  -> __ -> __ -> __ -> 'a1) -> 'a1

val classify_cmp_cases_inv_rect_Type2 :
  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
  -> __ -> __ -> __ -> 'a1) -> 'a1

val classify_cmp_cases_inv_rect_Type1 :
  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
  -> __ -> __ -> __ -> 'a1) -> 'a1

val classify_cmp_cases_inv_rect_Type0 :
  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
  -> __ -> __ -> __ -> 'a1) -> 'a1

val classify_cmp_cases_discr :
  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> classify_cmp_cases
  -> __

val classify_cmp_cases_jmdiscr :
  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> classify_cmp_cases
  -> __

val classify_cmp : Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases

type classify_fun_cases =
| Fun_case_f of Csyntax.typelist * Csyntax.type0
| Fun_default

val classify_fun_cases_rect_Type4 :
  (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
  'a1

val classify_fun_cases_rect_Type5 :
  (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
  'a1

val classify_fun_cases_rect_Type3 :
  (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
  'a1

val classify_fun_cases_rect_Type2 :
  (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
  'a1

val classify_fun_cases_rect_Type1 :
  (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
  'a1

val classify_fun_cases_rect_Type0 :
  (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
  'a1

val classify_fun_cases_inv_rect_Type4 :
  classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
  (__ -> 'a1) -> 'a1

val classify_fun_cases_inv_rect_Type3 :
  classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
  (__ -> 'a1) -> 'a1

val classify_fun_cases_inv_rect_Type2 :
  classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
  (__ -> 'a1) -> 'a1

val classify_fun_cases_inv_rect_Type1 :
  classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
  (__ -> 'a1) -> 'a1

val classify_fun_cases_inv_rect_Type0 :
  classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
  (__ -> 'a1) -> 'a1

val classify_fun_cases_discr : classify_fun_cases -> classify_fun_cases -> __

val classify_fun_cases_jmdiscr :
  classify_fun_cases -> classify_fun_cases -> __

val classify_fun : Csyntax.type0 -> classify_fun_cases