needs "Examples/ssrnat-compiled.hl";;

(* Module Hypermap_iso*)
module Hypermap_iso = struct

let hyp_iso = new_definition `hyp_iso f (H, G) <=>
                           BIJ f (dart H) (dart G) /\
                        (!x. x IN dart H ==>
                        edge_map G (f x) = f (edge_map H x) /\
                               node_map G (f x) = f (node_map H x) /\
                           face_map G (f x) = f (face_map H x))`;;
let res_inv = new_definition `res_inv f s = (\y. @x. f x = y /\ x IN s)`;;
open Ssrfun;;
open Ssrbool;;
open Ssrnat;;
open Fan;;
open Hypermap;;
open Fan_defs;;
open Hypermap_and_fan;;
parse_as_infix("iso",(24,"right"));;
let inE = CONJUNCT2 IN_ELIM_THM;;
let IN_TRANS = 
prove(`!(x:A) s t. t SUBSET s /\ x IN t ==> x IN s`,
 SET_TAC[]);;
(* Lemma bij_disjoint_union *)
let bij_disjoint_union = Sections.section_proof ["f";"g";"s";"t";"s'";"t'"]
`DISJOINT s t /\ DISJOINT s' t' /\ BIJ (f:A->B) s s' /\ BIJ (g:A->B) t t'
                ==> BIJ (\x. if x IN s then f x else g x) (s UNION t) (s' UNION t')`
[
   ((repeat_tactic 1 9 (((use_arg_then2 ("DISJOINT", [DISJOINT]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("SURJ", [SURJ]))(thm_tac (new_rewrite [] []))))));
   (BETA_TAC THEN (case THEN (move ["d_st"])) THEN (case THEN (move ["d_s't'"])) THEN (case THEN ALL_TAC) THEN (case THEN ALL_TAC) THEN (case THEN ((move ["fx"]) THEN (move ["f_inj"]))) THEN (case THEN ((move ["_"]) THEN (move ["f_surj"]))) THEN (case THEN ALL_TAC) THEN (case THEN ((move ["gx"]) THEN (move ["g_inj"]))) THEN (case THEN ((move ["_"]) THEN (move ["g_surj"]))));
   ((fun arg_tac -> arg_tac (Arg_term (`x IN t ==> ~(x IN s)`))) (term_tac (have_gen_tac ["x"](move ["x_in_t"]))));
   ((BETA_TAC THEN (move ["xt"])) THEN (((use_arg_then2 ("d_st", [])) (disch_tac [])) THEN (clear_assumption "d_st") THEN ((use_arg_then2 ("contraL", [contraL])) (disch_tac [])) THEN (clear_assumption "contraL") THEN (DISCH_THEN apply_tac) THEN (move ["xs"])));
   (((((use_arg_then2 ("MEMBER_NOT_EMPTY", [MEMBER_NOT_EMPTY]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN (done_tac));
   ((repeat_tactic 1 9 (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 ((split_tac))));
   ((THENL_FIRST) (BETA_TAC THEN (move ["x"]) THEN (case THEN (move ["x_in"]))) (((((use_arg_then2 ("x_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("fx", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
   (((((fun arg_tac -> (use_arg_then2 ("x_in_t", [])) (fun fst_arg -> (use_arg_then2 ("x_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("gx", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((BETA_TAC THEN (move ["x"]) THEN (move ["y"]) THEN (case THEN ALL_TAC) THEN (case THEN (move ["x_in"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["y_in"]))) THEN (((repeat_tactic 0 10 (((use_arg_then2 ("x_in", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("y_in", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("x_in_t", []))(thm_tac (new_rewrite [] []))))) THEN ((simp_tac THEN TRY done_tac))) THEN (move ["eq"])));
   ((((fun arg_tac -> (use_arg_then2 ("f_inj", [])) (fun fst_arg -> (use_arg_then2 ("eq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
   ((((use_arg_then2 ("d_s't'", [])) (disch_tac [])) THEN (clear_assumption "d_s't'") THEN ((use_arg_then2 ("contraLR", [contraLR])) (disch_tac [])) THEN (clear_assumption "contraLR") THEN (DISCH_THEN apply_tac) THEN (move ["_"])) THEN (((use_arg_then2 ("MEMBER_NOT_EMPTY", [MEMBER_NOT_EMPTY]))(gsym_then (thm_tac (new_rewrite [] []))))));
   (((fun arg_tac -> arg_tac (Arg_term (`f x`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fx", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("gx", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((((use_arg_then2 ("d_s't'", [])) (disch_tac [])) THEN (clear_assumption "d_s't'") THEN ((use_arg_then2 ("contraLR", [contraLR])) (disch_tac [])) THEN (clear_assumption "contraLR") THEN (DISCH_THEN apply_tac) THEN (move ["_"])) THEN (((use_arg_then2 ("MEMBER_NOT_EMPTY", [MEMBER_NOT_EMPTY]))(gsym_then (thm_tac (new_rewrite [] []))))));
   (((fun arg_tac -> arg_tac (Arg_term (`g x`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("gx", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fx", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((((fun arg_tac -> (use_arg_then2 ("g_inj", [])) (fun fst_arg -> (use_arg_then2 ("eq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
   ((THENL_FIRST) (BETA_TAC THEN (move ["x"]) THEN (case THEN (move ["x_in"]))) (((((use_arg_then2 ("x_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("fx", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
   (((((fun arg_tac -> (use_arg_then2 ("x_in_t", [])) (fun fst_arg -> (use_arg_then2 ("x_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("gx", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (BETA_TAC THEN (move ["x"]) THEN (case THEN (move ["x_in"])));
   (((fun arg_tac -> (use_arg_then2 ("f_surj", [])) (fun fst_arg -> (use_arg_then2 ("x_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (case THEN (move ["y"])) THEN (case THEN ((move ["ys"]) THEN (move ["fy_eq"]))));
   (((use_arg_then2 ("y", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("ys", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
   (((fun arg_tac -> (use_arg_then2 ("g_surj", [])) (fun fst_arg -> (use_arg_then2 ("x_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (case THEN (move ["y"])) THEN (case THEN ((move ["yt"]) THEN (move ["gy_eq"]))));
   (((use_arg_then2 ("y", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("yt", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("x_in_t", [])) (fun fst_arg -> (use_arg_then2 ("yt", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma disjoint_diff *)
let disjoint_diff = Sections.section_proof ["s";"t"]
`DISJOINT s (t DIFF s)`
[
   (((((use_arg_then2 ("DISJOINT", [DISJOINT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] []))))) THEN (move ["x"]));
   ((((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_DIFF", [IN_DIFF]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("NOT_IN_EMPTY", [NOT_IN_EMPTY]))(thm_tac (new_rewrite [] [])))));
   (((((use_arg_then2 ("andbA", [andbA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbAC", [andbAC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbN", [andbN]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andFb", [andFb]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma image_lemma *)
let image_lemma = Sections.section_proof ["f";"P"]
`IMAGE f {x | P x} = {f x | P x}`
[
   (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("andbC", [andbC]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Section PowerOrbit *)
Sections.begin_section "PowerOrbit";;
(Sections.add_section_var (mk_var ("f", (`:A -> B`))));;
(Sections.add_section_var (mk_var ("g1", (`:A -> A`))));;
(Sections.add_section_var (mk_var ("g2", (`:B -> B`))));;
(Sections.add_section_var (mk_var ("s", (`:A -> bool`))));;
(Sections.add_section_hyp "g1s" (`!x. x IN s ==> g1 x IN s`));;

(* Lemma power_in *)
let power_in = Sections.section_proof ["x";"n"]
`x IN s ==> (g1 POWER n) x IN s`
[
   ((THENL_FIRST) ((BETA_TAC THEN (move ["xs"])) THEN ((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; ((move ["n"]) THEN (move ["Ih"]))])) (((((use_arg_then2 ("POWER_0", [POWER_0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("I_THM", [I_THM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
   (((((use_arg_then2 ("COM_POWER", [COM_POWER]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("g1s", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;
(Sections.add_section_hyp "fg" (`!x. x IN s ==> f (g1 x) = g2 (f x)`));;

(* Lemma power_comm *)
let power_comm = Sections.section_proof ["x";"n"]
`x IN s ==> f ((g1 POWER n) x) = (g2 POWER n) (f x)`
[
   ((THENL_FIRST) ((BETA_TAC THEN (move ["xs"])) THEN ((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; ((move ["n"]) THEN (move ["Ih"]))])) (((repeat_tactic 1 9 (((use_arg_then2 ("POWER_0", [POWER_0]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("I_THM", [I_THM]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac)));
   (((repeat_tactic 1 9 (((use_arg_then2 ("COM_POWER", [COM_POWER]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("fg", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("power_in", [power_in]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Lemma orbit_comm *)
let orbit_comm = Sections.section_proof ["x"]
`x IN s ==> orbit_map g2 (f x) = IMAGE f (orbit_map g1 x)`
[
   (((repeat_tactic 1 9 (((use_arg_then2 ("orbit_map", [orbit_map]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["xs"]) THEN (move ["x"]));
   ((THENL) (split_tac) [((case THEN (move ["n"])) THEN (move ["h"])); ((case THEN (move ["y"])) THEN (case THEN (move ["x_eq"])) THEN (case THEN (move ["n"])) THEN (move ["h"]))]);
   ((fun arg_tac -> arg_tac (Arg_term (`(g1 POWER n) x`))) (term_tac exists_tac));
   (((((use_arg_then2 ("power_comm", [power_comm]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ((use_arg_then2 ("n", [])) (term_tac exists_tac)) THEN (done_tac));
   (((use_arg_then2 ("n", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("x_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("power_comm", [power_comm]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Finalization of the section PowerOrbit *)
let power_in = Sections.finalize_theorem power_in;;
let power_comm = Sections.finalize_theorem power_comm;;
let orbit_comm = Sections.finalize_theorem orbit_comm;;
Sections.end_section "PowerOrbit";;

(* Lemma image_ext_eq *)
let image_ext_eq = Sections.section_proof ["f";"g";"s"]
`(!x. x IN s ==> f x = g x) ==> IMAGE f s = IMAGE g s`
[
   ((BETA_TAC THEN (move ["eq"])) THEN (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))))) THEN (move ["y"])));
   (((split_tac) THEN ALL_TAC THEN (case THEN (move ["x"])) THEN (case THEN (move ["y_eq"])) THEN (move ["xs"])) THEN ((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("y_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma image_res *)
let image_res = Sections.section_proof ["f";"s";"u"]
`s SUBSET u ==> IMAGE f s = IMAGE (res f u) s`
[
   (((((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (move ["su"])) THEN (((use_arg_then2 ("image_ext_eq", [image_ext_eq])) (thm_tac apply_tac)) THEN (move ["x"]) THEN (move ["xs"])));
   (((((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("su", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma im_in_image *)
let im_in_image = Sections.section_proof ["f";"s";"x"]
`f x IN IMAGE f s <=> x IN s \/ ?y. y IN s /\ ~(x = y) /\ f x = f y`
[
   ((((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN ((THENL) (split_tac) [((case THEN (move ["y"])) THEN (move ["h"])); ALL_TAC]));
   (((fun arg_tac -> arg_tac (Arg_term (`x IN s`))) (disch_eq_tac "x_in" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
   (((use_arg_then2 ("y", [])) (term_tac exists_tac)) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)));
   ((((use_arg_then2 ("x_in", [])) (disch_tac [])) THEN (clear_assumption "x_in") THEN ((use_arg_then2 ("contra", [contra])) (disch_tac [])) THEN (clear_assumption "contra") THEN (DISCH_THEN apply_tac) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (((THENL) (BETA_TAC THEN ((THENL) case [(move ["x_in"]); ((case THEN (move ["y"])) THEN (move ["h"]))])) [((use_arg_then2 ("x", [])) (term_tac exists_tac)); ((use_arg_then2 ("y", [])) (term_tac exists_tac))]) THEN (done_tac));
];;

(* Section InjProps *)
Sections.begin_section "InjProps";;
(Sections.add_section_var (mk_var ("u", (`:A -> bool`))));;
(Sections.add_section_var (mk_var ("f", (`:A -> B`))));;
(Sections.add_section_hyp "inj" (`!x y. x IN u /\ y IN u /\ f x = f y ==> x = y`));;

(* Lemma image_inter_inj_gen *)
let image_inter_inj_gen = Sections.section_proof ["s";"t"]
`s SUBSET u /\ t SUBSET u
        ==> IMAGE f (s INTER t) = IMAGE f s INTER IMAGE f t`
[
   ((repeat_tactic 1 9 (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((move ["su"]) THEN (move ["tu"]))));
   (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] []))))) THEN (move ["y"]));
   ((THENL) (split_tac) [((case THEN (move ["x"])) THEN (case THEN (move ["y_eq"])) THEN (case THEN ((move ["xs"]) THEN (move ["xt"])))); ((case THEN ALL_TAC) THEN (case THEN (move ["x"])) THEN (case THEN ((move ["y_eq"]) THEN (move ["xs"]))) THEN (case THEN (move ["x'"])) THEN (case THEN ((move ["y_eq'"]) THEN (move ["x't"]))))]);
   ((split_tac) THEN ((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN (done_tac));
   (((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN (repeat_tactic 1 9 (((split_tac) THEN ((TRY done_tac))))));
   (((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("inj", [])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("su", [])) (fun fst_arg -> (use_arg_then2 ("xs", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("tu", [])) (fun fst_arg -> (use_arg_then2 ("x't", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("y_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("y_eq'", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Lemma image_inj_gen *)
let image_inj_gen = Sections.section_proof ["s";"t"]
`s SUBSET u /\ t SUBSET u /\ IMAGE f s = IMAGE f t
        ==> s = t`
[
   ((((repeat_tactic 1 9 (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))))) THEN ALL_TAC THEN (case THEN (move ["su"])) THEN (case THEN (move ["tu"])) THEN (move ["eq"]) THEN (move ["y"])) THEN ((split_tac) THEN (move ["y_in"])));
   ((THENL_FIRST) ((((fun arg_tac -> (use_arg_then2 ("iffLR", [iffLR])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("eq", [])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`f y`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (ANTS_TAC)) (((use_arg_then2 ("y", [])) (term_tac exists_tac)) THEN (done_tac)));
   (BETA_TAC THEN (case THEN (move ["x"])) THEN (case THEN (move ["f_eq"])) THEN (move ["xt"]));
   ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("inj", [])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("su", [])) (fun fst_arg -> (use_arg_then2 ("y_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("tu", [])) (fun fst_arg -> (use_arg_then2 ("xt", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
   ((THENL_FIRST) ((((fun arg_tac -> (use_arg_then2 ("iffRL", [iffRL])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("eq", [])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`f y`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (ANTS_TAC)) (((use_arg_then2 ("y", [])) (term_tac exists_tac)) THEN (done_tac)));
   (BETA_TAC THEN (case THEN (move ["x"])) THEN (case THEN (move ["f_eq"])) THEN (move ["xs"]));
   ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("inj", [])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("tu", [])) (fun fst_arg -> (use_arg_then2 ("y_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("su", [])) (fun fst_arg -> (use_arg_then2 ("xs", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma image_set_inj_gen *)
let image_set_inj_gen = Sections.section_proof ["s";"t"]
`s SUBSET u /\ t SUBSET u /\ IMAGE f s = IMAGE f t ==> s = t`
[
   ((((repeat_tactic 1 9 (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))))) THEN ALL_TAC THEN (case THEN (move ["su"])) THEN (case THEN (move ["tu"])) THEN (move ["i_eq"]) THEN (move ["x"])) THEN ((split_tac) THEN (move ["x_in"])));
   ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`f x IN IMAGE f s`))) (term_tac (have_gen_tac []ALL_TAC))) ((((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN ((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN (done_tac)));
   (((((use_arg_then2 ("i_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("im_in_image", [im_in_image]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN ((TRY done_tac)) THEN (case THEN (move ["y"])) THEN (case THEN (move ["y_in"])) THEN (case THEN (move ["neq"])) THEN (move ["f_eq"]));
   ((((use_arg_then2 ("neq", [])) (disch_tac [])) THEN (clear_assumption "neq") THEN ((use_arg_then2 ("contraR", [contraR])) (disch_tac [])) THEN (clear_assumption "contraR") THEN (DISCH_THEN apply_tac) THEN (move ["_"])) THEN (((use_arg_then2 ("inj", [])) (disch_tac [])) THEN (clear_assumption "inj") THEN (DISCH_THEN apply_tac)));
   (((((fun arg_tac -> (use_arg_then2 ("su", [])) (fun fst_arg -> (use_arg_then2 ("x_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("tu", [])) (fun fst_arg -> (use_arg_then2 ("y_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`f x IN IMAGE f t`))) (term_tac (have_gen_tac []ALL_TAC))) ((((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN ((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN (done_tac)));
   (((((use_arg_then2 ("i_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("im_in_image", [im_in_image]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN ((TRY done_tac)) THEN (case THEN (move ["y"])) THEN (case THEN (move ["y_in"])) THEN (case THEN (move ["neq"])) THEN (move ["f_eq"]));
   ((((use_arg_then2 ("neq", [])) (disch_tac [])) THEN (clear_assumption "neq") THEN ((use_arg_then2 ("contraR", [contraR])) (disch_tac [])) THEN (clear_assumption "contraR") THEN (DISCH_THEN apply_tac) THEN (move ["_"])) THEN (((use_arg_then2 ("inj", [])) (disch_tac [])) THEN (clear_assumption "inj") THEN (DISCH_THEN apply_tac)));
   (((((fun arg_tac -> (use_arg_then2 ("su", [])) (fun fst_arg -> (use_arg_then2 ("y_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("tu", [])) (fun fst_arg -> (use_arg_then2 ("x_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Finalization of the section InjProps *)
let image_inter_inj_gen = Sections.finalize_theorem image_inter_inj_gen;;
let image_inj_gen = Sections.finalize_theorem image_inj_gen;;
let image_set_inj_gen = Sections.finalize_theorem image_set_inj_gen;;
Sections.end_section "InjProps";;

(* Section FiniteBijections *)
Sections.begin_section "FiniteBijections";;
(Sections.add_section_var (mk_var ("s", (`:A->bool`))));;
(Sections.add_section_var (mk_var ("t", (`:B->bool`))));;

(* Lemma permutes_imp_bij *)
let permutes_imp_bij = Sections.section_proof ["p"]
`p permutes s ==> BIJ p s s`
[
   ((BETA_TAC THEN (move ["perm"])) THEN ((((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SURJ", [SURJ]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("PERMUTES_IN_IMAGE", [PERMUTES_IN_IMAGE])) (fun fst_arg -> (use_arg_then2 ("perm", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)));
   ((THENL_FIRST) ((THENL) (split_tac) [((move ["x"]) THEN (move ["y"]) THEN (case THEN (move ["xs"])) THEN (case THEN (move ["ys"])) THEN (move ["p_eq"])); ((move ["x"]) THEN (move ["xs"]))]) ((((fun arg_tac -> (use_arg_then2 ("PERMUTES_INJECTIVE", [PERMUTES_INJECTIVE])) (fun fst_arg -> (use_arg_then2 ("perm", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac)));
   ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PERMUTES_SURJECTIVE", [PERMUTES_SURJECTIVE])) (fun fst_arg -> (use_arg_then2 ("perm", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (case THEN (move ["y"])) THEN (move ["p_eq"])) THEN ((use_arg_then2 ("y", [])) (term_tac exists_tac)) THEN ((split_tac) THEN ((TRY done_tac))));
   (((((fun arg_tac -> (use_arg_then2 ("PERMUTES_IN_IMAGE", [PERMUTES_IN_IMAGE])) (fun fst_arg -> (use_arg_then2 ("perm", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("p_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma surj_image *)
let surj_image = Sections.section_proof ["f"]
`SURJ f s t ==> IMAGE f s = t`
[
   (((((use_arg_then2 ("SURJ", [SURJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((move ["f_in"]) THEN (move ["surj"]))) THEN (move ["y"]));
   (((THENL) ((THENL) (split_tac) [((case THEN (move ["x"])) THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (move ["xs"])); ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("surj", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (case THEN (move ["x"])) THEN (case THEN ((move ["xs"]) THEN (move ["eq"]))))]) [(((use_arg_then2 ("f_in", [])) (disch_tac [])) THEN (clear_assumption "f_in") THEN (exact_tac)); ((use_arg_then2 ("x", [])) (term_tac exists_tac))]) THEN (done_tac));
];;

(* Lemma surj_imp_finite *)
let surj_imp_finite = Sections.section_proof ["f"]
`FINITE s /\ SURJ f s t ==> FINITE t`
[
   ((BETA_TAC THEN (case THEN (move ["fin_s"])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("surj_image", [surj_image])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((use_arg_then2 ("FINITE_IMAGE", [FINITE_IMAGE])) (thm_tac apply_tac)) THEN (done_tac));
];;

(* Lemma inj_imp_finite *)
let inj_imp_finite = Sections.section_proof ["f"]
`FINITE t /\ INJ f s t ==> FINITE s`
[
   ((((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["fin_t"])) THEN (case THEN (move ["f_in"])) THEN (move ["inj"]));
   ((((fun arg_tac -> (use_arg_then2 ("FINITE_IMAGE_INJ_EQ", [FINITE_IMAGE_INJ_EQ])) (fun fst_arg -> (use_arg_then2 ("inj", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("FINITE_SUBSET", [FINITE_SUBSET])) (fun fst_arg -> (use_arg_then2 ("fin_t", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))));
   ((BETA_TAC THEN (move ["y"]) THEN (case THEN (move ["x"])) THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (move ["xs"])) THEN (((use_arg_then2 ("f_in", [])) (disch_tac [])) THEN (clear_assumption "f_in") THEN (exact_tac)) THEN (done_tac));
];;

(* Lemma bij_finite_eq *)
let bij_finite_eq = Sections.section_proof ["f"]
`BIJ f s t ==> (FINITE s <=> FINITE t)`
[
   (((((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] [])))) THEN (move ["bij"])) THEN ((THENL) (split_tac) [(move ["fin_s"]); (move ["fin_t"])]));
   ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("surj_imp_finite", [surj_imp_finite])) (fun fst_arg -> (use_arg_then2 ("fin_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
   ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("inj_imp_finite", [inj_imp_finite])) (fun fst_arg -> (use_arg_then2 ("fin_t", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma surj_imp_card_le *)
let surj_imp_card_le = Sections.section_proof ["f"]
`FINITE s /\ SURJ f s t ==> CARD t <= CARD s`
[
   ((BETA_TAC THEN (case THEN (move ["fin_s"])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("surj_image", [surj_image])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((use_arg_then2 ("CARD_IMAGE_LE", [CARD_IMAGE_LE])) (thm_tac apply_tac)) THEN (done_tac));
];;

(* Lemma inj_imp_card_le *)
let inj_imp_card_le = Sections.section_proof ["f"]
`FINITE t /\ INJ f s t ==> CARD s <= CARD t`
[
   ((BETA_TAC THEN (case THEN (move ["fin_t"])) THEN (move ["inj"])) THEN (((use_arg_then2 ("inj", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["f_in"])) THEN (move ["inj2"])));
   ((((fun arg_tac -> (use_arg_then2 ("CARD_IMAGE_INJ", [CARD_IMAGE_INJ])) (fun fst_arg -> (use_arg_then2 ("inj2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("inj_imp_finite", [inj_imp_finite])) (fun fst_arg -> (use_arg_then2 ("inj", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
   ((((((use_arg_then2 ("CARD_SUBSET", [CARD_SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fin_t", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] []))))) THEN (move ["y"]) THEN (case THEN (move ["x"])) THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (move ["xs"])) THEN (((use_arg_then2 ("f_in", [])) (disch_tac [])) THEN (clear_assumption "f_in") THEN (exact_tac)) THEN (done_tac));
];;

(* Lemma bij_card_eq *)
let bij_card_eq = Sections.section_proof ["f"]
`BIJ f s t /\ FINITE s ==> CARD t = CARD s`
[
   (((((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN ((move ["inj"]) THEN (move ["surj"]))) THEN (move ["fin_s"])) THEN (((use_arg_then2 ("anti_leq", [anti_leq])) (disch_tac [])) THEN (clear_assumption "anti_leq") THEN (DISCH_THEN apply_tac)));
   (((((fun arg_tac -> (use_arg_then2 ("surj_imp_card_le", [surj_imp_card_le])) (fun fst_arg -> (use_arg_then2 ("surj", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("inj_imp_card_le", [inj_imp_card_le])) (fun fst_arg -> (use_arg_then2 ("inj", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("surj_imp_finite", [surj_imp_finite])) (fun fst_arg -> (use_arg_then2 ("surj", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;
(Sections.add_section_hyp "fin_s" (`FINITE s`));;
(Sections.add_section_hyp "fin_t" (`FINITE t`));;
(Sections.add_section_hyp "card_eq" (`CARD s = CARD t`));;

(* Lemma finite_inj_eq_surj *)
let finite_inj_eq_surj = Sections.section_proof ["f"]
`INJ f s t <=> SURJ f s t`
[
   (((((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SURJ", [SURJ]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("andb_id2l", [andb_id2l])) (disch_tac [])) THEN (clear_assumption "andb_id2l") THEN (DISCH_THEN apply_tac) THEN (move ["f_in"])));
   ((((use_arg_then2 ("SURJECTIVE_IFF_INJECTIVE_GEN", [SURJECTIVE_IFF_INJECTIVE_GEN]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("fin_s", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fin_t", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("card_eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
   ((((((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] []))))) THEN (move ["y"]) THEN (case THEN (move ["x"])) THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (move ["xs"])) THEN (((use_arg_then2 ("f_in", [])) (disch_tac [])) THEN (clear_assumption "f_in") THEN (exact_tac)) THEN (done_tac));
];;

(* Lemma finite_inj_eq_bij *)
let finite_inj_eq_bij = Sections.section_proof ["f"]
`INJ f s t <=> BIJ f s t`
[
   (((((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("finite_inj_eq_surj", [finite_inj_eq_surj]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbb", [andbb]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma finite_surj_eq_bij *)
let finite_surj_eq_bij = Sections.section_proof ["f"]
`SURJ f s t <=> BIJ f s t`
[
   (((((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("finite_inj_eq_surj", [finite_inj_eq_surj]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbb", [andbb]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Finalization of the section FiniteBijections *)
let permutes_imp_bij = Sections.finalize_theorem permutes_imp_bij;;
let surj_image = Sections.finalize_theorem surj_image;;
let surj_imp_finite = Sections.finalize_theorem surj_imp_finite;;
let inj_imp_finite = Sections.finalize_theorem inj_imp_finite;;
let bij_finite_eq = Sections.finalize_theorem bij_finite_eq;;
let surj_imp_card_le = Sections.finalize_theorem surj_imp_card_le;;
let inj_imp_card_le = Sections.finalize_theorem inj_imp_card_le;;
let bij_card_eq = Sections.finalize_theorem bij_card_eq;;
let finite_inj_eq_surj = Sections.finalize_theorem finite_inj_eq_surj;;
let finite_inj_eq_bij = Sections.finalize_theorem finite_inj_eq_bij;;
let finite_surj_eq_bij = Sections.finalize_theorem finite_surj_eq_bij;;
Sections.end_section "FiniteBijections";;

(* Section ResInverse *)
Sections.begin_section "ResInverse";;

(* Lemma bij_alt *)
let bij_alt = Sections.section_proof ["f";"s";"t"]
`BIJ f s t <=>
        (!x. x IN s ==> f x IN t) /\
        (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) /\
        (!y. y IN t ==> ?x. x IN s /\ f x = y)`
[
   (((((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SURJ", [SURJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbAC", [andbAC]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andbA", [andbA]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("andbb", [andbb]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbAC", [andbAC]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Section Ext *)
Sections.begin_section "Ext";;
(Sections.add_section_var (mk_var ("f", (`:A->B`))); Sections.add_section_var (mk_var ("g", (`:A->B`))));;
(Sections.add_section_var (mk_var ("s", (`:A->bool`))));;
(Sections.add_section_var (mk_var ("t", (`:B->bool`))));;
(Sections.add_section_hyp "ext" (`!x. x IN s ==> f x = g x`));;

(* Lemma inj_ext *)
let inj_ext = Sections.section_proof []
`INJ f s t ==> INJ g s t`
[
   (((repeat_tactic 1 9 (((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((move ["f_in"]) THEN (move ["f_inj"])))) THEN ((THENL) (split_tac) [((move ["x"]) THEN (move ["xs"])); ((move ["x"]) THEN (move ["y"]) THEN (move ["h"]))]));
   (((((use_arg_then2 ("ext", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_in", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((((use_arg_then2 ("f_inj", [])) (disch_tac [])) THEN (clear_assumption "f_inj") THEN (DISCH_THEN apply_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("ext", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma surj_ext *)
let surj_ext = Sections.section_proof []
`SURJ f s t ==> SURJ g s t`
[
   (((repeat_tactic 1 9 (((use_arg_then2 ("SURJ", [SURJ]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((move ["f_in"]) THEN (move ["f_surj"])))) THEN ((THENL) (split_tac) [((move ["x"]) THEN (move ["xs"])); ((move ["x"]) THEN (move ["xt"]))]));
   (((((use_arg_then2 ("ext", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_in", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (((fun arg_tac -> (use_arg_then2 ("f_surj", [])) (fun fst_arg -> (use_arg_then2 ("xt", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (case THEN (move ["y"])) THEN (case THEN ((move ["ys"]) THEN (move ["eq"]))));
   (((use_arg_then2 ("y", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("ext", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma bij_ext *)
let bij_ext = Sections.section_proof []
`BIJ f s t ==> BIJ g s t`
[
   (((THENL) (((repeat_tactic 1 9 (((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] []))))) THEN (move ["h"])) THEN (split_tac)) [(((use_arg_then2 ("inj_ext", [inj_ext])) (disch_tac [])) THEN (clear_assumption "inj_ext") THEN (exact_tac)); (((use_arg_then2 ("surj_ext", [surj_ext])) (disch_tac [])) THEN (clear_assumption "surj_ext") THEN (exact_tac))]) THEN (done_tac));
];;

(* Finalization of the section Ext *)
let inj_ext = Sections.finalize_theorem inj_ext;;
let surj_ext = Sections.finalize_theorem surj_ext;;
let bij_ext = Sections.finalize_theorem bij_ext;;
Sections.end_section "Ext";;

(* Lemma res_inv_left *)
let res_inv_left = Sections.section_proof ["f";"s";"x"]
`(!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) /\ x IN s
        ==> res_inv f s (f x) = x`
[
   (((((use_arg_then2 ("res_inv", [res_inv]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN ((move ["inj"]) THEN (move ["xs"]))));
   ((((use_arg_then2 ("SELECT_UNIQUE", [SELECT_UNIQUE])) (thm_tac apply_tac)) THEN (simp_tac) THEN (move ["y"])) THEN ((THENL) (split_tac) [(case THEN ((move ["f_eq"]) THEN (move ["ys"]))); ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)))]));
   ((((fun arg_tac -> (use_arg_then2 ("inj", [])) (fun fst_arg -> (use_arg_then2 ("f_eq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma res_inv_right *)
let res_inv_right = Sections.section_proof ["f";"s";"t";"y"]
`(!y. y IN t ==> ?x. x IN s /\ f x = y) /\ y IN t
        ==> f (res_inv f s y) = y /\ res_inv f s y IN s`
[
   (((((use_arg_then2 ("res_inv", [res_inv]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["surj"])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("surj", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (case THEN (move ["x"])) THEN (move ["h"]));
   ((fun arg_tac -> (use_arg_then2 ("SELECT_AX", [SELECT_AX])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`\x. f x = y /\ x IN s`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (simp_tac)));
   ((DISCH_THEN apply_tac) THEN ((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN (done_tac));
];;

(* Lemma res_inv_bij *)
let res_inv_bij = Sections.section_proof ["f";"s";"t"]
`BIJ f s t ==>
        (!x. x IN s ==> res_inv f s (f x) = x) /\
        (!y. y IN t ==> f (res_inv f s y) = y) /\
        (!y. y IN t ==> res_inv f s y IN s)`
[
   (((((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SURJ", [SURJ]))(thm_tac (new_rewrite [] []))))) THEN (move ["h"]));
   (((THENL_FIRST) ((repeat_tactic 1 9 ((split_tac))) THEN (BETA_TAC THEN (move ["a"]) THEN (move ["a_in"]))) ((use_arg_then2 ("res_inv_left", [res_inv_left])) (thm_tac apply_tac))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("res_inv_right", [res_inv_right])) (fun fst_arg -> (use_arg_then2 ("f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("t", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma bij_res_inv *)
let bij_res_inv = Sections.section_proof ["f";"s";"t"]
`BIJ f s t ==> BIJ (res_inv f s) t s`
[
   ((repeat_tactic 1 9 (((use_arg_then2 ("bij_alt", [bij_alt]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["f_in"])) THEN (case THEN ((move ["inj"]) THEN (move ["surj"]))));
   ((THENL_FIRST) ((THENL) (split_tac) [((move ["x"]) THEN (move ["xt"])); ALL_TAC]) ((((fun arg_tac -> (use_arg_then2 ("res_inv_right", [res_inv_right])) (fun fst_arg -> (use_arg_then2 ("surj", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
   ((THENL_ROT (-1)) ((THENL) (split_tac) [((move ["x"]) THEN (move ["y"]) THEN (case THEN (move ["xt"])) THEN (case THEN (move ["yt"])) THEN (move ["inv_eq"])); ((move ["x"]) THEN (move ["xs"]))]));
   (((fun arg_tac -> arg_tac (Arg_term (`f x`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("f_in", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("res_inv_left", [res_inv_left]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("congr1", [congr1])) (fun fst_arg -> (use_arg_then2 ("f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("inv_eq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC);
   ((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("res_inv_right", [res_inv_right])) (fun fst_arg -> (use_arg_then2 ("surj", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma inj_res_inv_left *)
let inj_res_inv_left = Sections.section_proof ["f";"s";"t";"x"]
`INJ f s t /\ x IN s ==> res_inv f s (f x) = x`
[
   (((((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (move ["h"])) THEN ((((use_arg_then2 ("res_inv_left", [res_inv_left]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (done_tac));
];;

(* Lemma surj_res_inv_right *)
let surj_res_inv_right = Sections.section_proof ["f";"s";"t";"y"]
`SURJ f s t /\ y IN t ==>
	f (res_inv f s y) = y /\ res_inv f s y IN s`
[
   (((((use_arg_then2 ("SURJ", [SURJ]))(thm_tac (new_rewrite [] [])))) THEN (move ["h"])) THEN ((repeat_tactic 1 9 (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("res_inv_right", [res_inv_right])) (fun fst_arg -> (use_arg_then2 ("f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("t", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (done_tac));
];;

(* Finalization of the section ResInverse *)
let bij_alt = Sections.finalize_theorem bij_alt;;
let inj_ext = Sections.finalize_theorem inj_ext;;
let surj_ext = Sections.finalize_theorem surj_ext;;
let bij_ext = Sections.finalize_theorem bij_ext;;
let res_inv_left = Sections.finalize_theorem res_inv_left;;
let res_inv_right = Sections.finalize_theorem res_inv_right;;
let res_inv_bij = Sections.finalize_theorem res_inv_bij;;
let bij_res_inv = Sections.finalize_theorem bij_res_inv;;
let inj_res_inv_left = Sections.finalize_theorem inj_res_inv_left;;
let surj_res_inv_right = Sections.finalize_theorem surj_res_inv_right;;
Sections.end_section "ResInverse";;

(* Section Iso *)
Sections.begin_section "Iso";;

(* Lemma hyp_iso_imp_iso *)
let hyp_iso_imp_iso = Sections.section_proof ["H";"G";"f"]
`hyp_iso f (H, G) ==> H iso G`
[
   ((((((use_arg_then2 ("hyp_iso", [hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("iso", [iso]))(thm_tac (new_rewrite [] []))))) THEN (move ["h"])) THEN ((use_arg_then2 ("f", [])) (term_tac exists_tac)) THEN (done_tac));
];;

(* Lemma iso_imp_hyp_iso *)
let iso_imp_hyp_iso = Sections.section_proof ["H";"G"]
`H iso G ==> ?f. hyp_iso f (H, G)`
[
   (((((use_arg_then2 ("iso", [iso]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hyp_iso", [hyp_iso]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma h_map_outside *)
let h_map_outside = Sections.section_proof ["H";"x"]
`~(x:A IN dart H) ==>
        edge_map H x = x /\
        node_map H x = x /\
        face_map H x = x`
[
   (BETA_TAC THEN (move ["x_n_dart"]));
   ((fun arg_tac -> (use_arg_then2 ("hypermap_lemma", [hypermap_lemma])) (fun fst_arg -> (use_arg_then2 ("H", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["h"])));
   ((in_tac ["h"] false (repeat_tactic 1 9 (((use_arg_then2 ("permutes", [permutes]))(thm_tac (new_rewrite [] [])))))) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (done_tac));
];;

(* Lemma hyp_path_subset *)
let hyp_path_subset = Sections.section_proof ["H";"p";"n"]
`p 0 IN dart H /\ is_path H p n
        ==> (!i. i <= n ==> p i IN dart H)`
[
   (((((use_arg_then2 ("lemma_def_path", [lemma_def_path]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("go_one_step", [go_one_step]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["p0_in"])) THEN (move ["h"]));
   ((((THENL) elim [ALL_TAC; ((move ["i"]) THEN (move ["Ih"]))]) THEN ((TRY done_tac)) THEN (move ["i_le"])) THEN (in_tac ["i_le"] false (((use_arg_then2 ("LE_SUC_LT", [LE_SUC_LT]))(thm_tac (new_rewrite [] []))))));
   ((((fun arg_tac -> (use_arg_then2 ("h", [])) (fun fst_arg -> (use_arg_then2 ("i_le", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (repeat_tactic 1 9 (case)) THEN (BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((((use_arg_then2 ("lemma_dart_invariant", [lemma_dart_invariant]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("LT_IMP_LE", [LT_IMP_LE]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Section Iso1 *)
Sections.begin_section "Iso1";;
(Sections.add_section_var (mk_var ("H", (`:(A)hypermap`))));;
(Sections.add_section_var (mk_var ("G", (`:(B)hypermap`))));;
(Sections.add_section_var (mk_var ("f", (`:A->B`))));;

(* Lemma hyp_iso_edge_face *)
let hyp_iso_edge_face = Sections.section_proof []
`hyp_iso f (H,G) <=> BIJ f (dart H) (dart G) /\
	(!x. x IN dart H ==> edge_map G (f x) = f (edge_map H x)
			 /\ face_map G (f x) = f (face_map H x))`
[
   ((((use_arg_then2 ("hyp_iso", [hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andb_id2l", [andb_id2l])) (disch_tac [])) THEN (clear_assumption "andb_id2l") THEN (DISCH_THEN apply_tac) THEN (move ["_"])) THEN ((split_tac) THEN (move ["eq"]) THEN (move ["x"]) THEN (move ["x_in"])) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] []))))) THEN ((simp_tac THEN TRY done_tac))));
   ((((use_arg_then2 ("Hypermap.inverse2_hypermap_maps", [Hypermap.inverse2_hypermap_maps]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] [])))));
   ((fun arg_tac -> (use_arg_then2 ("Hypermap.hypermap_lemma", [Hypermap.hypermap_lemma])) (fun fst_arg -> (use_arg_then2 ("G", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["hypG"])));
   ((((fun arg_tac -> (use_arg_then2 ("PERMUTES_INVERSE_EQ", [PERMUTES_INVERSE_EQ])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`dart G`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("Hypermap.lemma_dart_invariant", [Hypermap.lemma_dart_invariant]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
   ((((use_arg_then2 ("EQ_SYM_EQ", [EQ_SYM_EQ]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("PERMUTES_INVERSE_EQ", [PERMUTES_INVERSE_EQ])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`dart G`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("Hypermap.lemma_dart_invariant", [Hypermap.lemma_dart_invariant]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
   (((((fun arg_tac -> (use_arg_then2 ("o_THM", [o_THM])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`edge_map H`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("o_THM", [o_THM])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`face_map H`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Hypermap.hypermap_cyclic", [Hypermap.hypermap_cyclic]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("I_THM", [I_THM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma hyp_iso_edge_node *)
let hyp_iso_edge_node = Sections.section_proof []
`hyp_iso f (H,G) <=> BIJ f (dart H) (dart G) /\
	(!x. x IN dart H ==> edge_map G (f x) = f (edge_map H x)
			 /\ node_map G (f x) = f (node_map H x))`
[
   ((((use_arg_then2 ("hyp_iso", [hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andb_id2l", [andb_id2l])) (disch_tac [])) THEN (clear_assumption "andb_id2l") THEN (DISCH_THEN apply_tac) THEN (move ["_"])) THEN ((split_tac) THEN (move ["eq"]) THEN (move ["x"]) THEN (move ["x_in"])) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] []))))) THEN ((simp_tac THEN TRY done_tac))));
   ((((use_arg_then2 ("Hypermap.inverse2_hypermap_maps", [Hypermap.inverse2_hypermap_maps]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] [])))));
   ((fun arg_tac -> (use_arg_then2 ("Hypermap.hypermap_lemma", [Hypermap.hypermap_lemma])) (fun fst_arg -> (use_arg_then2 ("G", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["hypG"])));
   ((((fun arg_tac -> (use_arg_then2 ("PERMUTES_INVERSE_EQ", [PERMUTES_INVERSE_EQ])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`dart G`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("Hypermap.lemma_dart_invariant", [Hypermap.lemma_dart_invariant]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
   ((((use_arg_then2 ("EQ_SYM_EQ", [EQ_SYM_EQ]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("PERMUTES_INVERSE_EQ", [PERMUTES_INVERSE_EQ])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`dart G`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("Hypermap.lemma_dart_invariant", [Hypermap.lemma_dart_invariant]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
   (((((fun arg_tac -> (use_arg_then2 ("o_THM", [o_THM])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`node_map H`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("o_THM", [o_THM])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`edge_map H`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Hypermap.hypermap_lemma", [Hypermap.hypermap_lemma]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("I_THM", [I_THM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;
(Sections.add_section_hyp "isoHG" (`hyp_iso f (H, G)`));;

(* Lemma hyp_iso_bij *)
let hyp_iso_bij = Sections.section_proof []
`BIJ f (dart H) (dart G)`
[
   ((in_tac ["isoHG"] false (((use_arg_then2 ("hyp_iso", [hyp_iso]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma hyp_iso_inj *)
let hyp_iso_inj = Sections.section_proof ["x";"y"]
`x IN dart H /\ y IN dart H /\ f x = f y ==> x = y`
[
   ((((use_arg_then2 ("isoHG", [])) (disch_tac [])) THEN (clear_assumption "isoHG") THEN BETA_TAC) THEN (((((use_arg_then2 ("hyp_iso", [hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("bij_alt", [bij_alt]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["_"])) THEN (case THEN (move ["inj"])) THEN (move ["_"]) THEN (move ["_"]) THEN (move ["h"])) THEN (((use_arg_then2 ("inj", [])) (disch_tac [])) THEN (clear_assumption "inj") THEN (exact_tac)) THEN (done_tac));
];;

(* Lemma hyp_iso_surj *)
let hyp_iso_surj = Sections.section_proof ["y"]
`y IN dart G ==> ?x. x IN dart H /\ f x = y`
[
   ((((use_arg_then2 ("isoHG", [])) (disch_tac [])) THEN (clear_assumption "isoHG") THEN BETA_TAC) THEN (((((use_arg_then2 ("hyp_iso", [hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("bij_alt", [bij_alt]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["_"])) THEN (case THEN (move ["_"])) THEN (move ["surj"]) THEN (move ["_"]) THEN (move ["y"])) THEN (((use_arg_then2 ("surj", [])) (disch_tac [])) THEN (clear_assumption "surj") THEN (exact_tac)) THEN (done_tac));
];;

(* Lemma hyp_iso_dart *)
let hyp_iso_dart = Sections.section_proof ["x"]
`x IN dart H ==> f x IN dart G`
[
   ((((use_arg_then2 ("isoHG", [])) (disch_tac [])) THEN (clear_assumption "isoHG") THEN BETA_TAC) THEN (((((use_arg_then2 ("hyp_iso", [hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("bij_alt", [bij_alt]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["h"])) THEN (move ["_"]) THEN (move ["_"])) THEN (((use_arg_then2 ("h", [])) (disch_tac [])) THEN (clear_assumption "h") THEN (exact_tac)) THEN (done_tac));
];;

(* Lemma hyp_iso_SURJ *)
let hyp_iso_SURJ = Sections.section_proof []
`SURJ f (dart H) (dart G)`
[
   ((((use_arg_then2 ("SURJ", [SURJ]))(thm_tac (new_rewrite [] [])))) THEN ((split_tac) THEN (move ["x"]) THEN (move ["x_in"])) THEN (((fun arg_tac ->(use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart]))(fun tmp_arg1 -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma hyp_iso_INJ *)
let hyp_iso_INJ = Sections.section_proof []
`INJ f (dart H) (dart G)`
[
   ((THENL_FIRST) ((((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] [])))) THEN ((THENL) (split_tac) [((move ["x"]) THEN (move ["x_in"])); ((move ["x"]) THEN (move ["y"]))])) ((((use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
   (((use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (disch_tac [])) THEN (clear_assumption "hyp_iso_inj") THEN (exact_tac));
];;

(* Lemma hyp_iso_comm *)
let hyp_iso_comm = Sections.section_proof ["x"]
`x IN dart H ==>
        edge_map G (f x) = f (edge_map H x) /\
        node_map G (f x) = f (node_map H x) /\
        face_map G (f x) = f (face_map H x)`
[
   ((((use_arg_then2 ("isoHG", [])) (disch_tac [])) THEN (clear_assumption "isoHG") THEN BETA_TAC) THEN ((((use_arg_then2 ("hyp_iso", [hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (move ["_"]) THEN (move ["h"]) THEN (move ["x_in"])) THEN (repeat_tactic 1 9 (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma hyp_iso_inverse_comm *)
let hyp_iso_inverse_comm = Sections.section_proof ["x"]
`x IN dart H
	==> inverse (edge_map G) (f x) = f (inverse (edge_map H) x)
	 /\ inverse (node_map G) (f x) = f (inverse (node_map H) x)
	 /\ inverse (face_map G) (f x) = f (inverse (face_map H) x)`
[
   (BETA_TAC THEN (move ["x_in"]));
   ((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("PERMUTES_INVERSE_EQ", [PERMUTES_INVERSE_EQ])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`dart G`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("Hypermap.hypermap_lemma", [Hypermap.hypermap_lemma]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
   ((repeat_tactic 1 9 (((use_arg_then2 ("hyp_iso_comm", [hyp_iso_comm]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("Hypermap.lemma_dart_inveriant_under_inverse_maps", [Hypermap.lemma_dart_inveriant_under_inverse_maps]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
   (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("PERMUTES_INVERSES", [PERMUTES_INVERSES])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`dart H`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("Hypermap.hypermap_lemma", [Hypermap.hypermap_lemma]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Lemma hyp_iso_inv *)
let hyp_iso_inv = Sections.section_proof []
`hyp_iso (res_inv f (dart H)) (G, H)`
[
   (((((use_arg_then2 ("hyp_iso", [hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("bij_res_inv", [bij_res_inv])) (fun fst_arg -> (use_arg_then2 ("hyp_iso_bij", [hyp_iso_bij])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))) THEN (move ["d"]) THEN (move ["d_in"]));
   ((fun arg_tac -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj])) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["t"]) THEN (case THEN ((move ["t_in"]) THEN (move ["d_eq"])))))));
   (((((use_arg_then2 ("d_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("hyp_iso_comm", [hyp_iso_comm]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("res_inv_bij", [res_inv_bij])) (fun fst_arg -> (use_arg_then2 ("hyp_iso_bij", [hyp_iso_bij])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("lemma_dart_invariant", [lemma_dart_invariant]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma hyp_iso_ext *)
let hyp_iso_ext = Sections.section_proof ["g"]
`(!d. d IN (dart H) ==> f d = g d)
	==> hyp_iso g (H, G)`
[
   ((BETA_TAC THEN (move ["ext"])) THEN (((((use_arg_then2 ("hyp_iso", [hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("bij_ext", [bij_ext])) (fun fst_arg -> (use_arg_then2 ("hyp_iso_bij", [hyp_iso_bij])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))) THEN (move ["d"]) THEN (move ["d_in"])));
   (((repeat_tactic 1 9 (((use_arg_then2 ("ext", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("hyp_iso_comm", [hyp_iso_comm]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("Hypermap.lemma_dart_invariant", [Hypermap.lemma_dart_invariant]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma iso_components *)
let iso_components = Sections.section_proof ["d"]
`d IN dart H ==>
        node G (f d) = IMAGE f (node H d) /\
        face G (f d) = IMAGE f (face H d) /\
        edge G (f d) = IMAGE f (edge H d)`
[
   ((((use_arg_then2 ("isoHG", [])) (disch_tac [])) THEN (clear_assumption "isoHG") THEN BETA_TAC) THEN ((((use_arg_then2 ("hyp_iso", [hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["bij"])) THEN (move ["f_eq"]) THEN (move ["d_in"])));
   ((repeat_tactic 1 9 (((use_arg_then2 ("node", [node]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("face", [face]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("edge", [edge]))(thm_tac (new_rewrite [] []))))));
   ((repeat_tactic 1 9 ((split_tac))) THEN (((fun arg_tac -> (use_arg_then2 ("orbit_comm", [orbit_comm])) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)) THEN ((split_tac) THEN (move ["x"]) THEN (move ["x_in"])) THEN ((repeat_tactic 0 10 (((use_arg_then2 ("lemma_dart_invariant", [lemma_dart_invariant]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Lemma hyp_iso_card_components *)
let hyp_iso_card_components = Sections.section_proof ["x"]
`x IN dart H ==> 
	CARD (face H x) = CARD (face G (f x)) /\
	CARD (node H x) = CARD (node G (f x)) /\
	CARD (edge H x) = CARD (edge G (f x))`
[
   ((BETA_TAC THEN (move ["x_in"])) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("iso_components", [iso_components]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))));
   (((repeat_tactic 1 9 (((use_arg_then2 ("CARD_IMAGE_INJ", [CARD_IMAGE_INJ]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((fun arg_tac ->(use_arg_then2 ("EDGE_FINITE", [EDGE_FINITE]))(fun tmp_arg1 -> (fun arg_tac ->(use_arg_then2 ("FACE_FINITE", [FACE_FINITE]))(fun tmp_arg1 -> (use_arg_then2 ("NODE_FINITE", [NODE_FINITE]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN (BETA_TAC THEN (move ["a"]) THEN (move ["b"]) THEN (case THEN (move ["a_in"])) THEN (case THEN (move ["b_in"])) THEN (move ["eq"])) THEN (((fun arg_tac -> (use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (fun fst_arg -> (use_arg_then2 ("eq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)));
   ((split_tac) THEN ((use_arg_then2 ("IN_TRANS", [IN_TRANS])) (thm_tac apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`face H x`))) (term_tac exists_tac)) THEN (((use_arg_then2 ("lemma_face_subset", [lemma_face_subset]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
   ((split_tac) THEN ((use_arg_then2 ("IN_TRANS", [IN_TRANS])) (thm_tac apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`node H x`))) (term_tac exists_tac)) THEN (((use_arg_then2 ("lemma_node_subset", [lemma_node_subset]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
   ((split_tac) THEN ((use_arg_then2 ("IN_TRANS", [IN_TRANS])) (thm_tac apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`edge H x`))) (term_tac exists_tac)) THEN (((use_arg_then2 ("lemma_edge_subset", [lemma_edge_subset]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma iso_node_set *)
let iso_node_set = Sections.section_proof []
`node_set G = IMAGE (IMAGE f) (node_set H)`
[
   (((repeat_tactic 1 9 (((use_arg_then2 ("node_set", [node_set]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("set_of_orbits", [set_of_orbits]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("node", [node]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["y"]));
   ((THENL_ROT (-1)) ((THENL) (split_tac) [((case THEN (move ["d"])) THEN (case THEN (move ["d_in"])) THEN (move ["y_eq"])); ((case THEN (move ["n"])) THEN (case THEN (move ["y_eq"])) THEN (case THEN (move ["d"])) THEN (case THEN (move ["d_in"])) THEN (move ["n_eq"]))]));
   ((fun arg_tac -> arg_tac (Arg_term (`f d`))) (term_tac exists_tac));
   (((((use_arg_then2 ("y_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("iso_components", [iso_components]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((simp_tac THEN TRY done_tac)) THEN (((use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((fun arg_tac -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj])) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["t"]) THEN (case THEN ((move ["t_in"]) THEN (move ["f_eq"])))))));
   (((fun arg_tac -> arg_tac (Arg_term (`node H t`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("y_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("iso_components", [iso_components]))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac))));
   (((use_arg_then2 ("t", [])) (term_tac exists_tac)) THEN (done_tac));
];;

(* Lemma iso_edge_set *)
let iso_edge_set = Sections.section_proof []
`edge_set G = IMAGE (IMAGE f) (edge_set H)`
[
   (((repeat_tactic 1 9 (((use_arg_then2 ("edge_set", [edge_set]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("set_of_orbits", [set_of_orbits]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("edge", [edge]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["y"]));
   ((THENL_ROT (-1)) ((THENL) (split_tac) [((case THEN (move ["d"])) THEN (case THEN (move ["d_in"])) THEN (move ["y_eq"])); ((case THEN (move ["n"])) THEN (case THEN (move ["y_eq"])) THEN (case THEN (move ["d"])) THEN (case THEN (move ["d_in"])) THEN (move ["n_eq"]))]));
   ((fun arg_tac -> arg_tac (Arg_term (`f d`))) (term_tac exists_tac));
   (((((use_arg_then2 ("y_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("iso_components", [iso_components]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((simp_tac THEN TRY done_tac)) THEN (((use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((fun arg_tac -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj])) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["t"]) THEN (case THEN ((move ["t_in"]) THEN (move ["f_eq"])))))));
   (((fun arg_tac -> arg_tac (Arg_term (`edge H t`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("y_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("iso_components", [iso_components]))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac))));
   (((use_arg_then2 ("t", [])) (term_tac exists_tac)) THEN (done_tac));
];;

(* Lemma iso_face_set *)
let iso_face_set = Sections.section_proof []
`face_set G = IMAGE (IMAGE f) (face_set H)`
[
   (((repeat_tactic 1 9 (((use_arg_then2 ("face_set", [face_set]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("set_of_orbits", [set_of_orbits]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("face", [face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["y"]));
   ((THENL_ROT (-1)) ((THENL) (split_tac) [((case THEN (move ["d"])) THEN (case THEN (move ["d_in"])) THEN (move ["y_eq"])); ((case THEN (move ["n"])) THEN (case THEN (move ["y_eq"])) THEN (case THEN (move ["d"])) THEN (case THEN (move ["d_in"])) THEN (move ["n_eq"]))]));
   ((fun arg_tac -> arg_tac (Arg_term (`f d`))) (term_tac exists_tac));
   (((((use_arg_then2 ("y_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("iso_components", [iso_components]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((simp_tac THEN TRY done_tac)) THEN (((use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((fun arg_tac -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj])) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["t"]) THEN (case THEN ((move ["t_in"]) THEN (move ["f_eq"])))))));
   (((fun arg_tac -> arg_tac (Arg_term (`face H t`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("y_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("iso_components", [iso_components]))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac))));
   (((use_arg_then2 ("t", [])) (term_tac exists_tac)) THEN (done_tac));
];;

(* Lemma iso_number_of_nodes *)
let iso_number_of_nodes = Sections.section_proof []
`number_of_nodes G = number_of_nodes H`
[
   (((repeat_tactic 1 9 (((use_arg_then2 ("number_of_nodes", [number_of_nodes]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("iso_node_set", [iso_node_set]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("CARD_IMAGE_INJ", [CARD_IMAGE_INJ]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("FINITE_HYPERMAP_ORBITS", [FINITE_HYPERMAP_ORBITS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN (move ["n1"]) THEN (move ["n2"]));
   (((repeat_tactic 1 9 (((use_arg_then2 ("node_set", [node_set]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("set_of_orbits", [set_of_orbits]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("node", [node]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN ((case THEN ALL_TAC) THEN (move ["d1"]) THEN (move ["n1_eq"]))) THEN (case THEN ((case THEN ALL_TAC) THEN (move ["d2"]) THEN (move ["n2_eq"]))) THEN (move ["i_eq"]));
   (((fun arg_tac -> (use_arg_then2 ("image_set_inj_gen", [image_set_inj_gen])) (fun fst_arg -> (use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
   (((((use_arg_then2 ("n1_eq", []))(thm_tac (new_rewrite [1] [])))) THEN (((use_arg_then2 ("n2_eq", []))(thm_tac (new_rewrite [1] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("lemma_node_subset", [lemma_node_subset]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Lemma iso_number_of_edges *)
let iso_number_of_edges = Sections.section_proof []
`number_of_edges G = number_of_edges H`
[
   (((repeat_tactic 1 9 (((use_arg_then2 ("number_of_edges", [number_of_edges]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("iso_edge_set", [iso_edge_set]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("CARD_IMAGE_INJ", [CARD_IMAGE_INJ]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("FINITE_HYPERMAP_ORBITS", [FINITE_HYPERMAP_ORBITS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN (move ["n1"]) THEN (move ["n2"]));
   (((repeat_tactic 1 9 (((use_arg_then2 ("edge_set", [edge_set]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("set_of_orbits", [set_of_orbits]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("edge", [edge]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN ((case THEN ALL_TAC) THEN (move ["d1"]) THEN (move ["n1_eq"]))) THEN (case THEN ((case THEN ALL_TAC) THEN (move ["d2"]) THEN (move ["n2_eq"]))) THEN (move ["i_eq"]));
   (((fun arg_tac -> (use_arg_then2 ("image_set_inj_gen", [image_set_inj_gen])) (fun fst_arg -> (use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
   (((((use_arg_then2 ("n1_eq", []))(thm_tac (new_rewrite [1] [])))) THEN (((use_arg_then2 ("n2_eq", []))(thm_tac (new_rewrite [1] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("lemma_edge_subset", [lemma_edge_subset]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Lemma iso_number_of_faces *)
let iso_number_of_faces = Sections.section_proof []
`number_of_faces G = number_of_faces H`
[
   (((repeat_tactic 1 9 (((use_arg_then2 ("number_of_faces", [number_of_faces]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("iso_face_set", [iso_face_set]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("CARD_IMAGE_INJ", [CARD_IMAGE_INJ]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("FINITE_HYPERMAP_ORBITS", [FINITE_HYPERMAP_ORBITS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN (move ["n1"]) THEN (move ["n2"]));
   (((repeat_tactic 1 9 (((use_arg_then2 ("face_set", [face_set]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("set_of_orbits", [set_of_orbits]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("face", [face]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN ((case THEN ALL_TAC) THEN (move ["d1"]) THEN (move ["n1_eq"]))) THEN (case THEN ((case THEN ALL_TAC) THEN (move ["d2"]) THEN (move ["n2_eq"]))) THEN (move ["i_eq"]));
   (((fun arg_tac -> (use_arg_then2 ("image_set_inj_gen", [image_set_inj_gen])) (fun fst_arg -> (use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
   (((((use_arg_then2 ("n1_eq", []))(thm_tac (new_rewrite [1] [])))) THEN (((use_arg_then2 ("n2_eq", []))(thm_tac (new_rewrite [1] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("lemma_face_subset", [lemma_face_subset]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Lemma iso_plain_imp *)
let iso_plain_imp = Sections.section_proof []
`plain_hypermap G ==> plain_hypermap H`
[
   (((repeat_tactic 1 9 (((use_arg_then2 ("plain_hypermap", [plain_hypermap]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("FUN_EQ_THM", [FUN_EQ_THM]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("I_THM", [I_THM]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] [])))))) THEN (move ["g_eq"]) THEN (move ["x"]));
   ((THENL_LAST) (((fun arg_tac -> arg_tac (Arg_term (`x IN dart H`))) (disch_eq_tac "x_in" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) ((repeat_tactic 1 9 (((use_arg_then2 ("h_map_outside", [h_map_outside]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
   ((((use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (disch_tac [])) THEN (clear_assumption "hyp_iso_inj") THEN (DISCH_THEN apply_tac)) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("hyp_iso_comm", [hyp_iso_comm]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("lemma_dart_invariant", [lemma_dart_invariant]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Lemma iso_edge_nondegenerate_imp *)
let iso_edge_nondegenerate_imp = Sections.section_proof []
`is_edge_nondegenerate G ==> is_edge_nondegenerate H`
[
   ((repeat_tactic 1 9 (((use_arg_then2 ("is_edge_nondegenerate", [is_edge_nondegenerate]))(thm_tac (new_rewrite [] []))))) THEN (move ["g_eq"]) THEN (move ["d"]) THEN (move ["d_in"]));
   (((fun arg_tac -> (use_arg_then2 ("g_eq", [])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN ((use_arg_then2 ("contra", [contra])) (disch_tac [])) THEN (clear_assumption "contra") THEN (DISCH_THEN apply_tac));
   ((((((use_arg_then2 ("hyp_iso_comm", [hyp_iso_comm]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma iso_simple_imp *)
let iso_simple_imp = Sections.section_proof []
`simple_hypermap G ==> simple_hypermap H`
[
   ((repeat_tactic 1 9 (((use_arg_then2 ("simple_hypermap", [simple_hypermap]))(thm_tac (new_rewrite [] []))))) THEN (move ["h"]) THEN (move ["d"]) THEN (move ["d_in"]));
   (((fun arg_tac -> (use_arg_then2 ("h", [])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC);
   ((repeat_tactic 1 9 (((use_arg_then2 ("iso_components", [iso_components]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("image_inter_inj_gen", [image_inter_inj_gen])) (fun fst_arg -> (use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("lemma_node_subset", [lemma_node_subset]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("lemma_face_subset", [lemma_face_subset]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
   ((fun arg_tac -> arg_tac (Arg_term (`{f d} = IMAGE f {d}`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))));
   (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_SING", [IN_SING]))(thm_tac (new_rewrite [] [])))))) THEN (move ["y"]));
   ((((THENL) (split_tac) [(((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))); ((case THEN (move ["x"])) THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))]) THEN ((TRY done_tac))) THEN ((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN (done_tac));
   ((BETA_TAC THEN (move ["eq"])) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("image_inj_gen", [image_inj_gen])) (fun fst_arg -> (use_arg_then2 ("eq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)));
   (((((use_arg_then2 ("SING_SUBSET", [SING_SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_in", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] []))))) THEN (move ["x"]) THEN (case THEN (move ["_"])));
   ((((use_arg_then2 ("x", [])) (disch_tac [])) THEN (clear_assumption "x") THEN BETA_TAC) THEN ((((use_arg_then2 ("SUBSET", [SUBSET]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("lemma_face_subset", [lemma_face_subset]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma iso_path_imp *)
let iso_path_imp = Sections.section_proof ["p";"n"]
`p 0 IN dart H /\ is_path H p n ==> is_path G (f o p) n`
[
   (BETA_TAC THEN (case THEN ((move ["p0_in"]) THEN (move ["p_path"]))));
   ((((use_arg_then2 ("p_path", [])) (disch_tac [])) THEN BETA_TAC) THEN (((repeat_tactic 1 9 (((use_arg_then2 ("lemma_def_path", [lemma_def_path]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("go_one_step", [go_one_step]))(thm_tac (new_rewrite [] [])))))) THEN (move ["h"]) THEN (move ["i"]) THEN (move ["i_lt"])));
   ((((fun arg_tac -> (use_arg_then2 ("h", [])) (fun fst_arg -> (use_arg_then2 ("i_lt", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (repeat_tactic 1 9 (case)) THEN (BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("hyp_iso_comm", [hyp_iso_comm]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("hyp_path_subset", [hyp_path_subset])) (fun fst_arg -> (use_arg_then2 ("p_path", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("p0_in", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("LT_IMP_LE", [LT_IMP_LE]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma iso_path_inv *)
let iso_path_inv = Sections.section_proof ["q";"n"]
`q 0 IN dart G /\ is_path G q n ==>
        ?p. (!i. i <= n ==> q i = f (p i)) /\ p 0 IN dart H /\ is_path H p n`
[
   ((BETA_TAC THEN (case THEN ((move ["q0"]) THEN (move ["q_path"])))) THEN (((use_arg_then2 ("q_path", [])) (disch_tac [])) THEN BETA_TAC));
   ((repeat_tactic 1 9 (((use_arg_then2 ("lemma_def_path", [lemma_def_path]))(thm_tac (new_rewrite [] []))))) THEN (move ["q_path2"]));
   (((fun arg_tac -> arg_tac (Arg_term (`res_inv f (dart H) o q`))) (term_tac exists_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] []))))));
   ((THENL) (split_tac) [((move ["i"]) THEN (move ["i_le"])); ALL_TAC]);
   (((((fun arg_tac -> (use_arg_then2 ("res_inv_right", [res_inv_right])) (fun fst_arg -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("hyp_path_subset", [hyp_path_subset])) (fun fst_arg -> (use_arg_then2 ("q_path", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (((((fun arg_tac -> (use_arg_then2 ("res_inv_right", [res_inv_right])) (fun fst_arg -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))) THEN (move ["i"]) THEN (move ["i_lt"]));
   ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("hyp_path_subset", [hyp_path_subset])) (fun fst_arg -> (use_arg_then2 ("q_path", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("q0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("LT_IMP_LE", [LT_IMP_LE])) (fun fst_arg -> (use_arg_then2 ("i_lt", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (case THEN ((move ["t"]) THEN (case THEN (move ["t_in"])) THEN (move ["qi_eq"]))))));
   ((((use_arg_then2 ("qi_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("res_inv_left", [res_inv_left])) (fun fst_arg -> (use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
   ((((fun arg_tac -> (use_arg_then2 ("q_path2", [])) (fun fst_arg -> (use_arg_then2 ("i_lt", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (repeat_tactic 1 9 (((use_arg_then2 ("go_one_step", [go_one_step]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (case)) THEN (BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((((use_arg_then2 ("qi_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("hyp_iso_comm", [hyp_iso_comm]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("res_inv_bij", [res_inv_bij])) (fun fst_arg -> (use_arg_then2 ("hyp_iso_bij", [hyp_iso_bij])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("lemma_dart_invariant", [lemma_dart_invariant]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma iso_comb_component *)
let iso_comb_component = Sections.section_proof ["d"]
`d IN dart H ==>
        comb_component G (f d) = IMAGE f (comb_component H d)`
[
   ((repeat_tactic 1 9 (((use_arg_then2 ("comb_component", [comb_component]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("image_lemma", [image_lemma]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("is_in_component", [is_in_component]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
   ((THENL_ROT (-1)) ((BETA_TAC THEN (move ["d_in"]) THEN (move ["z"])) THEN ((THENL) (split_tac) [((case THEN (move ["p"])) THEN (case THEN (move ["n"])) THEN (case THEN (move ["p0_eq"])) THEN (case THEN (move ["pn_eq"])) THEN (move ["pathG"])); ALL_TAC])));
   (BETA_TAC THEN (case THEN (move ["t"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["p"])) THEN (case THEN (move ["n"])) THEN (case THEN (move ["p0_eq"])) THEN (case THEN (move ["pn_eq"])) THEN (move ["path_p"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
   ((((fun arg_tac -> arg_tac (Arg_term (`f o p`))) (term_tac exists_tac)) THEN ((use_arg_then2 ("n", [])) (term_tac exists_tac))) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("iso_path_imp", [iso_path_imp]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("p0_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((THENL_FIRST) (((fun arg_tac -> (use_arg_then2 ("iso_path_inv", [iso_path_inv])) (fun fst_arg -> (use_arg_then2 ("pathG", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)) THEN (ANTS_TAC)) (((((use_arg_then2 ("p0_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
   (BETA_TAC THEN (case THEN (move ["q"])) THEN (case THEN (move ["p_eq"])) THEN (case THEN (move ["q0"])) THEN (move ["path_q"]));
   (((fun arg_tac -> arg_tac (Arg_term (`q n`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("p_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("LE_REFL", [LE_REFL]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("pn_eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)));
   ((((use_arg_then2 ("q", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("n", [])) (term_tac exists_tac))) THEN (repeat_tactic 1 9 (((split_tac) THEN ((TRY done_tac))))));
   ((((use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (disch_tac [])) THEN (clear_assumption "hyp_iso_inj") THEN (DISCH_THEN apply_tac)) THEN ((((use_arg_then2 ("p_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("LE_0", [LE_0]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma iso_set_part_components *)
let iso_set_part_components = Sections.section_proof []
`set_of_components G = IMAGE (IMAGE f) (set_of_components H)`
[
   (((repeat_tactic 1 9 (((use_arg_then2 ("set_of_components", [set_of_components]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("set_part_components", [set_part_components]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["c"]));
   ((THENL) (split_tac) [((case THEN (move ["d"])) THEN (case THEN (move ["d_in"])) THEN (move ["c_eq"])); ((case THEN (move ["c2"])) THEN (case THEN (move ["c_eq"])) THEN (case THEN (move ["t"])) THEN (case THEN (move ["t_in"])) THEN (move ["c2_eq"]))]);
   ((fun arg_tac -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj])) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["t"]) THEN (case THEN ((move ["t_in"]) THEN (move ["d_eq"])))))));
   ((THENL_LAST) (((fun arg_tac -> arg_tac (Arg_term (`comb_component H t`))) (term_tac exists_tac)) THEN (split_tac)) (((use_arg_then2 ("t", [])) (term_tac exists_tac)) THEN (done_tac)));
   (((((use_arg_then2 ("iso_comb_component", [iso_comb_component]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("d_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("c_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (done_tac));
   ((fun arg_tac -> arg_tac (Arg_term (`f t`))) (term_tac exists_tac));
   (((((use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("c_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("c2_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("iso_comb_component", [iso_comb_component]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Lemma iso_number_of_components *)
let iso_number_of_components = Sections.section_proof []
`number_of_components G = number_of_components H`
[
   ((repeat_tactic 1 9 (((use_arg_then2 ("number_of_components", [number_of_components]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("iso_set_part_components", [iso_set_part_components]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("CARD_IMAGE_INJ", [CARD_IMAGE_INJ]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
   (((((use_arg_then2 ("FINITE_HYPERMAP_COMPONENTS", [FINITE_HYPERMAP_COMPONENTS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN (move ["n1"]) THEN (move ["n2"]));
   ((repeat_tactic 1 9 (((use_arg_then2 ("set_of_components", [set_of_components]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("set_part_components", [set_part_components]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac));
   (BETA_TAC THEN (case THEN ((case THEN (move ["d1"])) THEN (move ["n1_eq"]))) THEN (case THEN ((case THEN (move ["d2"])) THEN (move ["n2_eq"]))) THEN (move ["i_eq"]));
   (((fun arg_tac -> (use_arg_then2 ("image_set_inj_gen", [image_set_inj_gen])) (fun fst_arg -> (use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
   (((((use_arg_then2 ("i_eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("n1_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n2_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("lemma_component_subset", [lemma_component_subset]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Lemma iso_dart *)
let iso_dart = Sections.section_proof []
`dart G = IMAGE f (dart H)`
[
   ((((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] []))))) THEN (move ["d"])) THEN ((THENL) (split_tac) [(move ["d_in"]); ((case THEN (move ["t"])) THEN (case THEN ((move ["d_eq"]) THEN (move ["t_in"]))))]));
   ((fun arg_tac -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj])) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["t"]) THEN (move ["h"])))));
   (((use_arg_then2 ("t", [])) (term_tac exists_tac)) THEN (done_tac));
   (((((use_arg_then2 ("d_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma iso_card_dart *)
let iso_card_dart = Sections.section_proof []
`CARD (dart G) = CARD (dart H)`
[
   (((((use_arg_then2 ("iso_dart", [iso_dart]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("CARD_IMAGE_INJ", [CARD_IMAGE_INJ]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("hypermap_lemma", [hypermap_lemma]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (disch_tac [])) THEN (clear_assumption "hyp_iso_inj") THEN (exact_tac)) THEN (done_tac));
];;

(* Lemma iso_planar_imp *)
let iso_planar_imp = Sections.section_proof []
`planar_hypermap G ==> planar_hypermap H`
[
   ((repeat_tactic 1 9 (((use_arg_then2 ("planar_hypermap", [planar_hypermap]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("iso_card_dart", [iso_card_dart]))(thm_tac (new_rewrite [] [])))));
   (((((use_arg_then2 ("iso_number_of_edges", [iso_number_of_edges]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("iso_number_of_nodes", [iso_number_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("iso_number_of_faces", [iso_number_of_faces]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("iso_number_of_components", [iso_number_of_components]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma iso_connected_imp *)
let iso_connected_imp = Sections.section_proof []
`connected_hypermap G ==> connected_hypermap H`
[
   (((repeat_tactic 1 9 (((use_arg_then2 ("connected_hypermap", [connected_hypermap]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("iso_number_of_components", [iso_number_of_components]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Finalization of the section Iso1 *)
let hyp_iso_edge_face = Sections.finalize_theorem hyp_iso_edge_face;;
let hyp_iso_edge_node = Sections.finalize_theorem hyp_iso_edge_node;;
let hyp_iso_bij = Sections.finalize_theorem hyp_iso_bij;;
let hyp_iso_inj = Sections.finalize_theorem hyp_iso_inj;;
let hyp_iso_surj = Sections.finalize_theorem hyp_iso_surj;;
let hyp_iso_dart = Sections.finalize_theorem hyp_iso_dart;;
let hyp_iso_SURJ = Sections.finalize_theorem hyp_iso_SURJ;;
let hyp_iso_INJ = Sections.finalize_theorem hyp_iso_INJ;;
let hyp_iso_comm = Sections.finalize_theorem hyp_iso_comm;;
let hyp_iso_inverse_comm = Sections.finalize_theorem hyp_iso_inverse_comm;;
let hyp_iso_inv = Sections.finalize_theorem hyp_iso_inv;;
let hyp_iso_ext = Sections.finalize_theorem hyp_iso_ext;;
let iso_components = Sections.finalize_theorem iso_components;;
let hyp_iso_card_components = Sections.finalize_theorem hyp_iso_card_components;;
let iso_node_set = Sections.finalize_theorem iso_node_set;;
let iso_edge_set = Sections.finalize_theorem iso_edge_set;;
let iso_face_set = Sections.finalize_theorem iso_face_set;;
let iso_number_of_nodes = Sections.finalize_theorem iso_number_of_nodes;;
let iso_number_of_edges = Sections.finalize_theorem iso_number_of_edges;;
let iso_number_of_faces = Sections.finalize_theorem iso_number_of_faces;;
let iso_plain_imp = Sections.finalize_theorem iso_plain_imp;;
let iso_edge_nondegenerate_imp = Sections.finalize_theorem iso_edge_nondegenerate_imp;;
let iso_simple_imp = Sections.finalize_theorem iso_simple_imp;;
let iso_path_imp = Sections.finalize_theorem iso_path_imp;;
let iso_path_inv = Sections.finalize_theorem iso_path_inv;;
let iso_comb_component = Sections.finalize_theorem iso_comb_component;;
let iso_set_part_components = Sections.finalize_theorem iso_set_part_components;;
let iso_number_of_components = Sections.finalize_theorem iso_number_of_components;;
let iso_dart = Sections.finalize_theorem iso_dart;;
let iso_card_dart = Sections.finalize_theorem iso_card_dart;;
let iso_planar_imp = Sections.finalize_theorem iso_planar_imp;;
let iso_connected_imp = Sections.finalize_theorem iso_connected_imp;;
Sections.end_section "Iso1";;
(Sections.add_section_type (mk_var ("H", (`:(C)hypermap`))));;
(Sections.add_section_type (mk_var ("G", (`:(D)hypermap`))));;

(* Lemma iso_plain *)
let iso_plain = Sections.section_proof ["H";"G"]
`H iso G ==> (plain_hypermap H <=> plain_hypermap G)`
[
   ((BETA_TAC THEN (move ["iso"])) THEN ((split_tac) THEN (move ["h"])) THEN ((fun arg_tac -> (use_arg_then2 ("iso_plain_imp", [iso_plain_imp])) (fun fst_arg -> (use_arg_then2 ("h", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac apply_tac)) THEN ((((use_arg_then2 ("iso_imp_hyp_iso", [iso_imp_hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("iso_sym", [iso_sym]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma iso_edge_nondegenerate *)
let iso_edge_nondegenerate = Sections.section_proof ["H";"G"]
`H iso G ==> (is_edge_nondegenerate H <=> is_edge_nondegenerate G)`
[
   ((BETA_TAC THEN (move ["iso"])) THEN ((split_tac) THEN (move ["h"])) THEN ((fun arg_tac -> (use_arg_then2 ("iso_edge_nondegenerate_imp", [iso_edge_nondegenerate_imp])) (fun fst_arg -> (use_arg_then2 ("h", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac apply_tac)) THEN ((((use_arg_then2 ("iso_imp_hyp_iso", [iso_imp_hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("iso_sym", [iso_sym]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma iso_simple *)
let iso_simple = Sections.section_proof ["H";"G"]
`H iso G ==> (simple_hypermap H <=> simple_hypermap G)`
[
   ((BETA_TAC THEN (move ["iso"])) THEN ((split_tac) THEN (move ["h"])) THEN ((fun arg_tac -> (use_arg_then2 ("iso_simple_imp", [iso_simple_imp])) (fun fst_arg -> (use_arg_then2 ("h", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac apply_tac)) THEN ((((use_arg_then2 ("iso_imp_hyp_iso", [iso_imp_hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("iso_sym", [iso_sym]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma iso_planar *)
let iso_planar = Sections.section_proof ["H";"G"]
`H iso G ==> (planar_hypermap H <=> planar_hypermap G)`
[
   ((BETA_TAC THEN (move ["iso"])) THEN ((split_tac) THEN (move ["h"])) THEN ((fun arg_tac -> (use_arg_then2 ("iso_planar_imp", [iso_planar_imp])) (fun fst_arg -> (use_arg_then2 ("h", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac apply_tac)) THEN ((((use_arg_then2 ("iso_imp_hyp_iso", [iso_imp_hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("iso_sym", [iso_sym]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma iso_connected *)
let iso_connected = Sections.section_proof ["H";"G"]
`H iso G ==> (connected_hypermap H <=> connected_hypermap G)`
[
   ((BETA_TAC THEN (move ["iso"])) THEN ((split_tac) THEN (move ["h"])) THEN ((fun arg_tac -> (use_arg_then2 ("iso_connected_imp", [iso_connected_imp])) (fun fst_arg -> (use_arg_then2 ("h", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac apply_tac)) THEN ((((use_arg_then2 ("iso_imp_hyp_iso", [iso_imp_hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("iso_sym", [iso_sym]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Finalization of the section Iso *)
let hyp_iso_imp_iso = Sections.finalize_theorem hyp_iso_imp_iso;;
let iso_imp_hyp_iso = Sections.finalize_theorem iso_imp_hyp_iso;;
let h_map_outside = Sections.finalize_theorem h_map_outside;;
let hyp_path_subset = Sections.finalize_theorem hyp_path_subset;;
let hyp_iso_edge_face = Sections.finalize_theorem hyp_iso_edge_face;;
let hyp_iso_edge_node = Sections.finalize_theorem hyp_iso_edge_node;;
let hyp_iso_bij = Sections.finalize_theorem hyp_iso_bij;;
let hyp_iso_inj = Sections.finalize_theorem hyp_iso_inj;;
let hyp_iso_surj = Sections.finalize_theorem hyp_iso_surj;;
let hyp_iso_dart = Sections.finalize_theorem hyp_iso_dart;;
let hyp_iso_SURJ = Sections.finalize_theorem hyp_iso_SURJ;;
let hyp_iso_INJ = Sections.finalize_theorem hyp_iso_INJ;;
let hyp_iso_comm = Sections.finalize_theorem hyp_iso_comm;;
let hyp_iso_inverse_comm = Sections.finalize_theorem hyp_iso_inverse_comm;;
let hyp_iso_inv = Sections.finalize_theorem hyp_iso_inv;;
let hyp_iso_ext = Sections.finalize_theorem hyp_iso_ext;;
let iso_components = Sections.finalize_theorem iso_components;;
let hyp_iso_card_components = Sections.finalize_theorem hyp_iso_card_components;;
let iso_node_set = Sections.finalize_theorem iso_node_set;;
let iso_edge_set = Sections.finalize_theorem iso_edge_set;;
let iso_face_set = Sections.finalize_theorem iso_face_set;;
let iso_number_of_nodes = Sections.finalize_theorem iso_number_of_nodes;;
let iso_number_of_edges = Sections.finalize_theorem iso_number_of_edges;;
let iso_number_of_faces = Sections.finalize_theorem iso_number_of_faces;;
let iso_plain_imp = Sections.finalize_theorem iso_plain_imp;;
let iso_edge_nondegenerate_imp = Sections.finalize_theorem iso_edge_nondegenerate_imp;;
let iso_simple_imp = Sections.finalize_theorem iso_simple_imp;;
let iso_path_imp = Sections.finalize_theorem iso_path_imp;;
let iso_path_inv = Sections.finalize_theorem iso_path_inv;;
let iso_comb_component = Sections.finalize_theorem iso_comb_component;;
let iso_set_part_components = Sections.finalize_theorem iso_set_part_components;;
let iso_number_of_components = Sections.finalize_theorem iso_number_of_components;;
let iso_dart = Sections.finalize_theorem iso_dart;;
let iso_card_dart = Sections.finalize_theorem iso_card_dart;;
let iso_planar_imp = Sections.finalize_theorem iso_planar_imp;;
let iso_connected_imp = Sections.finalize_theorem iso_connected_imp;;
let iso_plain = Sections.finalize_theorem iso_plain;;
let iso_edge_nondegenerate = Sections.finalize_theorem iso_edge_nondegenerate;;
let iso_simple = Sections.finalize_theorem iso_simple;;
let iso_planar = Sections.finalize_theorem iso_planar;;
let iso_connected = Sections.finalize_theorem iso_connected;;
Sections.end_section "Iso";;

(* Section FanHypermapsIso *)
Sections.begin_section "FanHypermapsIso";;

(* Lemma fan_in_e_imp_neq *)
let fan_in_e_imp_neq = Sections.section_proof ["V";"E";"v";"w"]
`FAN (vec 0,V,E) /\ {v, w} IN E ==> ~(v = w)`
[
   (((((use_arg_then2 ("FAN", [FAN]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("graph", [graph]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN", [IN]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("HAS_SIZE", [HAS_SIZE]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["_"])) THEN (case THEN (move ["size2"])) THEN (move ["_"]) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("size2", [])) (thm_tac (match_mp_then snd_th MP_TAC)))));
   (((((use_arg_then2 ("Geomdetail.CARD2", [Geomdetail.CARD2]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma in_set_of_edge_neq *)
let in_set_of_edge_neq = Sections.section_proof ["V";"E";"v";"w"]
`FAN (vec 0,V,E) /\ w IN set_of_edge v V E ==> ~(v = w)`
[
   (((((use_arg_then2 ("set_of_edge", [set_of_edge]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["fan"])) THEN (case THEN (move ["vwE"])) THEN (move ["_"]));
   (((fun arg_tac -> (use_arg_then2 ("fan_in_e_imp_neq", [fan_in_e_imp_neq])) (fun fst_arg -> (use_arg_then2 ("fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (exact_tac));
];;

(* Lemma dart_of_fan_eq *)
let dart_of_fan_eq = Sections.section_proof ["V";"E"]
`dart_of_fan (V,E) = dart1_of_fan (V,E) UNION {(v,v) | v IN V /\ set_of_edge v V E = {}}`
[
   (((((use_arg_then2 ("dart_of_fan", [dart_of_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart1_of_fan", [dart1_of_fan]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL UNION_ACI)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma darts_of_fan_disj *)
let darts_of_fan_disj = Sections.section_proof ["V";"E"]
`FAN (vec 0,V,E) ==>
        DISJOINT (dart1_of_fan (V,E)) {(v,v) | v IN V /\ set_of_edge v V E = {}}`
[
   (((((use_arg_then2 ("DISJOINT", [DISJOINT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("NOT_IN_EMPTY", [NOT_IN_EMPTY]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] []))))) THEN (move ["fan"]) THEN (move ["x"]));
   (((fun arg_tac -> arg_tac (Arg_term (`x IN _`))) (disch_eq_tac "x_in" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
   ((((use_arg_then2 ("x_in", [])) (disch_tac [])) THEN (clear_assumption "x_in") THEN BETA_TAC) THEN (((((use_arg_then2 ("dart1_of_fan", [dart1_of_fan]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["v"])) THEN (case THEN (move ["w"])) THEN (case THEN (move ["vw_in"])) THEN (move ["x_eq"])));
   (((use_arg_then2 ("vw_in", [])) (disch_tac [])) THEN (clear_assumption "vw_in") THEN ((use_arg_then2 ("contraL", [contraL])) (disch_tac [])) THEN (clear_assumption "contraL") THEN (DISCH_THEN apply_tac) THEN ALL_TAC THEN (case THEN (move ["u"])) THEN (case THEN (move ["_"])) THEN (move ["x_eq2"]));
   (((fun arg_tac -> (use_arg_then2 ("fan_in_e_imp_neq", [fan_in_e_imp_neq])) (fun fst_arg -> (use_arg_then2 ("fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN ((use_arg_then2 ("contraL", [contraL])) (disch_tac [])) THEN (clear_assumption "contraL") THEN (DISCH_THEN apply_tac) THEN (move ["in_e"]));
   (((repeat_tactic 1 9 (((use_arg_then2 ("NOT_FORALL_THM", [NOT_FORALL_THM]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("negb_imply", [negb_imply]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negbK", [negbK]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("v", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("w", [])) (term_tac exists_tac))));
   (((((use_arg_then2 ("in_e", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("x_eq2", [])) (disch_tac [])) THEN (clear_assumption "x_eq2") THEN BETA_TAC) THEN (((((use_arg_then2 ("x_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) THEN (done_tac));
];;

(* Lemma dart1_of_fan_eq_image *)
let dart1_of_fan_eq_image = Sections.section_proof ["V";"E"]
`dart1_of_fan (V,E) = IMAGE contracted_dart (d1_fan (vec 0,V,E))`
[
   (((((use_arg_then2 ("dart1_of_fan", [dart1_of_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d1_fan", [d1_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["d"]));
   ((THENL) (split_tac) [((case THEN (move ["v"])) THEN (case THEN (move ["w"])) THEN (case THEN (move ["in_e"])) THEN (move ["d_eq"])); ((case THEN (move ["x"])) THEN (case THEN (move ["d_eq"])) THEN (case THEN (move ["x'"])) THEN (case THEN (move ["v"])) THEN (case THEN (move ["w"])) THEN (case THEN (move ["w1"])) THEN (case THEN ALL_TAC) THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (case THEN (move ["in_e"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (move ["x_eq"]))]);
   ((fun arg_tac -> arg_tac (Arg_term (`vec 0, v, w, sigma_fan (vec 0) V E v w`))) (term_tac exists_tac));
   ((((use_arg_then2 ("contracted_dart", [contracted_dart]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
   ((((fun arg_tac -> arg_tac (Arg_term (`vec 0`))) (term_tac exists_tac)) THEN ((use_arg_then2 ("v", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("w", [])) (term_tac exists_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan (vec 0) V E v w`))) (term_tac exists_tac))) THEN (done_tac));
   ((((use_arg_then2 ("v", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("w", [])) (term_tac exists_tac))) THEN ((((use_arg_then2 ("in_e", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("x_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("contracted_dart", [contracted_dart]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma dart2_of_fan_eq_image *)
let dart2_of_fan_eq_image = Sections.section_proof ["V";"E"]
`{(v,v) | v IN V /\ set_of_edge v V E = {}} = IMAGE contracted_dart (d20_fan (vec 0,V,E))`
[
   (((((use_arg_then2 ("d20_fan", [d20_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN", [IN]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (move ["d"]));
   ((THENL) (split_tac) [((case THEN (move ["v"])) THEN (case THEN (move ["h"])) THEN (move ["d_eq"])); ((case THEN (move ["x"])) THEN (case THEN (move ["d_eq"])) THEN (case THEN (move ["x'"])) THEN (case THEN (move ["v"])) THEN (case THEN (move ["h"])) THEN (move ["x_eq"]))]);
   ((fun arg_tac -> arg_tac (Arg_term (`vec 0, v, v, v`))) (term_tac exists_tac));
   ((((use_arg_then2 ("contracted_dart", [contracted_dart]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
   ((((fun arg_tac -> arg_tac (Arg_term (`vec 0`))) (term_tac exists_tac)) THEN ((use_arg_then2 ("v", [])) (term_tac exists_tac))) THEN (done_tac));
   (((use_arg_then2 ("v", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("d_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("x_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("contracted_dart", [contracted_dart]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma disjoint_preimage *)
let disjoint_preimage = Sections.section_proof ["f";"s";"t"]
`DISJOINT (IMAGE f s) (IMAGE f t) ==> DISJOINT s t`
[
   ((repeat_tactic 1 9 (((use_arg_then2 ("DISJOINT", [DISJOINT]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("CONTRAPOS_THM", [CONTRAPOS_THM]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("MEMBER_NOT_EMPTY", [MEMBER_NOT_EMPTY]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] []))))));
   (BETA_TAC THEN (case THEN (move ["x"])) THEN (case THEN ((move ["xs"]) THEN (move ["xt"]))));
   (((fun arg_tac -> arg_tac (Arg_term (`f x`))) (term_tac exists_tac)) THEN (split_tac) THEN ((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN (done_tac));
];;

(* Lemma darts_of_fan_disj1 *)
let darts_of_fan_disj1 = Sections.section_proof ["V";"E"]
`FAN (vec 0,V,E) ==>
        DISJOINT (d1_fan (vec 0,V,E)) (d20_fan (vec 0,V,E))`
[
   ((BETA_TAC THEN (move ["fan"])) THEN (((fun arg_tac -> (use_arg_then2 ("disjoint_preimage", [disjoint_preimage])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`contracted_dart`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
   (((((use_arg_then2 ("dart1_of_fan_eq_image", [dart1_of_fan_eq_image]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dart2_of_fan_eq_image", [dart2_of_fan_eq_image]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("darts_of_fan_disj", [darts_of_fan_disj]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma bij_contracted_dart1 *)
let bij_contracted_dart1 = Sections.section_proof ["V";"E"]
`BIJ contracted_dart (d1_fan (vec 0,V,E)) (dart1_of_fan (V,E))`
[
   ((((use_arg_then2 ("bij_alt", [bij_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d1_fan", [d1_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart1_of_fan", [dart1_of_fan]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac));
   (repeat_tactic 1 9 ((split_tac)));
   (BETA_TAC THEN (move ["x"]) THEN (case THEN (move ["x'"])) THEN (case THEN (move ["v"])) THEN (case THEN (move ["w"])) THEN (case THEN (move ["w1"])) THEN (case THEN ALL_TAC) THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (case THEN (move ["in_e"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (move ["x_eq"]));
   ((((use_arg_then2 ("v", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("w", [])) (term_tac exists_tac))) THEN ((((use_arg_then2 ("x_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("contracted_dart", [contracted_dart]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (BETA_TAC THEN (move ["x"]) THEN (move ["y"]) THEN (case THEN ALL_TAC) THEN (case THEN (move ["x'"])) THEN (case THEN (move ["v"])) THEN (case THEN (move ["w"])) THEN (case THEN (move ["w1"])) THEN (case THEN (move ["h"])) THEN (move ["x_eq"]) THEN (case THEN ALL_TAC) THEN (case THEN (move ["y'"])) THEN (case THEN (move ["v'"])) THEN (case THEN (move ["w'"])) THEN (case THEN (move ["w1'"])) THEN (case THEN (move ["h'"])) THEN (move ["y_eq"]));
   (((((use_arg_then2 ("x_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("y_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("contracted_dart", [contracted_dart]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((move ["v_eq"]) THEN (move ["w_eq"]))));
   (((repeat_tactic 1 9 (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("h'", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("v_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (BETA_TAC THEN (move ["y"]) THEN (case THEN (move ["v"])) THEN (case THEN (move ["w"])) THEN (case THEN (move ["in_e"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
   ((fun arg_tac -> arg_tac (Arg_term (`vec 0, v, w, sigma_fan (vec 0) V E v w`))) (term_tac exists_tac));
   ((((use_arg_then2 ("contracted_dart", [contracted_dart]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
   ((((fun arg_tac -> arg_tac (Arg_term (`vec 0`))) (term_tac exists_tac)) THEN ((use_arg_then2 ("v", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("w", [])) (term_tac exists_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan (vec 0) V E v w`))) (term_tac exists_tac))) THEN (done_tac));
];;

(* Lemma bij_contracted_dart2 *)
let bij_contracted_dart2 = Sections.section_proof ["V";"E"]
`BIJ contracted_dart (d20_fan (vec 0,V,E)) {(v,v) | v IN V /\ set_of_edge v V E = {}}`
[
   ((((use_arg_then2 ("bij_alt", [bij_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d20_fan", [d20_fan]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN", [IN]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
   (repeat_tactic 1 9 ((split_tac)));
   (BETA_TAC THEN (move ["x"]) THEN (case THEN (move ["x'"])) THEN (case THEN (move ["v"])) THEN (case THEN (move ["h"])) THEN (move ["x_eq"]));
   (((use_arg_then2 ("v", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("x_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("contracted_dart", [contracted_dart]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (BETA_TAC THEN (move ["x"]) THEN (move ["y"]) THEN (case THEN ALL_TAC) THEN (case THEN (move ["x'"])) THEN (case THEN (move ["v"])) THEN (case THEN (move ["h"])) THEN (move ["x_eq"]) THEN (case THEN ALL_TAC) THEN (case THEN (move ["y'"])) THEN (case THEN (move ["v'"])) THEN (case THEN (move ["h'"])) THEN (move ["y_eq"]));
   ((((((use_arg_then2 ("x_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("y_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("contracted_dart", [contracted_dart]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("h'", []))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((BETA_TAC THEN (move ["y"]) THEN (case THEN (move ["v"])) THEN (case THEN (move ["h"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((fun arg_tac -> arg_tac (Arg_term (`vec 0, v, v, v`))) (term_tac exists_tac)));
   ((((use_arg_then2 ("contracted_dart", [contracted_dart]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
   ((((fun arg_tac -> arg_tac (Arg_term (`vec 0`))) (term_tac exists_tac)) THEN ((use_arg_then2 ("v", [])) (term_tac exists_tac))) THEN (done_tac));
];;

(* Section Iso *)
Sections.begin_section "Iso";;
(Sections.add_section_var (mk_var ("V", (`:real^3->bool`))));;
(Sections.add_section_var (mk_var ("E", (`:(real^3->bool)->bool`))));;
(Sections.add_section_hyp "fan" (`FAN (vec 0,V,E)`));;

(* Lemma bij_contracted_dart *)
let bij_contracted_dart = Sections.section_proof []
`BIJ contracted_dart (d_fan (vec 0,V,E)) (dart_of_fan (V,E))`
[
   ((fun arg_tac -> arg_tac (Arg_term (`contracted_dart = \t. if t IN d1_fan (vec 0,V,E) then contracted_dart t else contracted_dart t`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))));
   (((((use_arg_then2 ("if_same", [if_same]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ETA_AX", [ETA_AX]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((((use_arg_then2 ("d_fan", [d_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart_of_fan_eq", [dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("bij_disjoint_union", [bij_disjoint_union]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_of_fan_disj", [darts_of_fan_disj]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
   (((((use_arg_then2 ("darts_of_fan_disj1", [darts_of_fan_disj1]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("bij_contracted_dart1", [bij_contracted_dart1]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("bij_contracted_dart2", [bij_contracted_dart2]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma hypermap_of_fan_rep_alt *)
let hypermap_of_fan_rep_alt = Sections.section_proof []
`dart (hypermap1_of_fanx (vec 0,V,E)) = d_fan (vec 0,V,E)
	/\ edge_map (hypermap1_of_fanx (vec 0,V,E)) = res (e_fan (vec 0) V E) (d1_fan (vec 0,V,E))
	/\ node_map (hypermap1_of_fanx (vec 0,V,E)) = res (n_fan (vec 0) V E) (d1_fan (vec 0,V,E))
	/\ face_map (hypermap1_of_fanx (vec 0,V,E)) = res (f1_fan (vec 0) V E) (d1_fan (vec 0,V,E))`
[
   ((fun arg_tac -> (use_arg_then2 ("hypermap_of_fan_rep", [hypermap_of_fan_rep])) (fun fst_arg -> (use_arg_then2 ("fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
   (((fun arg_tac -> arg_tac (Arg_term (`\t. _ t`))) (term_tac (set_tac "p"))) THEN (((fun arg_tac ->  (conv_thm_tac DISCH_THEN)  (fun fst_arg -> (use_arg_then2 ("p", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac MP_TAC)) THEN BETA_TAC) THEN ((ANTS_TAC) THEN ((TRY done_tac)) THEN (move ["eq"])));
   (((repeat_tactic 1 9 (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("p_def", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Lemma fan_hypermaps_iso_explicit *)
let fan_hypermaps_iso_explicit = Sections.section_proof []
`hyp_iso contracted_dart (hypermap1_of_fanx (vec 0,V,E), hypermap_of_fan (V,E))`
[
   ((((use_arg_then2 ("hyp_iso", [hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("hypermap_of_fan_rep_alt", [hypermap_of_fan_rep_alt]))(thm_tac (new_rewrite [] []))))));
   ((((use_arg_then2 ("bij_contracted_dart", [bij_contracted_dart]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("d_fan", [d_fan]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))));
   ((fun arg_tac -> arg_tac (Arg_term (`x IN d20_fan (vec 0,V,E) ==> ~(x IN d1_fan (vec 0,V,E))`))) (term_tac (have_gen_tac ["x"](move ["x_in_d2"]))));
   ((BETA_TAC THEN (move ["x2"])) THEN (((fun arg_tac -> (use_arg_then2 ("darts_of_fan_disj1", [darts_of_fan_disj1])) (fun fst_arg -> (use_arg_then2 ("fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN ((use_arg_then2 ("contraL", [contraL])) (disch_tac [])) THEN (clear_assumption "contraL") THEN (DISCH_THEN apply_tac) THEN (move ["x1"])));
   (((((use_arg_then2 ("DISJOINT", [DISJOINT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEMBER_NOT_EMPTY", [MEMBER_NOT_EMPTY]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN (done_tac));
   ((THENL_ROT (-1)) (((((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] [])))) THEN (move ["x"]) THEN (case THEN (move ["x_in"]))) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("x_in", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("x_in_d2", []))(thm_tac (new_rewrite [] []))))) THEN ((simp_tac THEN TRY done_tac)))));
   ((((use_arg_then2 ("x_in", [])) (disch_tac [])) THEN (clear_assumption "x_in") THEN BETA_TAC) THEN (((((use_arg_then2 ("d20_fan", [d20_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["x'"])) THEN (case THEN (move ["v"])) THEN (case THEN (move ["h"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))));
   ((((use_arg_then2 ("contracted_dart", [contracted_dart]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_fan_pair_ext", [e_fan_pair_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_fan_pair_ext", [n_fan_pair_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_fan_pair_ext", [f_fan_pair_ext]))(thm_tac (new_rewrite [] [])))));
   ((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("NOT_IN_DART1_OF_FAN", [NOT_IN_DART1_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((((use_arg_then2 ("x_in", [])) (disch_tac [])) THEN (clear_assumption "x_in") THEN BETA_TAC) THEN (((((use_arg_then2 ("d1_fan", [d1_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["x'"])) THEN (case THEN (move ["v"])) THEN (case THEN (move ["w"])) THEN (case THEN (move ["w1"])) THEN (case THEN (move ["h"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))));
   ((((use_arg_then2 ("e_fan", [e_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_fan", [n_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f1_fan", [f1_fan]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("contracted_dart", [contracted_dart]))(thm_tac (new_rewrite [] []))))));
   ((((use_arg_then2 ("e_fan_pair_ext", [e_fan_pair_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_fan_pair_ext", [n_fan_pair_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_fan_pair_ext", [f_fan_pair_ext]))(thm_tac (new_rewrite [] [])))));
   ((fun arg_tac -> arg_tac (Arg_term (`v,w IN dart1_of_fan (V,E)`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac)))));
   (((((use_arg_then2 ("dart1_of_fan", [dart1_of_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (((use_arg_then2 ("v", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("w", [])) (term_tac exists_tac))) THEN (done_tac));
   ((((use_arg_then2 ("e_fan_pair", [e_fan_pair]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_fan_pair", [n_fan_pair]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_fan_pair", [f_fan_pair]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
   (((((use_arg_then2 ("Fan_misc.INVERSE_SIGMA_FAN_EQ_INVERSE1_SIGMA_FAN", [Fan_misc.INVERSE_SIGMA_FAN_EQ_INVERSE1_SIGMA_FAN]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Collect_geom.PER_SET2)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma fan_hypermaps_iso *)
let fan_hypermaps_iso = Sections.section_proof []
`(hypermap1_of_fanx (vec 0,V,E)) iso (hypermap_of_fan (V,E))`
[
   (((fun arg_tac -> (use_arg_then2 ("hyp_iso_imp_iso", [hyp_iso_imp_iso])) (fun fst_arg -> (use_arg_then2 ("fan_hypermaps_iso_explicit", [fan_hypermaps_iso_explicit])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (exact_tac));
];;
let ext_dart = new_definition 
	`ext_dart (V,E) (v,w) = (vec 0,v,w,extension_sigma_fan (vec 0) V E v w)`;;
(* Lemma ext_dart_eq_inv_contracted_dart *)
let ext_dart_eq_inv_contracted_dart = Sections.section_proof ["d"]
`d IN dart_of_fan (V,E)
	==> ext_dart (V,E) d = res_inv contracted_dart (d_fan (vec 0,V,E)) d`
[
   ((((use_arg_then2 ("d", [])) (disch_tac [])) THEN (clear_assumption "d") THEN case THEN (move ["v"]) THEN (move ["w"])) THEN ((((use_arg_then2 ("ext_dart", [ext_dart]))(thm_tac (new_rewrite [] [])))) THEN (move ["vw_in"])));
   ((fun arg_tac -> arg_tac (Arg_term (`extension_sigma_fan _ V E v w`))) (term_tac (set_tac "w1")));
   ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`(v,w) = contracted_dart (vec 0:real^3,v,w,w1:real^3)`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((((use_arg_then2 ("contracted_dart", [contracted_dart]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
   (((((use_arg_then2 ("res_inv_left", [res_inv_left]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN ((THENL) (split_tac) [((move ["x"]) THEN (move ["y"]) THEN (move ["h"])); ALL_TAC]));
   ((use_arg_then2 ("bij_contracted_dart", [bij_contracted_dart])) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
   ((((((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["_"])) THEN (move ["h2"]) THEN (move ["_"])) THEN (((use_arg_then2 ("h2", [])) (disch_tac [])) THEN (clear_assumption "h2") THEN (DISCH_THEN apply_tac)) THEN (done_tac));
   ((((use_arg_then2 ("w1_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("extension_sigma_fan", [extension_sigma_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_fan", [d_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] [])))));
   (((fun arg_tac -> arg_tac (Arg_term (`w IN set_of_edge v V E`))) (disch_eq_tac "w_in" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
   (((((use_arg_then2 ("d1_fan", [d1_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (DISJ1_TAC));
   ((((fun arg_tac -> arg_tac (Arg_term (`vec 0`))) (term_tac exists_tac)) THEN ((use_arg_then2 ("v", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("w", [])) (term_tac exists_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan (vec 0) V E v w`))) (term_tac exists_tac))) THEN (simp_tac));
   ((((fun arg_tac -> (use_arg_then2 ("properties_of_set_of_edge_fan", [properties_of_set_of_edge_fan])) (fun fst_arg -> (use_arg_then2 ("fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
   (((((use_arg_then2 ("d20_fan", [d20_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (DISJ2_TAC));
   ((((fun arg_tac -> arg_tac (Arg_term (`vec 0`))) (term_tac exists_tac)) THEN ((use_arg_then2 ("v", [])) (term_tac exists_tac))) THEN (simp_tac));
   ((((use_arg_then2 ("vw_in", [])) (disch_tac [])) THEN (clear_assumption "vw_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("dart_of_fan", [dart_of_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN case);
   ((BETA_TAC THEN (case THEN (move ["v'"]))) THEN (((((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN", [IN]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["h"])) THEN (move ["eq"])));
   ((repeat_tactic 1 9 (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (BETA_TAC THEN (case THEN (move ["v'"])) THEN (case THEN (move ["w'"])));
   (((((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("properties_of_set_of_edge_fan", [properties_of_set_of_edge_fan])) (fun fst_arg -> (use_arg_then2 ("fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["h"])) THEN (move ["eq"]));
   ((((use_arg_then2 ("w_in", [])) (disch_tac [])) THEN (clear_assumption "w_in") THEN BETA_TAC) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma fan_hypermaps_iso_explicit2 *)
let fan_hypermaps_iso_explicit2 = Sections.section_proof []
`hyp_iso (ext_dart (V,E)) (hypermap_of_fan (V,E),hypermap1_of_fanx (vec 0,V,E))`
[
   ((fun arg_tac -> (use_arg_then2 ("hyp_iso_inv", [hyp_iso_inv])) (fun fst_arg -> (use_arg_then2 ("fan_hypermaps_iso_explicit", [fan_hypermaps_iso_explicit])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["iso"])));
   (((fun arg_tac -> (use_arg_then2 ("hyp_iso_ext", [hyp_iso_ext])) (fun fst_arg -> (use_arg_then2 ("iso", [iso])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
   (((((use_arg_then2 ("hypermap_of_fan_rep_alt", [hypermap_of_fan_rep_alt]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (move ["d"]) THEN (move ["d_in"]));
   ((((use_arg_then2 ("ext_dart_eq_inv_contracted_dart", [ext_dart_eq_inv_contracted_dart]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma fan_hypermaps_iso2 *)
let fan_hypermaps_iso2 = Sections.section_proof []
`(hypermap_of_fan (V,E)) iso (hypermap1_of_fanx (vec 0,V,E))`
[
   (((fun arg_tac -> (use_arg_then2 ("hyp_iso_imp_iso", [hyp_iso_imp_iso])) (fun fst_arg -> (use_arg_then2 ("fan_hypermaps_iso_explicit2", [fan_hypermaps_iso_explicit2])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (exact_tac));
];;

(* Finalization of the section Iso *)
let bij_contracted_dart = Sections.finalize_theorem bij_contracted_dart;;
let hypermap_of_fan_rep_alt = Sections.finalize_theorem hypermap_of_fan_rep_alt;;
let fan_hypermaps_iso_explicit = Sections.finalize_theorem fan_hypermaps_iso_explicit;;
let fan_hypermaps_iso = Sections.finalize_theorem fan_hypermaps_iso;;
let ext_dart_eq_inv_contracted_dart = Sections.finalize_theorem ext_dart_eq_inv_contracted_dart;;
let fan_hypermaps_iso_explicit2 = Sections.finalize_theorem fan_hypermaps_iso_explicit2;;
let fan_hypermaps_iso2 = Sections.finalize_theorem fan_hypermaps_iso2;;
Sections.end_section "Iso";;

(* Finalization of the section FanHypermapsIso *)
let fan_in_e_imp_neq = Sections.finalize_theorem fan_in_e_imp_neq;;
let in_set_of_edge_neq = Sections.finalize_theorem in_set_of_edge_neq;;
let dart_of_fan_eq = Sections.finalize_theorem dart_of_fan_eq;;
let darts_of_fan_disj = Sections.finalize_theorem darts_of_fan_disj;;
let dart1_of_fan_eq_image = Sections.finalize_theorem dart1_of_fan_eq_image;;
let dart2_of_fan_eq_image = Sections.finalize_theorem dart2_of_fan_eq_image;;
let disjoint_preimage = Sections.finalize_theorem disjoint_preimage;;
let darts_of_fan_disj1 = Sections.finalize_theorem darts_of_fan_disj1;;
let bij_contracted_dart1 = Sections.finalize_theorem bij_contracted_dart1;;
let bij_contracted_dart2 = Sections.finalize_theorem bij_contracted_dart2;;
let bij_contracted_dart = Sections.finalize_theorem bij_contracted_dart;;
let hypermap_of_fan_rep_alt = Sections.finalize_theorem hypermap_of_fan_rep_alt;;
let fan_hypermaps_iso_explicit = Sections.finalize_theorem fan_hypermaps_iso_explicit;;
let fan_hypermaps_iso = Sections.finalize_theorem fan_hypermaps_iso;;
let ext_dart_eq_inv_contracted_dart = Sections.finalize_theorem ext_dart_eq_inv_contracted_dart;;
let fan_hypermaps_iso_explicit2 = Sections.finalize_theorem fan_hypermaps_iso_explicit2;;
let fan_hypermaps_iso2 = Sections.finalize_theorem fan_hypermaps_iso2;;
Sections.end_section "FanHypermapsIso";;

(* Close the module *)
end;;