needs "tame/ssreflect/tame_lemmas-compiled.hl";;

(* Module Rnsyjxm*)
module Rnsyjxm = struct

open Localization;;
open Tame_defs;;
open Ssrbool;;
open Ssrnat;;
open Hypermap_and_fan;;
open Fan_defs;;
open Hypermap;;
open Add_triangle;;
open Tame_general;;
open Hypermap_iso;;
open Wrgcvdr_cizmrrh;;

(* Lemma localization_set_of_edge_subset *)
let localization_set_of_edge_subset = Sections.section_proof ["V";"E";"f";"v"]
`set_of_edge v (v_prime V f) (e_prime E f) SUBSET set_of_edge v V E`
[
   ((((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("set_of_edge", [set_of_edge]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("e_prime", [e_prime]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("v_prime", [v_prime]))(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));
   ((BETA_TAC THEN (move ["u"]) THEN (case THEN ALL_TAC) THEN (case THEN (move ["x"])) THEN (case THEN (move ["w"])) THEN (case THEN (move ["h"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma in_face_imp_in_dart *)
let in_face_imp_in_dart = Sections.section_proof ["x";"H";"d"]
`x IN dart H /\ d IN face H x ==> d IN dart H`
[
   (BETA_TAC THEN (case THEN ((move ["x_in"]) THEN (move ["d_in"]))));
   (((((use_arg_then2 ("lemma_in_face_set", [lemma_in_face_set]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("lemma_face_identity", [lemma_face_identity])) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("lemma_in_face_set", [lemma_in_face_set]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Lemma in_face_imp_in_dart_alt *)
let in_face_imp_in_dart_alt = Sections.section_proof ["H";"f";"d"]
`f IN face_set H /\ d IN f ==> d IN dart H`
[
   (BETA_TAC THEN (case THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_face_representation", [lemma_face_representation])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (case THEN (move ["x"])) THEN (case THEN (move ["x_in"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (move ["d_in"]));
   ((((fun arg_tac -> (use_arg_then2 ("in_face_imp_in_dart", [in_face_imp_in_dart])) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma face_face_map_eq *)
let face_face_map_eq = Sections.section_proof ["H";"d"]
`face H (face_map H d) = face H d`
[
   ((((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] [])))) THEN ((use_arg_then2 ("lemma_face_identity", [lemma_face_identity])) (thm_tac apply_tac)) THEN ((((use_arg_then2 ("face", [face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("in_orbit_map1", [in_orbit_map1]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Section Fan *)
Sections.begin_section "Fan";;
(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 "fanV" (`FAN (vec 0,V,E)`));;

(* Let dartH *)
Sections.add_section_lemma "dartH" (Sections.section_proof []
`dart (hypermap_of_fan (V,E)) = dart_of_fan (V,E)`
[
   ((((use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
]);;

(* Let in_dart_inV *)
Sections.add_section_lemma "in_dart_inV" (Sections.section_proof ["d"]
`d IN dart_of_fan (V,E) ==> FST d IN V /\ SND d IN V`
[
   (((((use_arg_then2 ("pair_expand", [pair_expand]))(thm_tac (new_rewrite [1] [])))) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (done_tac));
]);;

(* Lemma card_set_of_edge_gt1_imp_in_dart1 *)
let card_set_of_edge_gt1_imp_in_dart1 = Sections.section_proof ["v";"w"]
`v,w IN dart_of_fan (V,E)
	/\ CARD (set_of_edge v V E) > 1 ==> v,w IN dart1_of_fan (V,E)`
[
   (BETA_TAC THEN (case THEN ((move ["vw_in"]) THEN (move ["card_gt1"]))));
   ((((use_arg_then2 ("vw_in", [])) (disch_tac [])) THEN (clear_assumption "vw_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("dart_of_fan_eq", [dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] []))))) THEN (case THEN ((TRY done_tac))));
   (((((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["z"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["z_in"])) THEN (move ["eq1"]) THEN (move ["eq2"]));
   ((((use_arg_then2 ("card_gt1", [])) (disch_tac [])) THEN (clear_assumption "card_gt1") THEN BETA_TAC) THEN ((((use_arg_then2 ("eq2", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("CARD_CLAUSES", [CARD_CLAUSES]))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
];;

(* Lemma azim_in_fan_eq_azim_dart *)
let azim_in_fan_eq_azim_dart = Sections.section_proof ["d"]
`d IN dart_of_fan (V,E)
	==> azim_in_fan d E = azim_dart (V,E) d`
[
   (((use_arg_then2 ("d", [])) (disch_tac [])) THEN (clear_assumption "d") THEN case THEN (move ["v"]) THEN (move ["w"]) THEN (move ["vw_in"]));
   ((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE azim_in_fan)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("azim_dart_eq_azim_fan", [azim_dart_eq_azim_fan]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("azim_fan", [azim_fan]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("EE_elim", [EE_elim])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
   (((fun arg_tac -> arg_tac (Arg_term (`_ > 1`))) (disch_eq_tac "ineq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
   ((((fun arg_tac -> (use_arg_then2 ("AZIM_CYCLE_EQ_SIGMA_FAN_ALT", [AZIM_CYCLE_EQ_SIGMA_FAN_ALT])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
   ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("card_set_of_edge_gt1_imp_in_dart1", [card_set_of_edge_gt1_imp_in_dart1])) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("ineq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART1_OF_FAN", [PAIR_IN_DART1_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma wedge_in_fan_gt_eq_w_dart_fan *)
let wedge_in_fan_gt_eq_w_dart_fan = Sections.section_proof ["d"]
`d IN dart1_of_fan (V,E)
	==> wedge_in_fan_gt d E = w_dart_fan (vec 0) V E (ext_dart (V,E) d)`
[
   (((use_arg_then2 ("d", [])) (disch_tac [])) THEN (clear_assumption "d") THEN case THEN (move ["v"]) THEN (move ["w"]) THEN (move ["vw_in"]));
   ((((use_arg_then2 ("wedge_in_fan_gt", [wedge_in_fan_gt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ext_dart", [ext_dart]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w_dart_fan", [w_dart_fan]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("EE_elim", [EE_elim])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
   ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART1_OF_FAN", [PAIR_IN_DART1_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["_"]) THEN (case THEN (move ["_"])) THEN (case THEN (move ["w_inE"])) THEN (move ["_"])))));
   (((fun arg_tac -> arg_tac (Arg_term (`CARD _ > 1`))) (disch_eq_tac "ineq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
   ((((fun arg_tac -> (use_arg_then2 ("AZIM_CYCLE_EQ_SIGMA_FAN_ALT", [AZIM_CYCLE_EQ_SIGMA_FAN_ALT])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
   (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`set_of_edge v V E = {w}`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac))))));
   (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_DIFF", [IN_DIFF]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNIV", [IN_UNIV]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((((use_arg_then2 ("ineq", [])) (disch_tac [])) THEN (clear_assumption "ineq") THEN BETA_TAC) THEN ((((use_arg_then2 ("gtE", [gtE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("NOT_LT", [NOT_LT]))(thm_tac (new_rewrite [] []))))));
   ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("finite_set_of_edge", [finite_set_of_edge])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("v", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["finE"])));
   ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`x <= 1 <=> x = 0 \/ x = 1`))) (term_tac (have_gen_tac ["x"](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((arith_tac) THEN (done_tac)));
   ((THENL_FIRST) case ((((((use_arg_then2 ("CARD_EQ_0", [CARD_EQ_0]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (move ["eq"])) THEN (((use_arg_then2 ("w_inE", [])) (disch_tac [])) THEN (clear_assumption "w_inE") THEN BETA_TAC) THEN ((((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("NOT_IN_EMPTY", [NOT_IN_EMPTY]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
   ((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("Rogers.CARD_1_IMP_SING", [Rogers.CARD_1_IMP_SING])) (fun fst_arg -> (use_arg_then2 ("finE", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (case THEN (move ["x"])) THEN (move ["eq"]));
   ((((use_arg_then2 ("w_inE", [])) (disch_tac [])) THEN (clear_assumption "w_inE") THEN BETA_TAC) THEN (((((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SING", [IN_SING]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma localization_dart_eq_dart1 *)
let localization_dart_eq_dart1 = Sections.section_proof ["f"]
`f IN face_set (hypermap_of_fan (V,E))
	/\ 2 <= CARD f
	==> dart_of_fan (v_prime V f, e_prime E f) = dart1_of_fan (v_prime V f, e_prime E f)`
[
   (BETA_TAC THEN (case THEN ((move ["f_in"]) THEN (move ["card_f"]))));
   ((((((use_arg_then2 ("dart_of_fan_eq", [dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] []))))) THEN (move ["d"])) THEN ((THENL) (split_tac) [((case THEN ALL_TAC) THEN ((TRY done_tac))); ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)))]));
   (((((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (((use_arg_then2 ("contraLR", [contraLR])) (disch_tac [])) THEN (clear_assumption "contraLR") THEN (DISCH_THEN apply_tac) THEN (move ["_"])));
   (((((use_arg_then2 ("NOT_EXISTS_THM", [NOT_EXISTS_THM]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("negb_and", [negb_and]))(thm_tac (new_rewrite [] [])))))) THEN (move ["v"]));
   ((((fun arg_tac -> arg_tac (Arg_term (`v IN _`))) (disch_eq_tac "v_in" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) THEN (DISJ1_TAC));
   ((((use_arg_then2 ("v_in", [])) (disch_tac [])) THEN (clear_assumption "v_in") THEN BETA_TAC) THEN (((((use_arg_then2 ("v_prime", [v_prime]))(thm_tac (new_rewrite [1] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["v_in"])) THEN (case THEN (move ["w"])) THEN (move ["vw_in_f"])));
   ((((use_arg_then2 ("MEMBER_NOT_EMPTY", [MEMBER_NOT_EMPTY]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("w", [])) (term_tac exists_tac)));
   ((((use_arg_then2 ("f_in", [])) (disch_tac [])) THEN (clear_assumption "f_in") THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_face_representation", [lemma_face_representation])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (case THEN (move ["x"]))) THEN ((((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["x_in"])) THEN (move ["f_eq"])));
   ((fun arg_tac -> arg_tac (Arg_term (`x IN dart1_of_fan (V,E)`))) (term_tac (have_gen_tac [](move ["x_in1"]))));
   (((use_arg_then2 ("card_f", [])) (disch_tac [])) THEN (clear_assumption "card_f") THEN ((use_arg_then2 ("contraLR", [contraLR])) (disch_tac [])) THEN (clear_assumption "contraLR") THEN (DISCH_THEN apply_tac) THEN (move ["x_not_in"]));
   (((((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("E_N_F_DEGENERATE_CASE", [E_N_F_DEGENERATE_CASE]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("CARD_SINGLETON", [CARD_SINGLETON]))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
   ((fun arg_tac -> arg_tac (Arg_term (`v,w IN dart1_of_fan (V,E)`))) (term_tac (have_gen_tac [](move ["vw_in1"]))));
   ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("FACE_SUBSET_DART1_OF_FAN", [FACE_SUBSET_DART1_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("x_in1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
   (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("IN_TRANS", [IN_TRANS])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (DISCH_THEN apply_tac)) THEN (((use_arg_then2 ("f_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (((((use_arg_then2 ("set_of_edge", [set_of_edge]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_prime", [e_prime]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (split_tac));
   ((((use_arg_then2 ("v", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("w", [])) (term_tac exists_tac))) THEN (((fun arg_tac -> (use_arg_then2 ("inE_eq_in_dart1", [inE_eq_in_dart1])) (fun fst_arg -> (use_arg_then2 ("V", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
   ((((use_arg_then2 ("v_prime", [v_prime]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART1_OF_FAN", [PAIR_IN_DART1_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("vw_in1", [])) (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 [] [])))));
   ((fun arg_tac -> arg_tac (Arg_term (`SND (f_fan_pair (V,E) (v,w))`))) (term_tac exists_tac));
   (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`w, SND (f_fan_pair (V,E) (v,w)) = face_map (hypermap_of_fan (V,E)) (v,w)`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))));
   (in_tac ["vw_in_f"] false (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))));
   (((((use_arg_then2 ("POWER_1", [POWER_1]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("lemma_face_identity", [lemma_face_identity])) (fun fst_arg -> (use_arg_then2 ("vw_in_f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("lemma_in_face", [lemma_in_face]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (((((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_fan_pair_ext", [f_fan_pair_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("vw_in1", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("f_fan_pair", [f_fan_pair]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma localization_dart1_subset *)
let localization_dart1_subset = Sections.section_proof ["f";"d"]
`d IN dart1_of_fan (v_prime V f, e_prime E f) ==> d IN dart1_of_fan (V,E)`
[
   (((use_arg_then2 ("d", [])) (disch_tac [])) THEN (clear_assumption "d") THEN case THEN (move ["v"]) THEN (move ["w"]));
   ((repeat_tactic 1 9 (((use_arg_then2 ("inE_eq_in_dart1", [inE_eq_in_dart1]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((fun arg_tac -> arg_tac (Arg_term (`{v,w}`))) (disch_tac [])) THEN BETA_TAC) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(gsym_then (thm_tac (new_rewrite [] []))))));
   ((use_arg_then2 ("Wrgcvdr_cizmrrh.E_PRIME_SUBSET_E", [Wrgcvdr_cizmrrh.E_PRIME_SUBSET_E])) (thm_tac apply_tac));
];;

(* Lemma localization_node_subset *)
let localization_node_subset = Sections.section_proof ["f";"d"]
`f IN face_set (hypermap_of_fan (V,E))
	==> node (hypermap_of_fan (v_prime V f, e_prime E f)) d 
		SUBSET node (hypermap_of_fan (V,E)) d`
[
   (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_face_representation", [lemma_face_representation])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (case THEN (move ["x"]))) THEN ((((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["x_in"])) THEN (move ["f_eq"])));
   ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Wrgcvdr_cizmrrh.IMP_FAN_V_PRIME_E_PRIME))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (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))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
   ((THENL_FIRST) (((((use_arg_then2 ("hypermap_HYP_elim", [hypermap_HYP_elim]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN (ANTS_TAC)) (((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN (done_tac)));
   (BETA_TAC THEN (move ["fan'"]));
   ((THENL_ROT (-1)) (((fun arg_tac -> arg_tac (Arg_term (`d IN dart1_of_fan (V,E)`))) (disch_eq_tac "d_in1" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)));
   ((repeat_tactic 1 9 (((use_arg_then2 ("E_N_F_DEGENERATE_CASE", [E_N_F_DEGENERATE_CASE]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("SUBSET_REFL", [SUBSET_REFL]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("fan'", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))));
   ((((use_arg_then2 ("d_in1", [])) (disch_tac [])) THEN (clear_assumption "d_in1") THEN ((use_arg_then2 ("contra", [contra])) (disch_tac [])) THEN (clear_assumption "contra") THEN (DISCH_THEN apply_tac) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("localization_dart1_subset", [localization_dart1_subset])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (done_tac));
   (((use_arg_then2 ("d_in1", [])) (disch_tac [])) THEN (clear_assumption "d_in1") THEN ((use_arg_then2 ("d", [])) (disch_tac [])) THEN (clear_assumption "d") THEN case THEN (move ["v"]) THEN (move ["w"]) THEN (move ["vw_in1"]));
   ((THENL_ROT (-1)) (((fun arg_tac -> arg_tac (Arg_term (`v,w IN dart1_of_fan (v_prime V f, e_prime E f)`))) (disch_eq_tac "vw_in1'" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)));
   (((((use_arg_then2 ("E_N_F_DEGENERATE_CASE", [E_N_F_DEGENERATE_CASE]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("SING_SUBSET", [SING_SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("node_refl", [node_refl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (((repeat_tactic 1 9 (((use_arg_then2 ("NODE_HYPERMAP_OF_FAN_ALT", [NODE_HYPERMAP_OF_FAN_ALT]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((move ["a"]) THEN (move ["b"]))));
   (((repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["u"])) THEN (case THEN (move ["u_in"])) THEN (move ["eqs"]));
   (((use_arg_then2 ("u", [])) (term_tac exists_tac)) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("eqs", []))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)));
   ((((fun arg_tac -> (use_arg_then2 ("IN_TRANS", [IN_TRANS])) (fun fst_arg -> (use_arg_then2 ("u_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)) THEN (((use_arg_then2 ("localization_set_of_edge_subset", [localization_set_of_edge_subset]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma f_fan_pair_ext_in_dart1 *)
let f_fan_pair_ext_in_dart1 = Sections.section_proof ["d"]
`d IN dart1_of_fan (V,E) ==> 
	f_fan_pair_ext (V,E) d IN dart1_of_fan (V,E)`
[
   ((BETA_TAC THEN (move ["d_in"])) THEN ((((use_arg_then2 ("f_fan_pair_ext", [f_fan_pair_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("E_N_F_IN_DART1_OF_FAN", [E_N_F_IN_DART1_OF_FAN]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma localization_simple_hypermap *)
let localization_simple_hypermap = Sections.section_proof ["f"]
`f IN face_set (hypermap_of_fan (V,E))
	/\ 2 <= CARD f
	/\ simple_hypermap (hypermap_of_fan (V,E))
	==> simple_hypermap (hypermap_of_fan (v_prime V f, e_prime E f))`
[
   (((repeat_tactic 1 9 (((use_arg_then2 ("simple_hypermap", [simple_hypermap]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["f_in"])) THEN (case THEN (move ["card_f"])) THEN (move ["simpleH"]));
   ((((use_arg_then2 ("f_in", [])) (disch_tac [])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_face_representation", [lemma_face_representation])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (case THEN (case THEN ((move ["v"]) THEN (move ["w"]))))) THEN ((((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["vw_in"])) THEN (move ["f_eq"])));
   ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Lvducxu.LVDUCXU))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (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))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
   ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL IMP_FAN_V_PRIME_E_PRIME))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (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))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
   ((THENL_FIRST) (((((use_arg_then2 ("hypermap_HYP_elim", [hypermap_HYP_elim]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN (ANTS_TAC)) (((fun arg_tac -> arg_tac (Arg_term (`v,w`))) (term_tac exists_tac)) THEN (done_tac)));
   (BETA_TAC THEN (move ["fan'"]));
   ((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))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["dartH'"]) THEN (move ["_"])))));
   (((((use_arg_then2 ("hypermap_HYP_elim", [hypermap_HYP_elim]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("darts_of_hyp_elim", [darts_of_hyp_elim]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN ((fun arg_tac ->  (conv_thm_tac DISCH_THEN)  (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac MP_TAC)));
   ((THENL_FIRST) (ANTS_TAC) ((((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
   (BETA_TAC THEN (case THEN (move ["ff_eq"])) THEN (move ["_"]));
   ((((use_arg_then2 ("dartH'", []))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN ((move ["a"]) THEN (move ["b"]))) THEN (move ["ab_in"]));
   ((((use_arg_then2 ("ab_in", [])) (disch_tac [])) THEN BETA_TAC) THEN (((((use_arg_then2 ("localization_dart_eq_dart1", [localization_dart_eq_dart1]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (move ["ab_in1"])));
   ((THENL_ROT (-1)) ((((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SING", [IN_SING]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((move ["x"]) THEN (move ["y"])))) THEN (split_tac)));
   ((BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((((use_arg_then2 ("node_refl", [node_refl]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("face_refl", [face_refl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (BETA_TAC THEN (case THEN (move ["xy_in_n"])) THEN (move ["xy_in_f"]));
   ((fun arg_tac -> arg_tac (Arg_term (`d IN f ==> d IN dart_of_fan (V,E)`))) (term_tac (have_gen_tac ["d"](move ["in_f_in_dart"]))));
   (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("IN_TRANS", [IN_TRANS])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FACE_SUBSET_DART_OF_FAN", [FACE_SUBSET_DART_OF_FAN]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((fun arg_tac -> arg_tac (Arg_term (`d IN dart_of_fan (v_prime V f, e_prime E f) ==> d IN f \/ SND d, FST d IN f`))) (term_tac (have_gen_tac ["d"](move ["dart_or"]))));
   (((((use_arg_then2 ("localization_dart_eq_dart1", [localization_dart_eq_dart1]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (((use_arg_then2 ("d", [])) (disch_tac [])) THEN (clear_assumption "d") THEN case THEN (move ["u"]) THEN (move ["z"])));
   ((((use_arg_then2 ("inE_eq_in_dart1", [inE_eq_in_dart1]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("e_prime", [e_prime]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
   ((BETA_TAC THEN (case THEN (move ["x'"])) THEN (case THEN (move ["y'"])) THEN (case THEN (move ["xy'_in"]))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Geomdetail.PAIR_EQ_EXPAND)))(thm_tac (new_rewrite [] [])))));
   ((case 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));
   (((fun arg_tac -> (use_arg_then2 ("dart_or", [])) (fun fst_arg -> (use_arg_then2 ("ab_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (simp_tac));
   (((fun arg_tac -> arg_tac (Arg_term (`a,b IN f`))) (disch_eq_tac "ab_in_f" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
   (((fun arg_tac -> (use_arg_then2 ("simpleH", [])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("in_f_in_dart", [])) (fun fst_arg -> (use_arg_then2 ("ab_in_f", [])) (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);
   (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SING", [IN_SING]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))));
   ((((fun arg_tac -> (use_arg_then2 ("lemma_face_identity", [lemma_face_identity])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`v,w`))) (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 ("f_eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("ff_eq", []))(thm_tac (new_rewrite [] [])))));
   ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("lemma_face_identity", [lemma_face_identity])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`v,w`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`a,b`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("ff_eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("xy_in_f", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))));
   ((((fun arg_tac -> (use_arg_then2 ("IN_TRANS", [IN_TRANS])) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("localization_node_subset", [localization_node_subset])) (fun fst_arg -> (use_arg_then2 ("f_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`a,b`))) (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));
   (BETA_TAC THEN (move ["ba_in_f"]));
   ((fun arg_tac -> arg_tac (Arg_term (`x = a`))) (term_tac (have_gen_tac [](move ["x_eq_a"]))));
   ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fst_node_hypermap_of_fan", [fst_node_hypermap_of_fan])) (fun fst_arg -> (use_arg_then2 ("fan'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("xy_in_n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (done_tac));
   ((in_tac ["xy_in_f"] true ((((use_arg_then2 ("x_eq_a", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("x_eq_a", [])) (disch_tac [])) THEN (clear_assumption "x_eq_a") THEN ((use_arg_then2 ("xy_in_n", [])) (disch_tac [])) THEN (clear_assumption "xy_in_n") THEN BETA_TAC THEN (move ["_"]) THEN (move ["_"]) THEN (simp_tac)));
   ((fun arg_tac -> arg_tac (Arg_term (`a,y IN dart_of_fan (v_prime V f,e_prime E f)`))) (term_tac (have_gen_tac [](move ["ay_in'"]))));
   (((((fun arg_tac -> (use_arg_then2 ("IN_TRANS", [IN_TRANS])) (fun fst_arg -> (use_arg_then2 ("xy_in_f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FACE_SUBSET_DART_OF_FAN", [FACE_SUBSET_DART_OF_FAN]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((fun arg_tac -> arg_tac (Arg_term (`y,a IN f`))) (term_tac (have_gen_tac [](move ["ya_in_f"]))));
   (((use_arg_then2 ("ay_in'", [])) (disch_tac [])) THEN (clear_assumption "ay_in'") THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("dart_or", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN case THEN (simp_tac) THEN (move ["ay_in_f2"]));
   (((use_arg_then2 ("xy_in_f", [])) (disch_tac [])) THEN (clear_assumption "xy_in_f") THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_face_identity", [lemma_face_identity])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC);
   (((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("lemma_face_identity", [lemma_face_identity])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`v,w`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`a,y`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("ff_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (move ["eq1"]));
   ((((use_arg_then2 ("ab_in_f", [])) (disch_tac [])) THEN (clear_assumption "ab_in_f") THEN BETA_TAC) THEN ((((use_arg_then2 ("ff_eq", []))(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_different_faces", [lemma_different_faces])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN ((((use_arg_then2 ("eq1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ff_eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
   (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`f_fan_pair_ext (V,E) (y,a) = f_fan_pair_ext (V,E) (b,a)`))) (term_tac (have_gen_tac []ALL_TAC))));
   (((((fun arg_tac -> (use_arg_then2 ("PERMUTES_INJECTIVE", [PERMUTES_INJECTIVE])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("F_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN", [F_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (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 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((fun arg_tac -> arg_tac (Arg_term (`_1 _2 (y,a)`))) (term_tac (set_tac "d1")));
   ((fun arg_tac -> arg_tac (Arg_term (`_1 _2 (b,a)`))) (term_tac (set_tac "d2")));
   ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`{d1} = {d2}`))) (term_tac (have_gen_tac []ALL_TAC)))) ((((use_arg_then2 ("SING_EQ", [SING_EQ]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
   ((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["_"]) THEN (case THEN (move ["_"])) THEN (case THEN (move ["_"])) THEN (move ["fH"])))));
   ((fun arg_tac -> arg_tac (Arg_term (`y,a IN dart1_of_fan (V,E) /\ b,a IN dart1_of_fan (V,E)`))) (term_tac (have_gen_tac [](case THEN ((move ["ya_in1"]) THEN (move ["ba_in1"]))))));
   ((split_tac) THEN (((use_arg_then2 ("dart1_switch", [dart1_switch]))(thm_tac (new_rewrite [] [])))));
   ((((use_arg_then2 ("ay_in'", [])) (disch_tac [])) THEN (clear_assumption "ay_in'") THEN BETA_TAC) THEN (((((use_arg_then2 ("localization_dart_eq_dart1", [localization_dart_eq_dart1]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("localization_dart1_subset", [localization_dart1_subset])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((((use_arg_then2 ("ab_in1", [])) (disch_tac [])) THEN (clear_assumption "ab_in1") THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("localization_dart1_subset", [localization_dart1_subset])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((fun arg_tac -> arg_tac (Arg_term (`d1 IN dart1_of_fan (V,E) /\ d2 IN dart1_of_fan (V,E)`))) (term_tac (have_gen_tac [](case THEN ((move ["d1_in1"]) THEN (move ["d2_in1"]))))));
   (((((use_arg_then2 ("d1_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("d2_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("f_fan_pair_ext_in_dart1", [f_fan_pair_ext_in_dart1]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
   ((fun arg_tac -> arg_tac (Arg_term (`d1 IN dart_of_fan (V,E) /\ d2 IN dart_of_fan (V,E)`))) (term_tac (have_gen_tac [](case THEN ((move ["d1_in"]) THEN (move ["d2_in"]))))));
   (((((use_arg_then2 ("dart_of_fan_eq", [dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("d1_in1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d2_in1", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (((((fun arg_tac -> (use_arg_then2 ("simpleH", [])) (fun fst_arg -> (use_arg_then2 ("d1_in", [])) (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 ("simpleH", [])) (fun fst_arg -> (use_arg_then2 ("d2_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (congr_tac (`_1 INTER _2`)));
   (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("HYPERMAP_OF_FAN_NODE_EQ", [HYPERMAP_OF_FAN_NODE_EQ])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d1_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d2_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
   (((((use_arg_then2 ("d1_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("d2_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("f_fan_pair_ext", [f_fan_pair_ext]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("ya_in1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ba_in1", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("f_fan_pair", [f_fan_pair]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
   ((((use_arg_then2 ("d1_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("d2_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("fH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("face_face_map_eq", [face_face_map_eq]))(thm_tac (new_rewrite [] []))))));
   ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("lemma_face_identity", [lemma_face_identity])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`v,w`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`y,a`))) (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 ("f_eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((TRY done_tac)));
   (((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("lemma_face_identity", [lemma_face_identity])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`v,w`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`b,a`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Finalization of the section Fan *)
let card_set_of_edge_gt1_imp_in_dart1 = Sections.finalize_theorem card_set_of_edge_gt1_imp_in_dart1;;
let azim_in_fan_eq_azim_dart = Sections.finalize_theorem azim_in_fan_eq_azim_dart;;
let wedge_in_fan_gt_eq_w_dart_fan = Sections.finalize_theorem wedge_in_fan_gt_eq_w_dart_fan;;
let localization_dart_eq_dart1 = Sections.finalize_theorem localization_dart_eq_dart1;;
let localization_dart1_subset = Sections.finalize_theorem localization_dart1_subset;;
let localization_node_subset = Sections.finalize_theorem localization_node_subset;;
let f_fan_pair_ext_in_dart1 = Sections.finalize_theorem f_fan_pair_ext_in_dart1;;
let localization_simple_hypermap = Sections.finalize_theorem localization_simple_hypermap;;
Sections.end_section "Fan";;

(* Section FullySurrounded *)
Sections.begin_section "FullySurrounded";;
(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 "fanV" (`FAN (vec 0,V,E)`));;
(Sections.add_section_hyp "f_surr" (`fully_surrounded (V,E)`));;

(* Let dartH *)
Sections.add_section_lemma "dartH" (Sections.section_proof []
`dart (hypermap_of_fan (V,E)) = dart_of_fan (V,E)`
[
   ((((use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
]);;

(* Let dart1_eq *)
Sections.add_section_lemma "dart1_eq" (Sections.section_proof []
`dart1_of_fan (V,E) = dart_of_fan (V,E)`
[
   ((((use_arg_then2 ("fully_surrounded_dart_of_fan_eq", [fully_surrounded_dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
]);;

(* Lemma fully_surrounded_simple_hypermap *)
let fully_surrounded_simple_hypermap = Sections.section_proof []
`simple_hypermap (hypermap_of_fan (V,E))`
[
   ((fun arg_tac -> (use_arg_then2 ("Hypermap_iso.fan_hypermaps_iso", [Hypermap_iso.fan_hypermaps_iso])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (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 ("Hypermap_iso.iso_simple", [Hypermap_iso.iso_simple])) (fun fst_arg -> (use_arg_then2 ("iso", [iso])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Conforming.SRPRNPL", [Conforming.SRPRNPL]))(thm_tac (new_rewrite [] [])))));
   ((((use_arg_then2 ("fully_surrounded_imp_conforming", [fully_surrounded_imp_conforming]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma f_surr_localization *)
let f_surr_localization = Sections.section_proof ["d"]
`d IN dart_of_fan (V,E)
	==> let f = face (hypermap_of_fan (V,E)) d in
	   local_fan (v_prime V f,e_prime E f,f)
	/\ face (hypermap_of_fan (v_prime V f, e_prime E f)) d = f
	/\ (!x. x IN f ==> azim_dart (V,E) x = azim_dart (v_prime V f, e_prime E f) x)
	/\ (!x. x IN f ==> wedge_in_fan_gt x E = wedge_in_fan_gt x (e_prime E f))
	/\ (!x. x IN f ==> wedge_in_fan_ge x E = wedge_in_fan_ge x (e_prime E f))`
[
   ((((use_arg_then2 ("d", [])) (disch_tac [])) THEN (clear_assumption "d") THEN case THEN (move ["v"]) THEN (move ["w"]) THEN (move ["vw_in"])) THEN (CONV_TAC let_CONV));
   ((fun arg_tac -> arg_tac (Arg_term (`face _1 _2`))) (term_tac (set_tac "f")));
   ((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Lvducxu.LVDUCXU))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (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 -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL IMP_FAN_V_PRIME_E_PRIME))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (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))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
   ((((use_arg_then2 ("darts_of_hyp_elim", [darts_of_hyp_elim]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("hypermap_HYP_elim", [hypermap_HYP_elim]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] [])))));
   ((THENL_FIRST) (ANTS_TAC) (((fun arg_tac -> arg_tac (Arg_term (`v,w`))) (term_tac exists_tac)) THEN (done_tac)));
   ((BETA_TAC THEN (move ["fan'"]) THEN ((fun arg_tac -> (fun arg_tac ->  (conv_thm_tac DISCH_THEN)  (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (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 MP_TAC))) THEN (((use_arg_then2 ("f_def", []))(thm_tac (new_rewrite [] [])))));
   (((((use_arg_then2 ("hypermap_HYP_elim", [hypermap_HYP_elim]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN ((ANTS_TAC) THEN ((TRY done_tac)) THEN (case THEN (move ["f_eq"])) THEN (case THEN (move ["in_f_eq"]))));
   ((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))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["dartH'"]) THEN (move ["_"])))));
   (ANTS_TAC);
   ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("FULLY_SURROUNDED_IMP_CARD_FACE_GE_3", [FULLY_SURROUNDED_IMP_CARD_FACE_GE_3])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["card_ge3"])));
   ((THENL_FIRST) (split_tac) ((((use_arg_then2 ("card_ge3", [])) (disch_tac [])) THEN (clear_assumption "card_ge3") THEN BETA_TAC) THEN (((use_arg_then2 ("f_def", []))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)));
   ((((use_arg_then2 ("localization_simple_hypermap", [localization_simple_hypermap]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fanV", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fully_surrounded_simple_hypermap", [fully_surrounded_simple_hypermap]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
   (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("lemma_in_face_set", [lemma_in_face_set]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("vw_in", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("card_ge3", [])) (disch_tac [])) THEN (clear_assumption "card_ge3") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
   ((BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((((use_arg_then2 ("f_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)));
   ((repeat_tactic 1 9 ((split_tac))) THEN (BETA_TAC THEN (move ["d"]) THEN (move ["d_in_f"])) THEN ((repeat_tactic 0 10 (((use_arg_then2 ("in_f_eq", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))));
   ((fun arg_tac -> arg_tac (Arg_term (`d IN dart_of_fan (V,E)`))) (term_tac (have_gen_tac [](move ["d_in"]))));
   (((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("in_face_imp_in_dart", [in_face_imp_in_dart])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`v,w`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`d IN dart_of_fan (v_prime V f, e_prime E f)`))) (term_tac (have_gen_tac [](move ["d_in'"])))));
   (((((fun arg_tac -> (use_arg_then2 ("azim_in_fan_eq_azim_dart", [azim_in_fan_eq_azim_dart])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("azim_in_fan_eq_azim_dart", [azim_in_fan_eq_azim_dart])) (fun fst_arg -> (use_arg_then2 ("fan'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("in_f_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (((((use_arg_then2 ("dart_of_fan_eq", [dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] []))))) THEN (DISJ1_TAC));
   (((use_arg_then2 ("d_in", [])) (disch_tac [])) THEN (clear_assumption "d_in") THEN ((use_arg_then2 ("d_in_f", [])) (disch_tac [])) THEN (clear_assumption "d_in_f") THEN ((use_arg_then2 ("d", [])) (disch_tac [])) THEN (clear_assumption "d") THEN case THEN (move ["a"]) THEN (move ["b"]) THEN (move ["ab_in_f"]) THEN (move ["ab_in"]));
   ((((use_arg_then2 ("inE_eq_in_dart1", [inE_eq_in_dart1]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("e_prime", [e_prime]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
   ((((use_arg_then2 ("a", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("b", [])) (term_tac exists_tac))) THEN ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("inE_eq_in_dart1", [inE_eq_in_dart1])) (fun fst_arg -> (use_arg_then2 ("V", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("E", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart1_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma f_surr_localization_convex_local *)
let f_surr_localization_convex_local = Sections.section_proof ["d"]
`d IN dart_of_fan (V,E)
	==> let f = face (hypermap_of_fan (V,E)) d in
	   convex_local_fan (v_prime V f,e_prime E f,f)`
[
   ((((use_arg_then2 ("d", [])) (disch_tac [])) THEN (clear_assumption "d") THEN case THEN (move ["v"]) THEN (move ["w"]) THEN (move ["vw_in"])) THEN (CONV_TAC let_CONV));
   ((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE f_surr_localization))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["local"]) THEN (case THEN (move ["f_eq"])) THEN (case THEN (move ["azim_eq"])) THEN (move ["wedge_eq"])))));
   ((((use_arg_then2 ("convex_local_fan", [convex_local_fan]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE f_surr_localization))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (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 [] [])))));
   ((fun arg_tac -> arg_tac (Arg_term (`face _1 _2`))) (term_tac (set_tac "f")));
   ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL IMP_FAN_V_PRIME_E_PRIME))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (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))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
   ((THENL_FIRST) (((((use_arg_then2 ("hypermap_HYP_elim", [hypermap_HYP_elim]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (ANTS_TAC)) (((fun arg_tac -> arg_tac (Arg_term (`v,w`))) (term_tac exists_tac)) THEN (done_tac)));
   (BETA_TAC THEN (move ["fan'"]) THEN (case THEN ((move ["a"]) THEN (move ["b"]))) THEN (move ["ab_in_f"]));
   ((fun arg_tac -> arg_tac (Arg_term (`a,b IN dart_of_fan (V,E)`))) (term_tac (have_gen_tac [](move ["ab_in"]))));
   (((((fun arg_tac -> (use_arg_then2 ("IN_TRANS", [IN_TRANS])) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("FACE_SUBSET_DART_OF_FAN", [FACE_SUBSET_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_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)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_def", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((fun arg_tac -> arg_tac (Arg_term (`v,w IN dart_of_fan (v_prime V f, e_prime E f)`))) (term_tac (have_gen_tac [](move ["vw_in'"]))));
   (((((use_arg_then2 ("dart_of_fan_eq", [dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] []))))) THEN (DISJ1_TAC));
   ((((use_arg_then2 ("inE_eq_in_dart1", [inE_eq_in_dart1]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("e_prime", [e_prime]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
   ((((use_arg_then2 ("v", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("w", [])) (term_tac exists_tac))) THEN ((((fun arg_tac -> (use_arg_then2 ("inE_eq_in_dart1", [inE_eq_in_dart1])) (fun fst_arg -> (use_arg_then2 ("V", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart1_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("vw_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)));
   (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("face_refl", [face_refl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((fun arg_tac -> arg_tac (Arg_term (`a,b IN dart_of_fan (v_prime V f, e_prime E f)`))) (term_tac (have_gen_tac [](move ["ab_in'"]))));
   (((((fun arg_tac -> (use_arg_then2 ("IN_TRANS", [IN_TRANS])) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("FACE_SUBSET_DART_OF_FAN", [FACE_SUBSET_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fan'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_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)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((((fun arg_tac -> (use_arg_then2 ("azim_in_fan_eq_azim_dart", [azim_in_fan_eq_azim_dart])) (fun fst_arg -> (use_arg_then2 ("fan'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("azim_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
   ((THENL_FIRST) (split_tac) ((((use_arg_then2 ("f_surr", [])) (disch_tac [])) THEN (clear_assumption "f_surr") THEN BETA_TAC) THEN ((((use_arg_then2 ("fully_surrounded", [fully_surrounded]))(thm_tac (new_rewrite [] [])))) THEN ((fun arg_tac ->  (conv_thm_tac DISCH_THEN)  (fun fst_arg -> (use_arg_then2 ("ab_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac MP_TAC)) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("REAL_LT_IMP_LE", [REAL_LT_IMP_LE])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (done_tac)));
   (((((use_arg_then2 ("wedge_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("v_prime", [v_prime]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN (move ["x"]) THEN (case THEN (move ["x_inV"])) THEN (case THEN (move ["y"])) THEN (move ["xy_in_f"]));
   ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`a,b IN dart1_of_fan (V,E)`))) (term_tac (have_gen_tac [](move ["ab_in1"])))) ((((use_arg_then2 ("dart1_eq", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
   (((use_arg_then2 ("IN_TRANS", [IN_TRANS])) (thm_tac apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`closure (wedge_in_fan_gt (a,b) E)`))) (term_tac exists_tac)) THEN (split_tac));
   ((((use_arg_then2 ("wedge_in_fan_gt", [wedge_in_fan_gt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("wedge_in_fan_ge", [wedge_in_fan_ge]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("EE_elim", [EE_elim])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
   ((((use_arg_then2 ("fully_surrounded_card_set_of_edge1", [fully_surrounded_card_set_of_edge1]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("ab_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((simp_tac THEN TRY done_tac)));
   ((((use_arg_then2 ("CLOSURE_MINIMAL_EQ", [CLOSURE_MINIMAL_EQ]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("Leaf_cell.WEDGE_SUBSET_WEDGE_GE", [Leaf_cell.WEDGE_SUBSET_WEDGE_GE]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
   ((((use_arg_then2 ("AZIM_CYCLE_EQ_SIGMA_FAN_ALT", [AZIM_CYCLE_EQ_SIGMA_FAN_ALT]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART1_OF_FAN", [PAIR_IN_DART1_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("ab_in1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
   (((((use_arg_then2 ("Leaf_cell.CLOSED_WEDGE", [Leaf_cell.CLOSED_WEDGE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DART1_NOT_COLLINEAR_2", [DART1_NOT_COLLINEAR_2])) (fun fst_arg -> (use_arg_then2 ("ab_in1", [])) (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 ("wedge_in_fan_gt_eq_w_dart_fan", [wedge_in_fan_gt_eq_w_dart_fan])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
   ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fully_surrounded_imp_conforming", [fully_surrounded_imp_conforming])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["confV"])));
   (((fun arg_tac -> (use_arg_then2 ("fan_hypermaps_iso_explicit2", [fan_hypermaps_iso_explicit2])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)) THEN ((fun arg_tac -> arg_tac (Arg_term (`ext_dart _`))) (term_tac (set_tac "h"))));
   (BETA_TAC THEN (move ["h_iso"]));
   ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("Conforming.DARTSET_LEADS_INTO_SUBSET_WDART_FAN", [Conforming.DARTSET_LEADS_INTO_SUBSET_WDART_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("confV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`IMAGE h f`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`h (a,b)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
   (ANTS_TAC);
   ((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("iso_components", [iso_components])) (fun fst_arg -> (use_arg_then2 ("h_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("lemma_in_face_set", [lemma_in_face_set]))(gsym_then (thm_tac (new_rewrite [] []))))));
   ((((fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("h_iso", [])) (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 [] [])))));
   (((((fun arg_tac -> (use_arg_then2 ("iso_components", [iso_components])) (fun fst_arg -> (use_arg_then2 ("h_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] []))))) THEN ((fun arg_tac -> arg_tac (Arg_term (`a,b`))) (term_tac exists_tac)) THEN (done_tac));
   ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("SUBSET_CLOSURE", [SUBSET_CLOSURE])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("IN_TRANS", [IN_TRANS])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
   ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan (vec 0) V E x y`))) (term_tac (set_tac "y'")));
   ((fun arg_tac -> arg_tac (Arg_term (`x,y IN dart_of_fan (V,E)`))) (term_tac (have_gen_tac [](move ["xy_in"]))));
   (((((fun arg_tac -> (use_arg_then2 ("IN_TRANS", [IN_TRANS])) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("FACE_SUBSET_DART_OF_FAN", [FACE_SUBSET_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_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)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_def", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (((use_arg_then2 ("IN_TRANS", [IN_TRANS])) (thm_tac apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`closure (aff_gt {vec 0} {x,y})`))) (term_tac exists_tac)));
   ((((use_arg_then2 ("Planarity.POINT_IN_CLOSURE_AFF_GT_1_2", [Planarity.POINT_IN_CLOSURE_AFF_GT_1_2]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))));
   ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("xy_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["xyV"])));
   ((((use_arg_then2 ("fanV", [])) (disch_tac [])) THEN BETA_TAC) THEN (((((use_arg_then2 ("FAN", [FAN]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fan2", [fan2]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["_"])) THEN (case THEN (move ["_"])) THEN (case THEN (move ["_"])) THEN (case THEN (move ["n0V"])) THEN (move ["_"])));
   ((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ", [PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (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))) (fun fst_arg -> (use_arg_then2 ("y", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac)));
   ((split_tac) THEN (((use_arg_then2 ("n0V", [])) (disch_tac [])) THEN (clear_assumption "n0V") 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));
   ((((use_arg_then2 ("CLOSURE_MINIMAL_EQ", [CLOSURE_MINIMAL_EQ]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("CLOSED_CLOSURE", [CLOSED_CLOSURE]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
   ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Cfyxfty.AFF_GT_SUBSET_CLOSURE_DARTSET_LEADS_INTO_FAN))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`h (x,y)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`IMAGE h f`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
   ((THENL_ROT (-1)) (ANTS_TAC));
   (((((use_arg_then2 ("h_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("ext_dart", [ext_dart]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Fan.pr2", [Fan.pr2]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Fan.pr3", [Fan.pr3]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((((use_arg_then2 ("fully_surrounded_imp_fan80", [fully_surrounded_imp_fan80]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
   ((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("iso_components", [iso_components])) (fun fst_arg -> (use_arg_then2 ("h_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("lemma_in_face_set", [lemma_in_face_set]))(gsym_then (thm_tac (new_rewrite [] []))))));
   (((((fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("h_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))))) THEN (split_tac));
   ((BETA_TAC THEN (move ["z"]) THEN (move ["zV"])) THEN (((use_arg_then2 ("fully_surrounded_card_set_of_edge1", [fully_surrounded_card_set_of_edge1]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
   (((((fun arg_tac -> (use_arg_then2 ("iso_components", [iso_components])) (fun fst_arg -> (use_arg_then2 ("h_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] []))))) THEN ((fun arg_tac -> arg_tac (Arg_term (`x,y`))) (term_tac exists_tac)) THEN (done_tac));
];;

(* Finalization of the section FullySurrounded *)
let fully_surrounded_simple_hypermap = Sections.finalize_theorem fully_surrounded_simple_hypermap;;
let f_surr_localization = Sections.finalize_theorem f_surr_localization;;
let f_surr_localization_convex_local = Sections.finalize_theorem f_surr_localization_convex_local;;
Sections.end_section "FullySurrounded";;
let RNSYJXM = REWRITE_RULE[IMP_IMP] f_surr_localization_convex_local;;

(* Close the module *)
end;;