module My_module = struct

open Pack_concl;;

let concl_list = [GLTVHUM_concl;DUUNHOR_concl;QXSKIIT_concl] ;;

let module_assum = list_mk_conj concl_list;;

(*
frees module_assum;;
type_vars_in_term module_assum;;
*)

axioms();;

let my_assum =  new_definition (mk_eq (`(my_assum:(N#A->bool)) x`,module_assum));;

let my_thm = prove_by_refinement(
  `(my_assum ((@) UNIV)) ==> (!x y z. (x = y) ==> (y =x ))`,
  (* {{{ proof *)
  [
  REPEAT STRIP_TAC;
  ]);;
  (* }}} *)

let INTRO_THEN (axiom,concl) = 
  FIRST_X_ASSUM (MATCH_MP axom


;;
help "MATCH_MP";;
INTRO_TAC (my_assum,GLTVHUM_concl);;

let fold_binop f = function
   [] -> failwith "fold_binop"
  | [a] -> a
  | a::xs -> List.fold_left f a xs;;

let make_assumption name concls = 
  let concl = list_mk_conj concls in
  let _ = (frees concl = []) or (failwith "make_assumption: free vars") in
  let z = type_vars_in_term concl in
  let ty = if (List.length z =0) then `:bool` 
  else
    let f a b = mk_type("prod",[a;b]) in
    let C = fold_binop f z in
     mk_type("fun",[C;`:bool`]) in
  ty;;


mk_type("fun",[`:A`;`:B`]);;
mk_type("prod",[`:A`;`:B`;`:C`]);;
List.fold_left;;
List.fold_right;;
make_assumption "" [`T`];;
concl_list;;
help "mk_type";;
dest_type `:A#B#C`;;
mk_type ("prod",[`:A`;`:B`]);;
help_grep"strip";;
help "mk_list";;
help_grep "mk";;
striplist;;
let GLTVHUM = prove(mk_comb(`GLTVHUM_concl,







end;;