needs "tame/ssreflect/seq2-compiled.hl";;
needs "hypermap/hypermap.hl";;
needs "fan/HypermapAndFan.hl";;
needs "fan/hypermap_iso-compiled.hl";;

(* Module List_hypermap*)
module List_hypermap = struct

open Ssrbool;;
open Ssrnat;;
open Seq;;
open Seq2;;
open Hypermap;;
open Hypermap_and_fan;;
parse_as_infix ("::", (12, "right"));;
override_interface ("::", `CONS`);;
make_overloadable "++" `:A -> A -> A`;;
overload_interface ("++", `cat`);;
let darts_k = new_definition `darts_k k H = {d:A | d IN dart H /\ CARD (face H d) = k}`;;
let face_set_k = 
	new_definition `face_set_k k (H:(A)hypermap) = {f | f IN face_set H /\ CARD f = k}`;;
let list_pairs = new_definition `list_pairs list = zip list (rot 1 list)`;;
let list_of_darts = new_definition 
	`list_of_darts L = foldr (\list all. (list_pairs list) ++ all) [] L`;;
let darts_of_list = new_definition `darts_of_list L = set_of_list (list_of_darts L)`;;
let list_of_faces = new_definition `list_of_faces L = MAP list_pairs L`;;
let faces_of_list = new_definition `faces_of_list L = MAP set_of_list (list_of_faces L)`;;
let list_of_elements = new_definition `list_of_elements L = undup (flatten L)`;;
let elements_of_list = new_definition `elements_of_list L = set_of_list (list_of_elements L)`;;
let list_of_nodes = new_definition 
  `list_of_nodes L = MAP (\x. filter (\d. FST d = x) (list_of_darts L)) (list_of_elements L)`;;
let nodes_of_list = new_definition `nodes_of_list L = MAP set_of_list (list_of_nodes L)`;;
let list_of_faces3 = new_definition `list_of_faces3 (L:((A)list)list) =
  filter (\f. LENGTH f = 3) (list_of_faces L)`;;
let list_of_faces4 = new_definition `list_of_faces4 (L:((A)list)list) =
  filter (\f. LENGTH f = 4) (list_of_faces L)`;;
let list_of_faces5 = new_definition `list_of_faces5 (L:((A)list)list) =
  filter (\f. LENGTH f = 5) (list_of_faces L)`;;
let list_of_faces6 = new_definition `list_of_faces6 (L:((A)list)list) =
  filter (\f. LENGTH f = 6) (list_of_faces L)`;;
let list_of_darts3 = new_definition `list_of_darts3 (L:((A)list)list) = 
  flatten (list_of_faces3 L)`;;
let list_of_darts4 = new_definition `list_of_darts4 (L:((A)list)list) =
  flatten (list_of_faces4 L)`;;
let list_of_darts5 = new_definition `list_of_darts5 (L:((A)list)list) = 
  flatten (list_of_faces5 L)`;;
let list_of_darts6 = new_definition `list_of_darts6 (L:((A)list)list) =
  flatten (list_of_faces6 L)`;;
let find_list = (GEN_ALL o define) `find_list [] x = []
	/\ find_list (CONS h t) x = if (MEM x h) then h else find_list t x`;;
let find_pair_list = (GEN_ALL o define) `find_pair_list [] d = [] 
   /\ find_pair_list (CONS h t) d = if (MEM d (list_pairs h)) then h else find_pair_list t d`;;
let find_face = new_definition `find_face L d = find_list (list_of_faces L) d`;;
let f_list = new_definition `f_list L d = next_el (find_face L d) d`;;
let e_list = new_definition `e_list d = (SND d, FST d)`;;
let n_list = new_definition `n_list L d = e_list (prev_el (find_face L d) d)`;;
let f_list_ext = new_definition `f_list_ext L = res (f_list L) (darts_of_list L)`;;
let e_list_ext = new_definition `e_list_ext L = res (e_list) (darts_of_list L)`;;
let n_list_ext = new_definition `n_list_ext L = res (n_list L) (darts_of_list L)`;;
let hypermap_of_list = new_definition 
	`hypermap_of_list (L:((A)list)list) = 
		hypermap (darts_of_list L, e_list_ext L, n_list_ext L, f_list_ext L)`;;
let good_list = new_definition `good_list L <=> 
	uniq (list_of_darts L) /\
         all (\l. ~(l = [])) L /\
         (!d. MEM d (list_of_darts L) ==> MEM (SND d, FST d) (list_of_darts L))`;;
let good_list_nodes = new_definition `good_list_nodes L <=> 
	node_set (hypermap_of_list L) = set_of_list (nodes_of_list L)`;;
(* Lemma list_pairs_empty *)
let list_pairs_empty = Sections.section_proof ["s"]
`list_pairs s = [] <=> s = []`
[
   (((((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("size_eq0", [size_eq0]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("size1_zip", [size1_zip]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqnn", [leqnn]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma list_of_darts_alt *)
let list_of_darts_alt = Sections.section_proof ["L"]
`list_of_darts L = flatten (list_of_faces L)`
[
   ((((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("flatten", [flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))));
   (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("MAP", [MAP]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Lemma find_face_alt *)
let find_face_alt = Sections.section_proof ["L";"d"]
`find_face L d = list_pairs (find_pair_list L d)`
[
   ((((use_arg_then2 ("find_face", [find_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))));
   ((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]);
   (((((use_arg_then2 ("MAP", [MAP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_list", [find_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_pair_list", [find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("zip", [zip]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((((use_arg_then2 ("MAP", [MAP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_pair_list", [find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_list", [find_list]))(thm_tac (new_rewrite [] [])))));
   ((((fun arg_tac -> arg_tac (Arg_term (`MEM d _`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma mem_find_list *)
let mem_find_list = Sections.section_proof ["x";"L"]
`MEM x (flatten L) ==> MEM (find_list L x) L`
[
   ((((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["l"])));
   (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("find_list", [find_list]))(thm_tac (new_rewrite [] []))))));
   ((THENL_FIRST) (BETA_TAC THEN (case THEN (((THENL) case [(((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))); (move ["lt"])]) THEN (move ["xl"])))) (((((use_arg_then2 ("xl", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
   ((((fun arg_tac -> arg_tac (Arg_term (`MEM x h`))) (disch_eq_tac "xh" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) THEN ((((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma mem_find_face *)
let mem_find_face = Sections.section_proof ["d";"L"]
`MEM d (list_of_darts L) 
	==> MEM (find_face L d) (list_of_faces L)`
[
   ((((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(thm_tac (new_rewrite [] [])))) THEN (move ["h"]));
   (((((use_arg_then2 ("find_face", [find_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_find_list", [mem_find_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma find_list_empty *)
let find_list_empty = Sections.section_proof ["d";"L"]
`find_list L d = [] <=> ~(MEM d (flatten L))`
[
   ((((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("NOT_EXISTS_THM", [NOT_EXISTS_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negb_and", [negb_and]))(thm_tac (new_rewrite [] [])))));
   (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_list", [find_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))));
   (((fun arg_tac -> arg_tac (Arg_term (`MEM d h`))) (disch_eq_tac "dh" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
   ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`~(h = [])`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac))))) ((((use_arg_then2 ("dh", [])) (disch_tac [])) THEN (clear_assumption "dh") THEN ((use_arg_then2 ("contraL", [contraL])) (disch_tac [])) THEN (clear_assumption "contraL") THEN (DISCH_THEN apply_tac) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
   (((((use_arg_then2 ("NOT_FORALL_THM", [NOT_FORALL_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negb_or", [negb_or]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("negbK", [negbK]))(thm_tac (new_rewrite [] [])))))) THEN ((use_arg_then2 ("h", [])) (term_tac exists_tac)) THEN (done_tac));
   ((((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN ((split_tac) THEN (move ["h1"]) THEN (move ["x"])));
   ((((fun arg_tac -> arg_tac (Arg_term (`x = h`))) (disch_eq_tac "eq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) THEN (((fun arg_tac ->(use_arg_then2 ("eq", []))(fun tmp_arg1 -> (use_arg_then2 ("h1", []))(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));
   ((((fun arg_tac -> (use_arg_then2 ("h1", [])) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case THEN (simp_tac)) THEN ((((use_arg_then2 ("negb_or", [negb_or]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma mem_find_list_nonempty *)
let mem_find_list_nonempty = Sections.section_proof ["x";"L"]
`all (\l. ~(l = [])) L
	==> (MEM x (flatten L) <=> MEM (find_list L x) L)`
[
   (((((use_arg_then2 ("allP", [allP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["h1"]));
   ((THENL_FIRST) ((THENL) (split_tac) [ALL_TAC; (move ["h2"])]) (((use_arg_then2 ("mem_find_list", [mem_find_list])) (thm_tac apply_tac)) THEN (done_tac)));
   ((((fun arg_tac -> (use_arg_then2 ("h1", [])) (fun fst_arg -> (use_arg_then2 ("h2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("find_list_empty", [find_list_empty]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negbK", [negbK]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma mem_find_face_nonempty *)
let mem_find_face_nonempty = Sections.section_proof ["d";"L"]
`all (\l. ~(l = [])) L
	==> (MEM d (list_of_darts L) <=> MEM (find_face L d) (list_of_faces L))`
[
   (BETA_TAC THEN (move ["h1"]));
   ((((use_arg_then2 ("find_face", [find_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_find_list_nonempty", [mem_find_list_nonempty]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
   ((in_tac ["h1"] true ((repeat_tactic 1 9 (((use_arg_then2 ("allP", [allP]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (simp_tac))) THEN ((((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))) THEN (move ["s"])));
   ((((use_arg_then2 ("MEM_MAP", [MEM_MAP]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["l"])) THEN (case THEN (move ["l_L"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
   (((((use_arg_then2 ("EQ_SYM_EQ", [EQ_SYM_EQ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_pairs_empty", [list_pairs_empty]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("h1", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma e_list_ext_involution *)
let e_list_ext_involution = Sections.section_proof ["L"]
`good_list L ==> e_list_ext L o e_list_ext L = I`
[
   (((((use_arg_then2 ("FUN_EQ_THM", [FUN_EQ_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("I_THM", [I_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_list_ext", [e_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["h_uniq"])) THEN (case THEN (move ["all_n"])) THEN (move ["mem_snd"]) THEN (case THEN ((move ["x"]) THEN (move ["y"]))));
   ((repeat_tactic 1 9 (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FST", [FST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SND", [SND]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))));
   (((fun arg_tac -> arg_tac (Arg_term (`MEM (x,y) _`))) (disch_eq_tac "xy_in" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
   ((((fun arg_tac -> (use_arg_then2 ("mem_snd", [])) (fun fst_arg -> (use_arg_then2 ("xy_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (simp_tac)) THEN (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
   ((((use_arg_then2 ("xy_in", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;
let INVERSE_EXISTS_IMP_BIJECTIVE = 
prove(`!(f:A->B) g. f o g = I /\ g o f = I ==> (!y. ?!x. f x = y)`,

   REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM] THEN			
     REPEAT STRIP_TAC THEN REWRITE_TAC[EXISTS_UNIQUE] THEN
     EXISTS_TAC `(g:B->A) y` THEN
     ASM_REWRITE_TAC[] THEN
     REPEAT STRIP_TAC THEN
     POP_ASSUM (MP_TAC o AP_TERM `g:B->A`) THEN
     ASM_REWRITE_TAC[]);;
(* Lemma e_list_ext_permutes_darts *)
let e_list_ext_permutes_darts = Sections.section_proof ["L"]
`good_list L 
	==> (e_list_ext L) permutes (darts_of_list L)`
[
   (((((use_arg_then2 ("permutes", [permutes]))(thm_tac (new_rewrite [] [])))) THEN (move ["good_l"])) THEN (split_tac));
   ((BETA_TAC THEN (move ["x"]) THEN (move ["x_n"])) THEN ((((use_arg_then2 ("e_list_ext", [e_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("x_n", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((use_arg_then2 ("INVERSE_EXISTS_IMP_BIJECTIVE", [INVERSE_EXISTS_IMP_BIJECTIVE])) (thm_tac apply_tac));
   (((fun arg_tac -> arg_tac (Arg_term (`e_list_ext L`))) (term_tac exists_tac)) THEN (((use_arg_then2 ("ETA_AX", [ETA_AX]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then2 ("e_list_ext_involution", [e_list_ext_involution]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma dart_in_darts *)
let dart_in_darts = Sections.section_proof ["d";"l";"L"]
`MEM d (list_pairs l) /\ MEM l L
	==> MEM d (list_of_darts L)`
[
   (((((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM_MAP", [MEM_MAP]))(thm_tac (new_rewrite [] []))))) THEN (move ["h"]));
   (((fun arg_tac -> arg_tac (Arg_term (`list_pairs l`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("l", [])) (term_tac exists_tac)) THEN (done_tac));
];;

(* Lemma mem_find_pair_list *)
let mem_find_pair_list = Sections.section_proof ["d";"L"]
`MEM d (list_of_darts L) ==> MEM (find_pair_list L d) L`
[
   (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("find_pair_list", [find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)));
   (((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_pairs h)`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
   ((((((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("orFb", [orFb]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_darts", [list_of_darts]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("Ih", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma dart_in_find_pair_list *)
let dart_in_find_pair_list = Sections.section_proof ["d";"L"]
`MEM d (list_of_darts L) <=> MEM d (list_pairs (find_pair_list L d))`
[
   (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_pair_list", [find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] []))))));
   (((((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("zip", [zip]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_pairs h)`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) THEN ((((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("orFb", [orFb]))(thm_tac (new_rewrite [] []))))));
   (((((use_arg_then2 ("list_of_darts", [list_of_darts]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma dart_in_face *)
let dart_in_face = Sections.section_proof ["d";"L"]
`MEM d (list_of_darts L) <=> MEM d (find_face L d)`
[
   (((((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart_in_find_pair_list", [dart_in_find_pair_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma uniq_imp_unique_list *)
let uniq_imp_unique_list = Sections.section_proof ["l1";"l2";"d";"L"]
`uniq (list_of_darts L) /\ MEM l1 L /\ MEM l2 L
	/\ MEM d (list_pairs l1) /\ MEM d (list_pairs l2)
	==> l1 = l2`
[
   (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))));
   ((((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("list_of_darts", [list_of_darts]))(gsym_then (thm_tac (new_rewrite [] []))))));
   ((((use_arg_then2 ("cat_uniq", [cat_uniq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hasP", [hasP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("NOT_EXISTS_THM", [NOT_EXISTS_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negb_and", [negb_and]))(thm_tac (new_rewrite [] [])))));
   (BETA_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["uniq_h"])) THEN (case THEN (move ["not_mem"])) THEN (move ["uniq_t"]) THEN (case THEN (move ["h1"])) THEN (case THEN (move ["h2"])) THEN (case THEN (move ["d_l1"])) THEN (move ["d_l2"]));
   ((THENL_LAST) (((use_arg_then2 ("h2", [])) (disch_tac [])) THEN (clear_assumption "h2") THEN ((use_arg_then2 ("h1", [])) (disch_tac [])) THEN (clear_assumption "h1") THEN case THEN (move ["h1"]) THEN (case THEN ALL_TAC) THEN (move ["h2"]) THEN ((TRY done_tac))) (((use_arg_then2 ("Ih", [])) (disch_tac [])) THEN (clear_assumption "Ih") THEN (exact_tac)));
   ((((fun arg_tac -> (use_arg_then2 ("not_mem", [])) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("h1", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("d_l1", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)));
   ((((fun arg_tac -> (use_arg_then2 ("dart_in_darts", [dart_in_darts])) (fun fst_arg -> (use_arg_then2 ("d_l2", [])) (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 ("not_mem", [])) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("h2", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("d_l2", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)));
   ((((fun arg_tac -> (use_arg_then2 ("dart_in_darts", [dart_in_darts])) (fun fst_arg -> (use_arg_then2 ("d_l1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma find_pair_list_unique *)
let find_pair_list_unique = Sections.section_proof ["l";"d";"L"]
`uniq (list_of_darts L) /\ MEM l L /\ MEM d (list_pairs l) 
	==> l = find_pair_list L d`
[
   (BETA_TAC THEN (case THEN (move ["uniq_darts"])) THEN (case THEN (move ["l_L"])) THEN (move ["mem_d"]));
   (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("uniq_imp_unique_list", [uniq_imp_unique_list])) (fun fst_arg -> (use_arg_then2 ("uniq_darts", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem_d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
   (((((use_arg_then2 ("l_L", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_face_alt", [find_face_alt]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_find_pair_list", [mem_find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("dart_in_darts", [dart_in_darts])) (fun fst_arg -> (use_arg_then2 ("mem_d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma uniq_find_face *)
let uniq_find_face = Sections.section_proof ["d";"L"]
`uniq (list_of_darts L) ==> uniq (find_face L d)`
[
   (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_face", [find_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MAP", [MAP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_list", [find_list]))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac))));
   (((((use_arg_then2 ("list_of_darts", [list_of_darts]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("list_of_faces", [list_of_faces]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("find_face", [find_face]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("cat_uniq", [cat_uniq]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["uniq_h"])) THEN (case THEN (move ["_"])) THEN (move ["uniq_t"]));
   ((((fun arg_tac -> arg_tac (Arg_term (`MEM d _`))) (disch_tac [])) THEN case THEN ((simp_tac THEN TRY done_tac))) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma size_list_pairs *)
let size_list_pairs = Sections.section_proof ["l"]
`sizel (list_pairs l) = sizel l`
[
   (((((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size1_zip", [size1_zip]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqnn", [leqnn]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma mem_list_pairs *)
let mem_list_pairs = Sections.section_proof ["x";"y";"l"]
`MEM (x,y) (list_pairs l) ==> MEM x l /\ MEM y l`
[
   (((((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("mem_zip", [mem_zip])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (((use_arg_then2 ("mem_rot", [mem_rot]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma mem_f_list *)
let mem_f_list = Sections.section_proof ["d";"L"]
`MEM d (list_of_darts L) ==> MEM (f_list L d) (find_face L d)`
[
   ((BETA_TAC THEN (move ["mem_d"])) THEN ((((use_arg_then2 ("f_list", [f_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_next_el", [mem_next_el]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Lemma nth_list_pairs *)
let nth_list_pairs = Sections.section_proof ["x0";"i";"s"]
`i < sizel s
	==> nth (x0, x0) (list_pairs s) i
		= (nth x0 s i, nth x0 s (if i = sizel s - 1 then 0 else i + 1))`
[
   ((BETA_TAC THEN (move ["i_lt"])) THEN ((((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth_zip", [nth_zip]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))));
   (((((use_arg_then2 ("nth_shift_left", [nth_shift_left]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("fun_if", [fun_if]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Lemma uniq_list_pairs *)
let uniq_list_pairs = Sections.section_proof ["s"]
`uniq s ==> uniq (list_pairs s)`
[
   ((fun arg_tac -> arg_tac (Arg_term (`HD s`))) (term_tac (set_tac "x0")));
   (((((fun arg_tac -> (use_arg_then2 ("uniq_nthP", [uniq_nthP])) (fun fst_arg -> (use_arg_then2 ("x0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("uniq_nthP", [uniq_nthP])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x0, x0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] []))))) THEN (move ["h"]) THEN (move ["i"]) THEN (move ["j"]) THEN (case THEN (move ["i_lt_j"])) THEN (move ["j_lt"]));
   (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("h", [])) (fun fst_arg -> (use_arg_then2 ("i_lt_j", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("j_lt", [])) (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));
   ((repeat_tactic 1 9 (((use_arg_then2 ("nth_list_pairs", [nth_list_pairs]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 0 10 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac));
   ((((use_arg_then2 ("j_lt", [])) (disch_tac [])) THEN (clear_assumption "j_lt") THEN ((use_arg_then2 ("i_lt_j", [])) (disch_tac [])) THEN (clear_assumption "i_lt_j") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
];;

(* Lemma mem_list_pairs_explicit *)
let mem_list_pairs_explicit = Sections.section_proof ["x";"y";"s"]
`uniq s /\ MEM (x,y) (list_pairs s)
	==> y = next_el s x`
[
   (((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nthP", [nthP])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x,y`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x,x`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["uniq_s"])) THEN (case THEN (move ["i"])));
   (((((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth_zip", [nth_zip]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))))) THEN ALL_TAC THEN (case THEN (move ["i_lt"])) THEN (case THEN (move ["x_eq"])) THEN (move ["y_eq"]));
   ((THENL_FIRST) (((fun arg_tac -> (use_arg_then2 ("next_el_alt", [next_el_alt])) (fun fst_arg -> (use_arg_then2 ("x", [])) (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 ("nthP", [nthP])) (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 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("i", [])) (term_tac exists_tac)) THEN (done_tac)));
   (((((use_arg_then2 ("y_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("x_eq", []))(gsym_then (thm_tac (new_rewrite [3] []))))) THEN (((use_arg_then2 ("index_uniq", [index_uniq]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma index_fst_snd *)
let index_fst_snd = Sections.section_proof ["x0";"i";"x";"y";"s"]
`uniq s /\ i < sizel s /\ nth (x0,x0) (list_pairs s) i = (x,y)
	==> indexl x s = i /\ indexl y s = if (i = sizel s - 1) then 0 else i + 1`
[
   (BETA_TAC THEN (case THEN (move ["uniq_s"])) THEN (case THEN (move ["i_lt"])) THEN (simp_tac));
   (((((use_arg_then2 ("nth_list_pairs", [nth_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))))));
   (((repeat_tactic 1 9 (((use_arg_then2 ("index_uniq", [index_uniq]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("uniq_s", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("i_lt", [])) (disch_tac [])) THEN (clear_assumption "i_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
];;

(* Lemma next_el_list_pairs *)
let next_el_list_pairs = Sections.section_proof ["x";"y";"s"]
`uniq s /\ MEM (x,y) (list_pairs s)
	==> next_el (list_pairs s) (x,y) = (y, next_el s y)`
[
   (BETA_TAC THEN (case THEN ((move ["uniq_s"]) THEN (move ["mem_d"]))));
   ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`MEM y s`))) (term_tac (have_gen_tac [](move ["ys"])))) ((((fun arg_tac -> (use_arg_then2 ("mem_list_pairs", [mem_list_pairs])) (fun fst_arg -> (use_arg_then2 ("mem_d", [])) (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 ("next_el_alt", [next_el_alt])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x,x`))) (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 ("next_el_alt", [next_el_alt])) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
   ((fun arg_tac -> arg_tac (Arg_term (`indexl _1 _2`))) (term_tac (set_tac "i")));
   ((fun arg_tac -> arg_tac (Arg_term (`nth (x,x) (list_pairs s) i = x,y`))) (term_tac (have_gen_tac [](move ["nth_i"]))));
   (((((use_arg_then2 ("i_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("nth_index", [nth_index]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((fun arg_tac -> arg_tac (Arg_term (`i < sizel s`))) (term_tac (have_gen_tac [](move ["i_lt"]))));
   (((((use_arg_then2 ("i_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((repeat_tactic 1 9 (((use_arg_then2 ("nth_shift_left", [nth_shift_left]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 0 10 (((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
   ((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("index_fst_snd", [index_fst_snd])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("i_lt", [])) (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 ("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 ((TRY done_tac)));
   (((fun arg_tac -> arg_tac (Arg_term (`i = sizel s - 1`))) (disch_eq_tac "eq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
   ((THENL_FIRST) (((use_arg_then2 ("nth_list_pairs", [nth_list_pairs]))(thm_tac (new_rewrite [] [])))) ((((use_arg_then2 ("i_lt", [])) (disch_tac [])) THEN (clear_assumption "i_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
   ((((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN (split_tac));
   (((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nth_index", [nth_index])) (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))) (fun fst_arg -> (use_arg_then2 ("s", [])) (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 -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("index_fst_snd", [index_fst_snd])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("i_lt", [])) (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 ("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 (done_tac));
   ((((fun arg_tac -> arg_tac (Arg_term (`0 = sizel s - 1`))) (disch_eq_tac "eq2" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) THEN (((use_arg_then2 ("eq2", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((THENL_FIRST) (((use_arg_then2 ("nth_list_pairs", [nth_list_pairs]))(thm_tac (new_rewrite [] [])))) ((((use_arg_then2 ("eq", [])) (disch_tac [])) THEN (clear_assumption "eq") THEN ((use_arg_then2 ("i_lt", [])) (disch_tac [])) THEN (clear_assumption "i_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
   ((((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN (split_tac));
   (((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nth_index", [nth_index])) (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))) (fun fst_arg -> (use_arg_then2 ("s", [])) (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 -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("index_fst_snd", [index_fst_snd])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("i_lt", [])) (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 ("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 (done_tac));
   ((((fun arg_tac -> arg_tac (Arg_term (`i + 1 = _`))) (disch_eq_tac "eq2" [])) THEN case THEN (process_fst_eq_tac)) THEN (done_tac));
];;

(* Lemma prev_el_list_pairs *)
let prev_el_list_pairs = Sections.section_proof ["x";"y";"s"]
`uniq s /\ MEM (x,y) (list_pairs s)
	==> prev_el (list_pairs s) (x,y) = (prev_el s x, x)`
[
   (BETA_TAC THEN (case THEN ((move ["uniq_s"]) THEN (move ["mem_d"]))));
   ((fun arg_tac -> arg_tac (Arg_term (`prev_el _1 _2`))) (term_tac (set_tac "t")));
   ((fun arg_tac -> arg_tac (Arg_term (`MEM t (list_pairs s)`))) (term_tac (have_gen_tac [](move ["mem_t"]))));
   (((((use_arg_then2 ("t_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (((use_arg_then2 ("t_def", [])) (disch_tac [])) THEN (clear_assumption "t_def") THEN ((use_arg_then2 ("mem_t", [])) (disch_tac [])) THEN (clear_assumption "mem_t") THEN ((use_arg_then2 ("t", [])) (disch_tac [])) THEN (clear_assumption "t") THEN case THEN (move ["a"]) THEN (move ["b"]) THEN (move ["mem_t"]) THEN (move ["t_def"]));
   ((fun arg_tac -> arg_tac (Arg_term (`b = next_el s a`))) (term_tac (have_gen_tac []ALL_TAC)));
   ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("mem_list_pairs_explicit", [mem_list_pairs_explicit])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem_t", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
   ((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("congr1", [congr1])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`prev_el s`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC);
   (((((use_arg_then2 ("prev_next_id", [prev_next_id]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("mem_list_pairs", [mem_list_pairs])) (fun fst_arg -> (use_arg_then2 ("mem_t", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))));
   (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`b = x`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)))))));
   (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("congr1", [congr1])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`next_el (list_pairs s)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("t_def", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC);
   ((((((use_arg_then2 ("next_prev_id", [next_prev_id]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uniq_list_pairs", [uniq_list_pairs]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("next_el_list_pairs", [next_el_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma f_list_inverse *)
let f_list_inverse = Sections.section_proof ["d";"L"]
`uniq (list_of_darts L) /\ MEM d (list_of_darts L)
	==> f_list L (prev_el (find_face L d) d) = d 
	/\ prev_el (find_face L (f_list L d)) (f_list L d) = d`
[
   ((BETA_TAC THEN (case THEN ((move ["uniq_s"]) THEN (move ["mem_d"])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("f_list", [f_list]))(thm_tac (new_rewrite [] []))))) THEN (split_tac));
   ((fun arg_tac -> arg_tac (Arg_term (`find_face L d`))) (term_tac (set_tac "f")));
   (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`find_face L (prev_el f d) = f`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))));
   (((((use_arg_then2 ("next_prev_id", [next_prev_id]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("uniq_find_face", [uniq_find_face]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
   (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] []))))) THEN ((congr_tac (`_1 _2`)) THEN ((TRY done_tac))));
   (((fun arg_tac -> (use_arg_then2 ("find_pair_list_unique", [find_pair_list_unique])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
   ((((use_arg_then2 ("mem_find_pair_list", [mem_find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("find_face_alt", [find_face_alt]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
   (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
   ((fun arg_tac -> arg_tac (Arg_term (`find_face L d`))) (term_tac (set_tac "f")));
   (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`find_face L (next_el f d) = f`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))));
   (((((use_arg_then2 ("prev_next_id", [prev_next_id]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("uniq_find_face", [uniq_find_face]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
   (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] []))))) THEN ((congr_tac (`_1 _2`)) THEN ((TRY done_tac))));
   (((fun arg_tac -> (use_arg_then2 ("find_pair_list_unique", [find_pair_list_unique])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
   ((((use_arg_then2 ("mem_find_pair_list", [mem_find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("find_face_alt", [find_face_alt]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_next_el", [mem_next_el]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
   (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Lemma find_face_f_list *)
let find_face_f_list = Sections.section_proof ["d";"L"]
`uniq (list_of_darts L) /\ MEM d (list_of_darts L)
	==> find_face L (f_list L d) = find_face L d`
[
   (BETA_TAC THEN (case THEN ((move ["uniq_s"]) THEN (move ["mem_d"]))));
   (((repeat_tactic 1 9 (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] []))))) THEN ((congr_tac (`_1 _2`)) THEN ((TRY done_tac))));
   (((fun arg_tac -> (use_arg_then2 ("find_pair_list_unique", [find_pair_list_unique])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
   (((((use_arg_then2 ("mem_find_pair_list", [mem_find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("find_face_alt", [find_face_alt]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_f_list", [mem_f_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma f_list_ext_permutes_darts *)
let f_list_ext_permutes_darts = Sections.section_proof ["L"]
`uniq (list_of_darts L)
	==> (f_list_ext L) permutes (darts_of_list L)`
[
   (BETA_TAC THEN (move ["uniq_s"]));
   ((((use_arg_then2 ("f_list_ext", [f_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Hypermap_and_fan.RES_PERMUTES", [Hypermap_and_fan.RES_PERMUTES]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))));
   ((THENL) (split_tac) [((move ["d"]) THEN (move ["mem_d"])); ALL_TAC]);
   (((((use_arg_then2 ("dart_in_face", [dart_in_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_face_f_list", [find_face_f_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("mem_f_list", [mem_f_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((THENL_ROT (-1)) ((THENL) (split_tac) [((move ["d"]) THEN (move ["mem_d"])); ((move ["d1"]) THEN (move ["d2"]) THEN (case THEN (move ["mem_d1"])) THEN (case THEN (move ["mem_d2"])) THEN (move ["eq"]))]));
   ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("f_list_inverse", [f_list_inverse])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem_d1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["_"]) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))))));
   (((((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("f_list_inverse", [f_list_inverse])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem_d2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((fun arg_tac -> arg_tac (Arg_term (`prev_el (find_face L d) d`))) (term_tac exists_tac));
   ((((use_arg_then2 ("f_list_inverse", [f_list_inverse]))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac)) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(thm_tac (new_rewrite [] [])))));
   ((fun arg_tac -> arg_tac (Arg_term (`find_face L d`))) (term_tac (set_tac "f")));
   (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`find_face L (prev_el f d) = f`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))));
   (((((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
   (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] []))))) THEN ((congr_tac (`_1 _2`)) THEN ((TRY done_tac))));
   (((fun arg_tac -> (use_arg_then2 ("find_pair_list_unique", [find_pair_list_unique])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
   ((((use_arg_then2 ("mem_find_pair_list", [mem_find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("find_face_alt", [find_face_alt]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
   (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Lemma find_face_empty *)
let find_face_empty = Sections.section_proof ["d";"L"]
`find_face L d = [] <=> ~MEM d (list_of_darts L)`
[
   (((((use_arg_then2 ("find_face", [find_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_list_empty", [find_list_empty]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma mem_find_face_imp_faces_eq *)
let mem_find_face_imp_faces_eq = Sections.section_proof ["d1";"d2";"L"]
`uniq (list_of_darts L) /\ MEM d1 (find_face L d2)
	==> find_face L d1 = find_face L d2`
[
   (BETA_TAC THEN (case THEN ((move ["uniq_s"]) THEN (move ["mem_d1"]))));
   (((repeat_tactic 1 9 (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] []))))) THEN ((congr_tac (`_1 _2`)) THEN ((TRY done_tac))));
   (((fun arg_tac -> (use_arg_then2 ("find_pair_list_unique", [find_pair_list_unique])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
   ((((use_arg_then2 ("find_face_alt", [find_face_alt]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_d1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_find_pair_list", [mem_find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
   (((use_arg_then2 ("mem_d1", [])) (disch_tac [])) THEN (clear_assumption "mem_d1") THEN ((use_arg_then2 ("contraLR", [contraLR])) (disch_tac [])) THEN (clear_assumption "contraLR") THEN (DISCH_THEN apply_tac));
   (((((use_arg_then2 ("find_face_empty", [find_face_empty]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma mem_find_face_imp_mem_darts *)
let mem_find_face_imp_mem_darts = Sections.section_proof ["d";"y";"L"]
`MEM d (find_face L y) ==> MEM d (list_of_darts L)`
[
   (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("find_face", [find_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MAP", [MAP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_list", [find_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))));
   ((((use_arg_then2 ("list_of_darts", [list_of_darts]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] [])))));
   (((fun arg_tac -> arg_tac (Arg_term (`MEM y _`))) (disch_eq_tac "mem_y" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
   ((((((use_arg_then2 ("list_of_faces", [list_of_faces]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("find_face", [find_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("Ih", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma f_list_ext_inverse *)
let f_list_ext_inverse = Sections.section_proof ["L"]
`uniq (list_of_darts L)
	==> inverse (f_list_ext L) = res (\d. prev_el (find_face L d) d) (darts_of_list L)`
[
   ((((use_arg_then2 ("FUN_EQ_THM", [FUN_EQ_THM]))(thm_tac (new_rewrite [] [])))) THEN (move ["uniq_s"]) THEN (move ["d"]));
   (((fun arg_tac -> (use_arg_then2 ("PERMUTES_INVERSE_EQ", [PERMUTES_INVERSE_EQ])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("f_list_ext_permutes_darts", [f_list_ext_permutes_darts])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (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 [] []))));
   ((((use_arg_then2 ("f_list_ext", [f_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))));
   ((THENL_LAST) (((fun arg_tac -> arg_tac (Arg_term (`MEM d _`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) ((((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
   ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`MEM _1 _2`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac)))))) ((((use_arg_then2 ("f_list_inverse", [f_list_inverse]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
   (((use_arg_then2 ("mem_find_face_imp_mem_darts", [mem_find_face_imp_mem_darts])) (thm_tac apply_tac)) THEN ((use_arg_then2 ("d", [])) (term_tac exists_tac)));
   (((((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Lemma f_list_ext_inverse_works *)
let f_list_ext_inverse_works = Sections.section_proof ["L"]
`uniq (list_of_darts L)
	==> f_list_ext L o inverse (f_list_ext L) = I
	/\ inverse (f_list_ext L) o f_list_ext L = I`
[
   (BETA_TAC THEN (move ["uniq_s"]));
   (((fun arg_tac -> (use_arg_then2 ("PERMUTES_INVERSES_o", [PERMUTES_INVERSES_o])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("f_list_ext_permutes_darts", [f_list_ext_permutes_darts])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (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 (exact_tac));
];;

(* Lemma n_eq_e_fi *)
let n_eq_e_fi = Sections.section_proof ["L"]
`uniq (list_of_darts L)
	==> n_list_ext L = e_list_ext L o inverse (f_list_ext L)`
[
   (BETA_TAC THEN (move ["uniq_s"]));
   (((((use_arg_then2 ("f_list_ext_inverse", [f_list_ext_inverse]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("eq_ext", [eq_ext]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_list_ext", [n_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_list_ext", [e_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["d"]));
   ((((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))));
   ((THENL_LAST) (((fun arg_tac -> arg_tac (Arg_term (`MEM d _`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) ((((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
   ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`MEM _1 _2`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac)))))) ((((use_arg_then2 ("n_list", [n_list]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
   (((use_arg_then2 ("mem_find_face_imp_mem_darts", [mem_find_face_imp_mem_darts])) (thm_tac apply_tac)) THEN ((use_arg_then2 ("d", [])) (term_tac exists_tac)));
   (((((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Lemma n_list_ext_permutes_darts *)
let n_list_ext_permutes_darts = Sections.section_proof ["L"]
`good_list L
	==> (n_list_ext L) permutes (darts_of_list L)`
[
   ((BETA_TAC THEN (move ["good_s"])) THEN (((use_arg_then2 ("good_s", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniq_s"])) THEN (move ["_"])));
   ((((use_arg_then2 ("n_eq_e_fi", [n_eq_e_fi]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("PERMUTES_COMPOSE", [PERMUTES_COMPOSE]))(thm_tac (new_rewrite [] [])))));
   ((((use_arg_then2 ("e_list_ext_permutes_darts", [e_list_ext_permutes_darts]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("PERMUTES_INVERSE", [PERMUTES_INVERSE]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
   (((fun arg_tac -> (use_arg_then2 ("f_list_ext_permutes_darts", [f_list_ext_permutes_darts])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (exact_tac));
];;

(* Lemma e_n_f_id *)
let e_n_f_id = Sections.section_proof ["L"]
`good_list L
	==> e_list_ext L o n_list_ext L o f_list_ext L = I`
[
   ((BETA_TAC THEN (move ["good_s"])) THEN (((use_arg_then2 ("good_s", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniq_s"])) THEN (move ["_"])));
   (((((use_arg_then2 ("n_eq_e_fi", [n_eq_e_fi]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("o_ASSOC", [o_ASSOC]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("e_list_ext_involution", [e_list_ext_involution]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("I_O_ID", [I_O_ID]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_list_ext_inverse_works", [f_list_ext_inverse_works]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma tuple_hypermap_of_list *)
let tuple_hypermap_of_list = Sections.section_proof ["L"]
`good_list L
	==> tuple_hypermap (hypermap_of_list L) =
	darts_of_list L, e_list_ext L, n_list_ext L, f_list_ext L`
[
   ((BETA_TAC THEN (move ["good_s"])) THEN (((use_arg_then2 ("good_s", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniq_s"])) THEN (move ["_"])));
   ((((use_arg_then2 ("hypermap_of_list", [hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (CONJUNCT2 hypermap_tybij)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac));
   ((((use_arg_then2 ("e_list_ext_permutes_darts", [e_list_ext_permutes_darts]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("n_list_ext_permutes_darts", [n_list_ext_permutes_darts]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_list_ext_permutes_darts", [f_list_ext_permutes_darts]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
   (((((use_arg_then2 ("e_n_f_id", [e_n_f_id]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FINITE_SET_OF_LIST", [FINITE_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma f_list_ext_orbit *)
let f_list_ext_orbit = Sections.section_proof ["L";"x"]
`MEM x (list_of_darts L) /\ uniq (list_of_darts L)
	==> orbit_map (f_list_ext L) x = set_of_list (find_face L x)`
[
   (BETA_TAC THEN (case THEN ((move ["mem_x"]) THEN (move ["uniq_l"]))));
   ((((use_arg_then2 ("f_list_ext", [f_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ORBIT_MAP_RES", [ORBIT_MAP_RES]))(thm_tac (new_rewrite [] [])))));
   (((((use_arg_then2 ("f_list_ext", [f_list_ext]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_list_ext_permutes_darts", [f_list_ext_permutes_darts]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`MEM x (find_face L x)`))) (term_tac (have_gen_tac [](move ["x_in_face"])))) ((((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac)));
   (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`orbit_map (f_list L) x = orbit_map (next_el (find_face L x)) x`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))));
   (((((use_arg_then2 ("next_el_orbit", [next_el_orbit]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("uniq_find_face", [uniq_find_face]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`(f_list L POWER n) x = (next_el (find_face L x) POWER n) x`))) (term_tac (have_gen_tac ["n"](move ["eq"])))));
   (((repeat_tactic 1 9 (((use_arg_then2 ("orbit_map", [orbit_map]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((THENL_FIRST) ((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 (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 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_list", [f_list]))(thm_tac (new_rewrite [] [])))));
   ((congr_tac (`next_el _1 _2`)) THEN ((TRY done_tac)));
   (((fun arg_tac -> (use_arg_then2 ("mem_find_face_imp_faces_eq", [mem_find_face_imp_faces_eq])) (fun fst_arg -> (use_arg_then2 ("uniq_l", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
   ((((fun arg_tac -> (use_arg_then2 ("next_el_power", [next_el_power])) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uniq_find_face", [uniq_find_face]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
   ((((use_arg_then2 ("mem_nth", [mem_nth]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DIVISION", [DIVISION]))(gsym_then (thm_tac (new_rewrite [] []))))));
   ((((use_arg_then2 ("x_in_face", [])) (disch_tac [])) THEN (clear_assumption "x_in_face") THEN BETA_TAC) THEN (((use_arg_then2 ("index_mem", [index_mem]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
];;

(* Lemma uniq_flatten *)
let uniq_flatten = Sections.section_proof ["L"]
`uniq (flatten L) /\ all (\l. ~(l = [])) L ==> uniq L`
[
   (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("uniq", [uniq]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("flatten", [flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("all", [all]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat_uniq", [cat_uniq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("flatten", [flatten]))(gsym_then (thm_tac (new_rewrite [] [])))))));
   (BETA_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["uniq_h"])) THEN (case THEN (move ["not_has"])) THEN (move ["uniq_t"]) THEN (case THEN (move ["h_n0"])) THEN (move ["all_t"]));
   ((((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))));
   ((((use_arg_then2 ("not_has", [])) (disch_tac [])) THEN (clear_assumption "not_has") THEN ((use_arg_then2 ("contra", [contra])) (disch_tac [])) THEN (clear_assumption "contra") THEN (DISCH_THEN apply_tac)) THEN (((((use_arg_then2 ("hasP", [hasP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["ht"])));
   ((((use_arg_then2 ("h_n0", [])) (disch_tac [])) THEN (clear_assumption "h_n0") THEN BETA_TAC) THEN (((((use_arg_then2 ("size_eq0", [size_eq0]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("lt0n", [lt0n]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("has_predT", [has_predT]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hasP", [hasP]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ALL_TAC THEN (case THEN (move ["x"])) THEN (case THEN (move ["xh"])) THEN (move ["_"])));
   (((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("xh", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))));
   ((((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] [])))) THEN ((use_arg_then2 ("h", [])) (term_tac exists_tac)) THEN (done_tac));
];;

(* Lemma flatten_filter_empty *)
let flatten_filter_empty = Sections.section_proof ["L"]
`flatten (filter (\l. ~(l = [])) L) = flatten L`
[
   (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("flatten", [flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("filter", [filter]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("flatten", [flatten]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)));
   (((fun arg_tac -> arg_tac (Arg_term (`h = []`))) (disch_eq_tac "eq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
   (((((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (((((use_arg_then2 ("flatten", [flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("flatten", [flatten]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma uniq_sublist_unique *)
let uniq_sublist_unique = Sections.section_proof ["l1";"l2";"L";"x"]
`uniq (flatten L) /\ MEM l1 L /\ MEM l2 L
	/\ MEM x l1 /\ MEM x l2
	==> l1 = l2`
[
   (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("flatten_cons", [flatten_cons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat_uniq", [cat_uniq]))(thm_tac (new_rewrite [] []))))));
   (BETA_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["uniq_h"])) THEN (case THEN (move ["not_has"])) THEN (move ["uniq_t"]) THEN (case THEN (move ["c1"])) THEN (case THEN (move ["c2"])) THEN (case THEN (move ["x_l1"])) THEN (move ["x_l2"]));
   ((THENL_LAST) (((THENL) (((use_arg_then2 ("c2", [])) (disch_tac [])) THEN (clear_assumption "c2") THEN ((use_arg_then2 ("c1", [])) (disch_tac [])) THEN (clear_assumption "c1") THEN case) [(move ["eq1"]); (move ["l1t"])]) THEN ((THENL) case [(move ["eq2"]); (move ["l2t"])]) THEN ((TRY done_tac))) ((((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
   ((((use_arg_then2 ("not_has", [])) (disch_tac [])) THEN (clear_assumption "not_has") THEN ((use_arg_then2 ("contraR", [contraR])) (disch_tac [])) THEN (clear_assumption "contraR") THEN (DISCH_THEN apply_tac) THEN (move ["_"])) THEN ((((use_arg_then2 ("hasP", [hasP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)));
   (((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq1", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("x_l1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("l2", [])) (term_tac exists_tac)) THEN (done_tac));
   ((((use_arg_then2 ("not_has", [])) (disch_tac [])) THEN (clear_assumption "not_has") THEN ((use_arg_then2 ("contraR", [contraR])) (disch_tac [])) THEN (clear_assumption "contraR") THEN (DISCH_THEN apply_tac) THEN (move ["_"])) THEN ((((use_arg_then2 ("hasP", [hasP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)));
   (((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq2", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("x_l2", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("l1", [])) (term_tac exists_tac)) THEN (done_tac));
];;

(* Lemma uniq_face_unique *)
let uniq_face_unique = Sections.section_proof ["f1";"f2";"d";"L"]
`uniq (list_of_darts L)
	/\ MEM f1 (list_of_faces L) /\ MEM f2 (list_of_faces L) /\ MEM d f1 /\ MEM d f2
	==> f1 = f2`
[
   (BETA_TAC THEN (case THEN (move ["uniq_l"])) THEN (case THEN (move ["mem_f1"])) THEN (case THEN (move ["mem_f2"])) THEN (case THEN (move ["mem_d1"])) THEN (move ["mem_d2"]));
   ((use_arg_then2 ("uniq_sublist_unique", [uniq_sublist_unique])) (thm_tac apply_tac));
   (((fun arg_tac -> arg_tac (Arg_term (`list_of_faces L`))) (term_tac exists_tac)) THEN ((use_arg_then2 ("d", [])) (term_tac exists_tac)));
   ((((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma mem_face_lemma *)
let mem_face_lemma = Sections.section_proof ["f";"L"]
`good_list L /\ MEM f (list_of_faces L)
	==> ?d. MEM d (list_of_darts L) /\ f = find_face L d`
[
   ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["uniq_s"])) THEN (case THEN (move ["all_n0"])) THEN (move ["_"]) THEN (move ["mem_f"]));
   ((fun arg_tac -> arg_tac (Arg_term (`HD f`))) (term_tac exists_tac));
   ((fun arg_tac -> arg_tac (Arg_term (`~(f = [])`))) (term_tac (have_gen_tac [](move ["f_n0"]))));
   (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`all (\l. ~(l = [])) (list_of_faces L)`))) (term_tac (have_gen_tac []ALL_TAC))));
   ((((use_arg_then2 ("contraL", [contraL])) (disch_tac [])) THEN (clear_assumption "contraL") THEN (DISCH_THEN apply_tac)) THEN (((((use_arg_then2 ("allPn", [allPn]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["f_eq"])) THEN ((use_arg_then2 ("f", [])) (term_tac exists_tac)) THEN (done_tac));
   (((((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("all_map", [all_map]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("preim", [preim]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("allP", [allP]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["x"]) THEN (move ["x_L"]) THEN (simp_tac));
   (((use_arg_then2 ("list_pairs_empty", [list_pairs_empty]))(thm_tac (new_rewrite [] []))));
   ((((use_arg_then2 ("all_n0", [])) (disch_tac [])) THEN (clear_assumption "all_n0") THEN BETA_TAC) THEN ((((use_arg_then2 ("allP", [allP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((fun arg_tac ->  (conv_thm_tac DISCH_THEN)  (fun fst_arg -> (use_arg_then2 ("x_L", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac MP_TAC))) THEN (done_tac));
   ((fun arg_tac -> arg_tac (Arg_term (`MEM (HD f) f`))) (term_tac (have_gen_tac [](move ["mem_hd"]))));
   ((((use_arg_then2 ("f_n0", [])) (disch_tac [])) THEN (clear_assumption "f_n0") THEN ((use_arg_then2 ("f", [])) (disch_tac [])) THEN (clear_assumption "f") THEN case THEN ((TRY done_tac)) THEN (move ["h"]) THEN (move ["t"])) THEN ((((use_arg_then2 ("HD", [HD]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (((use_arg_then2 ("dart_in_face", [dart_in_face]))(thm_tac (new_rewrite [] []))));
   ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`find_face L (HD f) = f`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))) ((ALL_TAC) THEN (done_tac)));
   (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("uniq_face_unique", [uniq_face_unique])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`HD f`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
   (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`MEM (HD f) (list_of_darts L)`))) (term_tac (have_gen_tac [](move ["mem_hd2"])))));
   (((((use_arg_then2 ("mem_find_face", [mem_find_face]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
   (((((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("f", [])) (term_tac exists_tac)) THEN (done_tac));
];;

(* Lemma face_set_eq_list *)
let face_set_eq_list = Sections.section_proof ["L"]
`good_list L
	==> face_set (hypermap_of_list L) = set_of_list (faces_of_list L)`
[
   ((BETA_TAC THEN (move ["good_s"])) THEN (((use_arg_then2 ("good_s", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniq_s"])) THEN (case THEN (move ["all_n0"])) THEN (move ["_"])));
   ((((use_arg_then2 ("face_set", [face_set]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("face_map", [face_map]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart", [dart]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("tuple_hypermap_of_list", [tuple_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac)));
   (((((use_arg_then2 ("set_of_orbits", [set_of_orbits]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (move ["f"]));
   ((((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))));
   ((THENL) (split_tac) [((case THEN (move ["d"])) THEN (case THEN (move ["mem_d"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))); ALL_TAC]);
   ((((use_arg_then2 ("f_list_ext_orbit", [f_list_ext_orbit]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("faces_of_list", [faces_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM_MAP", [MEM_MAP]))(thm_tac (new_rewrite [] [])))));
   (((fun arg_tac -> arg_tac (Arg_term (`find_face L d`))) (term_tac exists_tac)) THEN (((use_arg_then2 ("mem_find_face", [mem_find_face]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
   (((((use_arg_then2 ("faces_of_list", [faces_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM_MAP", [MEM_MAP]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["ff"])) THEN (case THEN (move ["mem_ff"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
   ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("mem_face_lemma", [mem_face_lemma])) (fun fst_arg -> (use_arg_then2 ("good_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem_ff", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["d"]) THEN (case THEN (move ["mem_d"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))));
   (((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("f_list_ext_orbit", [f_list_ext_orbit]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma components_hypermap_of_list *)
let components_hypermap_of_list = Sections.section_proof ["L"]
`good_list L
	==> dart (hypermap_of_list L) = darts_of_list L
	/\ edge_map (hypermap_of_list L) = e_list_ext L
 	/\ node_map (hypermap_of_list L) = n_list_ext L
	/\ face_map (hypermap_of_list L) = f_list_ext L`
[
   (BETA_TAC THEN (move ["good_s"]));
   ((((use_arg_then2 ("dart", [dart]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("edge_map", [edge_map]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("node_map", [node_map]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("face_map", [face_map]))(thm_tac (new_rewrite [] [])))));
   ((((use_arg_then2 ("tuple_hypermap_of_list", [tuple_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma node_of_list_lemma *)
let node_of_list_lemma = Sections.section_proof ["x";"L"]
`set_of_list (filter (\d. FST d = x) (list_of_darts L))
	= {(x, y) | y | (x, y) IN darts_of_list L}`
[
   (((((use_arg_then2 ("set_of_list_filter", [set_of_list_filter]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(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 ["y"])) THEN (move ["h"])); ((case THEN (move ["y"])) THEN (move ["h"]))]);
   (((fun arg_tac -> arg_tac (Arg_term (`SND d`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("h", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("PAIR", [PAIR]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN (done_tac));
];;

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

(* Lemma set_nodes_of_list *)
let set_nodes_of_list = Sections.section_proof ["L"]
`set_of_list (nodes_of_list L)
	= {{(x, y) | y | (x, y) IN darts_of_list L} | x | x IN elements_of_list L}`
[
   ((((use_arg_then2 ("nodes_of_list", [nodes_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_nodes", [list_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("SET_OF_LIST_MAP", [SET_OF_LIST_MAP]))(thm_tac (new_rewrite [] []))))));
   ((repeat_tactic 1 9 (((use_arg_then2 ("image_lemma", [image_lemma]))(gsym_then (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 ("elements_of_list", [elements_of_list]))(gsym_then (thm_tac (new_rewrite [] []))))));
   (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(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) (split_tac) [((case THEN (move ["n"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["i"])) THEN (move ["h"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))); ((case THEN (move ["i"])) THEN (move ["h"]))]);
   (((use_arg_then2 ("i", [])) (term_tac exists_tac)) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("node_of_list_lemma", [node_of_list_lemma]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((fun arg_tac -> arg_tac (Arg_term (`filter (\d. FST d = i) (list_of_darts L)`))) (term_tac exists_tac));
   ((((use_arg_then2 ("node_of_list_lemma", [node_of_list_lemma]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("h", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac));
   (((use_arg_then2 ("i", [])) (term_tac exists_tac)) THEN (done_tac));
];;

(* Lemma good_list_node *)
let good_list_node = Sections.section_proof ["L";"d"]
`good_list L /\ good_list_nodes L /\ d IN darts_of_list L
	==> node (hypermap_of_list L) d = {(FST d, y) | y | (FST d, y) IN darts_of_list L}`
[
   ((((use_arg_then2 ("good_list_nodes", [good_list_nodes]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("node_set", [node_set]))(thm_tac (new_rewrite [] [])))) THEN (((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 [] []))))));
   (((((use_arg_then2 ("set_nodes_of_list", [set_nodes_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(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 ["good_s"])) THEN (case THEN (move ["eq"])) THEN (move ["d_in"]));
   (((fun arg_tac -> (use_arg_then2 ("eq", [])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`node (hypermap_of_list L) d`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC);
   ((fun arg_tac -> arg_tac (Arg_term (`?x. _ x`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac)))));
   (((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
   ((BETA_TAC THEN (case THEN (move ["x"])) THEN (case THEN (move ["x_in"])) THEN (move ["eq"])) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))));
   ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`x = FST d`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))) ((ALL_TAC) THEN (done_tac)));
   ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("node_refl", [node_refl])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list L`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d", [])) (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 ("eq", []))(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 ["y"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma prev_el_list_pairs_general *)
let prev_el_list_pairs_general = Sections.section_proof ["x";"y";"s"]
`MEM (x,y) (list_pairs s)
	==> ?z. prev_el (list_pairs s) (x,y) = (z,x) /\ MEM (z,x) (list_pairs s)`
[
   (BETA_TAC THEN (move ["mem_xy"]));
   ((fun arg_tac -> arg_tac (Arg_term (`FST (prev_el (list_pairs s) (x,y))`))) (term_tac (set_tac "z")));
   ((use_arg_then2 ("z", [])) (term_tac exists_tac));
   ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`_1 = _2`))) (term_tac (have_gen_tac [](move ["eq"]))))) (((((use_arg_then2 ("eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
   ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`SND (prev_el (list_pairs s) (x,y)) = x`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [2] []))))))))) (((((use_arg_then2 ("z_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("PAIR", [PAIR]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
   ((((fun arg_tac -> (use_arg_then2 ("prev_el_alt", [prev_el_alt])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x,x`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
   ((fun arg_tac -> arg_tac (Arg_term (`indexl (x,y) _`))) (term_tac (set_tac "k")));
   ((fun arg_tac -> arg_tac (Arg_term (`sizel s`))) (term_tac (set_tac "n")));
   ((fun arg_tac -> arg_tac (Arg_term (`k < n:num`))) (term_tac (have_gen_tac [](move ["k_lt"]))));
   (((((use_arg_then2 ("k_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("n_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((fun arg_tac -> arg_tac (Arg_term (`nth x s k = x`))) (term_tac (have_gen_tac [](move ["nth_s"]))));
   ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nth_index", [nth_index])) (fun fst_arg -> (use_arg_then2 ("mem_xy", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x,x`))) (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 ("k_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth_zip", [nth_zip]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((((use_arg_then2 ("nth_shift_right", [nth_shift_right]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))));
   (((fun arg_tac -> arg_tac (Arg_term (`k = 0`))) (disch_eq_tac "eq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
   ((THENL_LAST) ((((use_arg_then2 ("nth_zip", [nth_zip]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("SND", [SND]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth_shift_left", [nth_shift_left]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) (((((use_arg_then2 ("eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("nth_s", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
   ((((use_arg_then2 ("n_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("k_lt", [])) (disch_tac [])) THEN (clear_assumption "k_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
   ((THENL_FIRST) ((((use_arg_then2 ("nth_zip", [nth_zip]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("SND", [SND]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth_shift_left", [nth_shift_left]))(thm_tac (new_rewrite [] []))))) ((((use_arg_then2 ("n_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("k_lt", [])) (disch_tac [])) THEN (clear_assumption "k_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
   ((THENL_FIRST) (((use_arg_then2 ("subnK", [subnK]))(thm_tac (new_rewrite [] [])))) ((((use_arg_then2 ("eq", [])) (disch_tac [])) THEN (clear_assumption "eq") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
   (((((use_arg_then2 ("nth_s", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_def", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("k_lt", [])) (disch_tac [])) THEN (clear_assumption "k_lt") THEN ((use_arg_then2 ("eq", [])) (disch_tac [])) THEN (clear_assumption "eq") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
];;

(* Lemma n_list_ext_fst *)
let n_list_ext_fst = Sections.section_proof ["x";"y";"L"]
`good_list L /\ (x,y) IN darts_of_list L
	==> ?z. n_list_ext L (x,y) = (x,z) /\ (x,z) IN darts_of_list L`
[
   (BETA_TAC THEN (case THEN ((move ["good_s"]) THEN (move ["xy_in"]))));
   ((((use_arg_then2 ("xy_in", [])) (disch_tac [])) THEN BETA_TAC) THEN (((((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] []))))) THEN (move ["mem_xy"])));
   ((fun arg_tac -> (use_arg_then2 ("prev_el_list_pairs_general", [prev_el_list_pairs_general])) (fun fst_arg -> (use_arg_then2 ("mem_xy", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["z"]) THEN (case THEN ((move ["eq"]) THEN (move ["mem_zx"])))))));
   ((use_arg_then2 ("z", [])) (term_tac exists_tac));
   ((fun arg_tac -> arg_tac (Arg_term (`_1 = _2`))) (term_tac (have_gen_tac [](move ["n_eq"]))));
   (((((use_arg_then2 ("n_list_ext", [n_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_list", [n_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("xy_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((((use_arg_then2 ("n_eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("n_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((TRY done_tac)));
   (((((use_arg_then2 ("lemma_dart_invariant", [lemma_dart_invariant]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma list_ext_power_in_darts *)
let list_ext_power_in_darts = Sections.section_proof ["d";"L";"n"]
`good_list L /\ d IN darts_of_list L
	==> (e_list_ext L POWER n) d IN darts_of_list L /\
	    (n_list_ext L POWER n) d IN darts_of_list L /\
	    (f_list_ext L POWER n) d IN darts_of_list L`
[
   ((BETA_TAC THEN (case THEN (move ["good_s"]))) THEN (((repeat_tactic 1 9 (((use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((TRY done_tac))) THEN (move ["d_in"])));
   ((((use_arg_then2 ("lemma_dart_invariant_power_node", [lemma_dart_invariant_power_node]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
   ((((use_arg_then2 ("lemma_dart_invariant_power_face", [lemma_dart_invariant_power_face]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))));
   (((use_arg_then2 ("Hypermap_iso.IN_TRANS", [Hypermap_iso.IN_TRANS])) (thm_tac apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`edge (hypermap_of_list L) d`))) (term_tac exists_tac)));
   (((((use_arg_then2 ("lemma_edge_subset", [lemma_edge_subset]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("lemma_in_edge2", [lemma_in_edge2]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma fst_n_list_ext_power *)
let fst_n_list_ext_power = Sections.section_proof ["x";"y";"L";"n"]
`good_list L /\ x,y IN darts_of_list L
	==> FST ((n_list_ext L POWER n) (x,y)) = x`
[
   (BETA_TAC THEN (case THEN ((move ["good_s"]) THEN (move ["xy_in"]))));
   ((THENL_FIRST) ((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)));
   ((fun arg_tac -> arg_tac (Arg_term (`(n_list_ext L POWER n) (x,y)`))) (term_tac (set_tac "d")));
   ((((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 ("d_def", []))(thm_tac (new_rewrite [] [])))));
   ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("n_list_ext_fst", [n_list_ext_fst])) (fun fst_arg -> (use_arg_then2 ("good_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`FST d`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`SND d`))) (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 ("PAIR", [PAIR]))(thm_tac (new_rewrite [] [])))) THEN (ANTS_TAC));
   (((((use_arg_then2 ("d_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("list_ext_power_in_darts", [list_ext_power_in_darts]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((BETA_TAC THEN (case THEN (move ["z"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma mem_list_pairs_exists *)
let mem_list_pairs_exists = Sections.section_proof ["x";"l"]
`MEM x l <=> ?y. MEM (x,y) (list_pairs l)`
[
   ((THENL) (split_tac) [(move ["mem_x"]); ((case THEN (move ["y"])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("mem_list_pairs", [mem_list_pairs])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (simp_tac))]);
   ((fun arg_tac -> arg_tac (Arg_term (`next_el l x`))) (term_tac exists_tac));
   (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nthP", [nthP])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x,next_el l x`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x,x`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [])))));
   ((fun arg_tac -> arg_tac (Arg_term (`indexl x l`))) (term_tac exists_tac));
   ((((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_x", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))));
   ((((use_arg_then2 ("nth_list_pairs", [nth_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("nth_index", [nth_index]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
   ((((use_arg_then2 ("next_el", [next_el]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth0", [nth0]))(gsym_then (thm_tac (new_rewrite [] []))))));
   ((((fun arg_tac -> arg_tac (Arg_term (`indexl x l = _`))) (disch_tac [])) THEN case THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma mem_list_of_darts *)
let mem_list_of_darts = Sections.section_proof ["d";"L"]
`MEM d (list_of_darts L)
	<=> ?l. MEM l L /\ MEM d (list_pairs l)`
[
   ((THENL_LAST) ((THENL) (split_tac) [ALL_TAC; ((case THEN (move ["l"])) THEN (case THEN ((move ["mem_l"]) THEN (move ["mem_d"]))))]) (((use_arg_then2 ("dart_in_darts", [dart_in_darts])) (thm_tac apply_tac)) THEN ((use_arg_then2 ("l", [])) (term_tac exists_tac)) THEN (done_tac)));
   (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))));
   ((((use_arg_then2 ("list_of_darts", [list_of_darts]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] [])))));
   ((THENL_FIRST) (case THEN (move ["mem_d"])) (((use_arg_then2 ("h", [])) (term_tac exists_tac)) THEN (done_tac)));
   (((fun arg_tac -> (use_arg_then2 ("Ih", [])) (fun fst_arg -> (use_arg_then2 ("mem_d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (case THEN (move ["l"])) THEN (case THEN (move ["mem_l"])) THEN (move ["mem_d2"]));
   (((use_arg_then2 ("l", [])) (term_tac exists_tac)) THEN (done_tac));
];;

(* Lemma mem_list_of_elements *)
let mem_list_of_elements = Sections.section_proof ["x";"L"]
`MEM x (list_of_elements L)
	<=> ?y. MEM (x,y) (list_of_darts L)`
[
   ((((use_arg_then2 ("list_of_elements", [list_of_elements]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_undup", [mem_undup]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_list_of_darts", [mem_list_of_darts]))(thm_tac (new_rewrite [] [])))));
   ((((use_arg_then2 ("SWAP_EXISTS_THM", [SWAP_EXISTS_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("RIGHT_EXISTS_AND_THM", [RIGHT_EXISTS_AND_THM]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))));
   ((((use_arg_then2 ("mem_list_pairs_exists", [mem_list_pairs_exists]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma uniq_node *)
let uniq_node = Sections.section_proof ["L";"n"]
`good_list L /\ MEM n (list_of_nodes L) ==> uniq n`
[
   (((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_nodes", [list_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM_MAP", [MEM_MAP]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["uniq_s"])) THEN (move ["_"]) THEN (case THEN (move ["d"])) THEN (case THEN (move ["mem_d"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
   ((((use_arg_then2 ("filter_uniq", [filter_uniq]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma uniq_face *)
let uniq_face = Sections.section_proof ["L";"f"]
`good_list L /\ MEM f (list_of_faces L) ==> uniq f`
[
   ((BETA_TAC THEN (case THEN ((move ["good_s"]) THEN (move ["mem_f"])))) THEN (((use_arg_then2 ("good_s", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN (move ["h"])));
   ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("mem_face_lemma", [mem_face_lemma])) (fun fst_arg -> (use_arg_then2 ("mem_f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("good_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["d"]) THEN (case THEN (move ["mem_d"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))));
   ((((use_arg_then2 ("uniq_find_face", [uniq_find_face]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma list_of_darts_nil *)
let list_of_darts_nil = Sections.section_proof []
`list_of_darts [] = []`
[
   (((((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL foldr)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma list_of_darts_cons *)
let list_of_darts_cons = Sections.section_proof ["h";"t"]
`list_of_darts (h :: t) = list_pairs h ++ list_of_darts t`
[
   (((((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL foldr)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("list_of_darts", [list_of_darts]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Lemma list_of_darts_cat *)
let list_of_darts_cat = Sections.section_proof ["s1";"s2"]
`list_of_darts (s1 ++ s2) = list_of_darts s1 ++ list_of_darts s2`
[
   (((THENL) (((use_arg_then2 ("s1", [])) (disch_tac [])) THEN (clear_assumption "s1") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((fun arg_tac ->(use_arg_then2 ("list_of_darts_nil", [list_of_darts_nil]))(fun tmp_arg1 -> (use_arg_then2 ("list_of_darts_cons", [list_of_darts_cons]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))));
   (((((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("catA", [catA]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma good_list_uniq *)
let good_list_uniq = Sections.section_proof ["L"]
`good_list L ==> uniq L`
[
   ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniqL"])) THEN (case THEN (move ["allL"])) THEN (move ["_"]));
   (((THENL) (((use_arg_then2 ("uniqL", [])) (disch_tac [])) THEN (clear_assumption "uniqL") THEN ((use_arg_then2 ("allL", [])) (disch_tac [])) THEN (clear_assumption "allL") THEN ((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL uniq)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))));
   (((((use_arg_then2 ("all", [all]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("list_of_darts_cons", [list_of_darts_cons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat_uniq", [cat_uniq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hasPn", [hasPn]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["h_neq"])) THEN (move ["all_t"]) THEN (case THEN (move ["_"])) THEN (case THEN (move ["mem_h"])) THEN (move ["uniq_t"]));
   ((((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))));
   ((fun arg_tac -> arg_tac (Arg_term (`?d. MEM d (list_pairs h)`))) (term_tac (have_gen_tac [](case THEN ((move ["d"]) THEN (move ["mem_d"]))))));
   ((THENL_LAST) (((THENL) (((fun arg_tac -> arg_tac (Arg_term (`list_pairs h`))) (disch_eq_tac "eq" [])) THEN case) [ALL_TAC; ((move ["h'"]) THEN (move ["t'"]))]) THEN (process_fst_eq_tac)) (((use_arg_then2 ("h'", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
   ((((use_arg_then2 ("eq", [])) (disch_tac [])) THEN (clear_assumption "eq") THEN BETA_TAC) THEN ((((use_arg_then2 ("size_eq0", [size_eq0]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_eq0", [size_eq0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("h_neq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((((use_arg_then2 ("mem_h", [])) (disch_tac [])) THEN (clear_assumption "mem_h") THEN ((use_arg_then2 ("contraL", [contraL])) (disch_tac [])) THEN (clear_assumption "contraL") THEN (DISCH_THEN apply_tac)) THEN (((((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 (move ["mem_h"])));
   (((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))));
   ((((use_arg_then2 ("mem_list_of_darts", [mem_list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN ((use_arg_then2 ("h", [])) (term_tac exists_tac)) THEN (done_tac));
];;

(* Lemma list_pairs_inj *)
let list_pairs_inj = Sections.section_proof ["s1";"s2"]
`list_pairs s1 = list_pairs s2 ==> s1 = s2`
[
   ((repeat_tactic 1 9 (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] []))))) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("congr1", [congr1])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`unzip1`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))));
   (((repeat_tactic 1 9 (((use_arg_then2 ("unzip1_zip", [unzip1_zip]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqnn", [leqnn]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma uniq_list_of_faces *)
let uniq_list_of_faces = Sections.section_proof ["L"]
`good_list L ==> uniq (list_of_faces L)`
[
   ((((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))) THEN (move ["goodL"]));
   ((((((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("map_inj_uniq", [map_inj_uniq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("good_list_uniq", [good_list_uniq]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (move ["x"]) THEN (move ["y"]) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("list_pairs_inj", [list_pairs_inj])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (done_tac));
];;

(* Lemma uniq_faces_of_list *)
let uniq_faces_of_list = Sections.section_proof ["L"]
`good_list L ==> uniq (faces_of_list L)`
[
   ((((use_arg_then2 ("faces_of_list", [faces_of_list]))(thm_tac (new_rewrite [] [])))) THEN (move ["goodL"]));
   (((((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("map_inj_in_uniq", [map_inj_in_uniq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uniq_list_of_faces", [uniq_list_of_faces]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (move ["f1"]) THEN (move ["f2"]) THEN (case THEN ALL_TAC) THEN (case THEN ((move ["mem1"]) THEN (move ["mem2"]))) THEN (move ["eq"]));
   ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("mem_face_lemma", [mem_face_lemma])) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN (move ["d"]))));
   ((((use_arg_then2 ("dart_in_face", [dart_in_face]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["mem_d"])) THEN (move ["f1_eq"]));
   (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("uniq_face_unique", [uniq_face_unique])) (fun fst_arg -> (use_arg_then2 ("mem1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
   ((THENL_FIRST) (((((use_arg_then2 ("f1_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (split_tac)) ((((use_arg_then2 ("goodL", [])) (disch_tac [])) THEN (clear_assumption "goodL") THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
   (((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f1_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma card_faces_of_list *)
let card_faces_of_list = Sections.section_proof ["L"]
`good_list L
	==> CARD (face_set (hypermap_of_list L)) = sizel (list_of_faces L)`
[
   ((BETA_TAC THEN (move ["goodL"])) THEN ((((use_arg_then2 ("face_set_eq_list", [face_set_eq_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))));
   ((((use_arg_then2 ("card_set_of_list_uniq", [card_set_of_list_uniq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uniq_faces_of_list", [uniq_faces_of_list]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
   (((((use_arg_then2 ("faces_of_list", [faces_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_map", [size_map]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma card_darts_of_list *)
let card_darts_of_list = Sections.section_proof ["L"]
`good_list L 
	==> CARD (dart (hypermap_of_list L)) = sizel (list_of_darts L)`
[
   (BETA_TAC THEN (move ["goodL"]));
   ((((use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("card_set_of_list_uniq", [card_set_of_list_uniq]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
   ((((use_arg_then2 ("goodL", [])) (disch_tac [])) THEN (clear_assumption "goodL") THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma uniq_list_of_elements *)
let uniq_list_of_elements = Sections.section_proof ["L"]
`uniq (list_of_elements L)`
[
   (((((use_arg_then2 ("list_of_elements", [list_of_elements]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("undup_uniq", [undup_uniq]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma uniq_list_of_nodes *)
let uniq_list_of_nodes = Sections.section_proof ["L"]
`uniq (list_of_nodes L)`
[
   (((((use_arg_then2 ("list_of_nodes", [list_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("map_inj_in_uniq", [map_inj_in_uniq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uniq_list_of_elements", [uniq_list_of_elements]))(thm_tac (new_rewrite [] []))))) THEN ((simp_tac THEN TRY done_tac))) THEN (move ["a"]) THEN (move ["b"]));
   ((repeat_tactic 1 9 (((use_arg_then2 ("mem_list_of_elements", [mem_list_of_elements]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN ALL_TAC) THEN (case THEN ((move ["c"]) THEN (move ["mem_a"]))) THEN (case THEN ((move ["d"]) THEN (move ["mem_b"]))));
   (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("congr1", [congr1])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`MEM (a,c)`))) (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 (DISCH_THEN (fun snd_th -> (use_arg_then2 ("EQ_IMP", [EQ_IMP])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("mem_a", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma mem_not_nil *)
let mem_not_nil = Sections.section_proof ["s"]
`~(s = []) <=> (?x. MEM x s)`
[
   (((THENL) (((use_arg_then2 ("s", [])) (disch_tac [])) THEN (clear_assumption "s") THEN case) [ALL_TAC; ((move ["h"]) THEN (move ["t"]))]) THEN ((((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("NOT_CONS_NIL", [NOT_CONS_NIL]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ((use_arg_then2 ("h", [])) (term_tac exists_tac)) THEN (done_tac));
];;

(* Lemma node_of_list_not_nil *)
let node_of_list_not_nil = Sections.section_proof ["L";"n"]
`MEM n (list_of_nodes L) ==> ~(n = [])`
[
   (((((use_arg_then2 ("list_of_nodes", [list_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mapP", [mapP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_list_of_elements", [mem_list_of_elements]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["a"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["b"])) THEN (move ["mem_ab"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
   (((((use_arg_then2 ("mem_not_nil", [mem_not_nil]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`a,b`))) (term_tac exists_tac)));
   (((((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("mem_ab", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma nodes_of_list_eq *)
let nodes_of_list_eq = Sections.section_proof ["L";"n1";"n2";"a"]
`MEM n1 (list_of_nodes L) /\ MEM n2 (list_of_nodes L) /\
	MEM a n1 /\ MEM a n2 ==> n1 = n2`
[
   ((((use_arg_then2 ("list_of_nodes", [list_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("mapP", [mapP]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("mem_list_of_elements", [mem_list_of_elements]))(thm_tac (new_rewrite [] [])))));
   (BETA_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["x"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["y"])) THEN (move ["mem_xy"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (case THEN ALL_TAC) THEN (case THEN (move ["u"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["v"])) THEN (move ["mem_uv"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
   ((((repeat_tactic 1 9 (((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Lemma uniq_nodes_of_list *)
let uniq_nodes_of_list = Sections.section_proof ["L"]
`uniq (nodes_of_list L)`
[
   (((((use_arg_then2 ("nodes_of_list", [nodes_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("map_inj_in_uniq", [map_inj_in_uniq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uniq_list_of_nodes", [uniq_list_of_nodes]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (move ["n1"]) THEN (move ["n2"]) THEN (case THEN ALL_TAC) THEN (case THEN ((move ["mem1"]) THEN (move ["mem2"]))) THEN (move ["eq"]));
   ((fun arg_tac -> arg_tac (Arg_term (`?d. d IN set_of_list n1`))) (term_tac (have_gen_tac [](case THEN ((move ["d"]) THEN (move ["d_in"]))))));
   (((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_not_nil", [mem_not_nil]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("node_of_list_not_nil", [node_of_list_not_nil])) (fun fst_arg -> (use_arg_then2 ("mem1", [])) (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 ("nodes_of_list_eq", [nodes_of_list_eq])) (fun fst_arg -> (use_arg_then2 ("mem1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)) THEN ((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Lemma size_list_of_nodes *)
let size_list_of_nodes = Sections.section_proof ["L"]
`sizel (list_of_nodes L) = sizel (list_of_elements L)`
[
   (((((use_arg_then2 ("list_of_nodes", [list_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_map", [size_map]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma card_nodes_of_list *)
let card_nodes_of_list = Sections.section_proof ["L"]
`CARD (set_of_list (nodes_of_list L)) = sizel (list_of_elements L)`
[
   ((((use_arg_then2 ("card_set_of_list_uniq", [card_set_of_list_uniq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uniq_nodes_of_list", [uniq_nodes_of_list]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
   (((((use_arg_then2 ("nodes_of_list", [nodes_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_map", [size_map]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_list_of_nodes", [size_list_of_nodes]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma surj_delete *)
let surj_delete = Sections.section_proof ["f";"s";"t";"a";"b"]
`SURJ f s t /\ f a = f b /\ a IN s /\ b IN s /\ ~(a = b)
	==> SURJ f (s DELETE a) t`
[
   ((((repeat_tactic 1 9 (((use_arg_then2 ("SURJ", [SURJ]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_DELETE", [IN_DELETE]))(thm_tac (new_rewrite [] [])))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN ((move ["f_in"]) THEN (move ["f_surj"]))) THEN (case THEN (move ["eq"])) THEN (case THEN (move ["a_in"])) THEN (case THEN (move ["b_in"])) THEN (move ["neq"])) THEN (split_tac));
   ((BETA_TAC THEN (move ["x"]) THEN (case THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("f_in", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (BETA_TAC THEN (move ["x"]) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("f_surj", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (case THEN (move ["y"])) THEN (case THEN (move ["y_in"])) THEN (move ["f_eq"]));
   ((THENL_LAST) (((fun arg_tac -> arg_tac (Arg_term (`y = a`))) (disch_eq_tac "y_eq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) (((use_arg_then2 ("y", [])) (term_tac exists_tac)) THEN (done_tac)));
   (((use_arg_then2 ("b", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("b_in", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("neq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("y_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma fst_node_hypermap_of_list *)
let fst_node_hypermap_of_list = Sections.section_proof ["L";"d"]
`good_list L
	==> (!x. x IN node (hypermap_of_list L) d ==> FST x = FST d)`
[
   (((use_arg_then2 ("d", [])) (disch_tac [])) THEN (clear_assumption "d") THEN BETA_TAC THEN (case THEN ((move ["a"]) THEN (move ["b"]))) THEN (move ["goodL"]) THEN (move ["x"]));
   ((fun arg_tac -> (use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list])) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["hypL"])));
   ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list L`))) (term_tac (set_tac "H")));
   ((THENL_ROT (-1)) (((fun arg_tac -> arg_tac (Arg_term (`a,b IN darts_of_list L`))) (disch_eq_tac "ab_in" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)));
   ((((((use_arg_then2 ("lemma_node_exception", [lemma_node_exception]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("hypL", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) 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));
   (((((use_arg_then2 ("node", [node]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("orbit_map", [orbit_map]))(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 ["k"])) THEN (case THEN (move ["_"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
   (((((use_arg_then2 ("hypL", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fst_n_list_ext_power", [fst_n_list_ext_power]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma fst_choice_node_hypermap_of_list *)
let fst_choice_node_hypermap_of_list = Sections.section_proof ["L";"d"]
`good_list L
	==> FST (CHOICE (node (hypermap_of_list L) d)) = FST d`
[
   ((BETA_TAC THEN (move ["goodL"])) THEN (((fun arg_tac -> (use_arg_then2 ("fst_node_hypermap_of_list", [fst_node_hypermap_of_list])) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)));
   ((((use_arg_then2 ("CHOICE_DEF", [CHOICE_DEF]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEMBER_NOT_EMPTY", [MEMBER_NOT_EMPTY]))(gsym_then (thm_tac (new_rewrite [] []))))));
   (((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("node_refl", [node_refl]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma surj_fst_nodes_hypermap_of_list *)
let surj_fst_nodes_hypermap_of_list = Sections.section_proof ["L"]
`good_list L
	==> SURJ (\n. FST (CHOICE n)) (node_set (hypermap_of_list L)) (elements_of_list L)`
[
   (((((use_arg_then2 ("SURJ", [SURJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("elements_of_list", [elements_of_list]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))))) THEN (move ["goodL"]));
   ((fun arg_tac -> (use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list])) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["hypL"])));
   ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list L`))) (term_tac (set_tac "H")));
   (((THENL) (split_tac) [((move ["x"]) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_node_representation", [lemma_node_representation])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (case THEN (move ["d"])) THEN (case THEN (move ["d_in"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))); (move ["a"])]) THEN (simp_tac));
   ((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("fst_choice_node_hypermap_of_list", [fst_choice_node_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("mem_list_of_elements", [mem_list_of_elements]))(thm_tac (new_rewrite [] [])))));
   (((fun arg_tac -> arg_tac (Arg_term (`SND d`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hypL", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("pair_expand", [pair_expand]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
   ((((use_arg_then2 ("mem_list_of_elements", [mem_list_of_elements]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["b"])));
   (((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hypL", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["ab_in"]));
   ((fun arg_tac -> arg_tac (Arg_term (`node H (a,b)`))) (term_tac exists_tac));
   ((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("fst_choice_node_hypermap_of_list", [fst_choice_node_hypermap_of_list])) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))));
   ((((use_arg_then2 ("lemma_in_node_set", [lemma_in_node_set]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma good_list_nodes_condition *)
let good_list_nodes_condition = Sections.section_proof ["L"]
`good_list L
   ==> (good_list_nodes L <=> CARD (node_set (hypermap_of_list L)) = sizel (list_of_elements L))`
[
   ((THENL_FIRST) (((((use_arg_then2 ("good_list_nodes", [good_list_nodes]))(thm_tac (new_rewrite [] [])))) THEN (move ["goodL"])) THEN ((split_tac) THEN (move ["eq"]))) (((((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("card_nodes_of_list", [card_nodes_of_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
   (((((use_arg_then2 ("SUBSET_CARD_EQ", [SUBSET_CARD_EQ]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("card_nodes_of_list", [card_nodes_of_list]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("FINITE_SET_OF_LIST", [FINITE_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] []))))) THEN (move ["n"]));
   ((fun arg_tac -> (use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list])) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["hypL"])));
   ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list L`))) (term_tac (set_tac "H")));
   ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_node_representation", [lemma_node_representation])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (case THEN (move ["r"])) THEN (case THEN (move ["r_in"])) THEN (move ["n_eq"]));
   ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`MEM r (list_of_darts L)`))) (term_tac (have_gen_tac [](move ["mem_r"])))) (((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hypL", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)));
   ((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nodes_of_list", [nodes_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mapP", [mapP]))(thm_tac (new_rewrite [] [])))));
   (((fun arg_tac -> arg_tac (Arg_term (`filter (\y. FST y = FST r) (list_of_darts L)`))) (term_tac exists_tac)) THEN (split_tac));
   ((((use_arg_then2 ("list_of_nodes", [list_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mapP", [mapP]))(thm_tac (new_rewrite [] [])))));
   ((((fun arg_tac -> arg_tac (Arg_term (`FST r`))) (term_tac exists_tac)) THEN (simp_tac)) THEN (((use_arg_then2 ("mem_list_of_elements", [mem_list_of_elements]))(thm_tac (new_rewrite [] [])))));
   (((fun arg_tac -> arg_tac (Arg_term (`SND r`))) (term_tac exists_tac)) THEN (((use_arg_then2 ("pair_expand", [pair_expand]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((fun arg_tac -> arg_tac (Arg_term (`set_of_list _`))) (term_tac (set_tac "s")));
   (((use_arg_then2 ("eq", [])) (disch_tac [])) THEN (clear_assumption "eq") THEN ((use_arg_then2 ("contraLR", [contraLR])) (disch_tac [])) THEN (clear_assumption "contraLR") THEN (DISCH_THEN apply_tac) THEN (move ["neq"]));
   ((fun arg_tac -> arg_tac (Arg_term (`n PSUBSET s`))) (term_tac (have_gen_tac []ALL_TAC)));
   (((((use_arg_then2 ("PSUBSET", [PSUBSET]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("neq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("s_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["x"]) THEN (move ["x_in"]));
   ((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hypL", []))(gsym_then (thm_tac (new_rewrite [] []))))));
   ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fst_node_hypermap_of_list", [fst_node_hypermap_of_list])) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (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));
   (((use_arg_then2 ("Hypermap_iso.IN_TRANS", [Hypermap_iso.IN_TRANS])) (thm_tac apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`node H r`))) (term_tac exists_tac)));
   (((((use_arg_then2 ("lemma_node_subset", [lemma_node_subset]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
   ((((use_arg_then2 ("PSUBSET_ALT", [PSUBSET_ALT]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["_"])) THEN (case THEN (move ["a"])) THEN (case THEN (move ["a_in"])) THEN (move ["a_n_in"]));
   ((fun arg_tac -> arg_tac (Arg_term (`~(sizel (list_of_elements L) = 0)`))) (term_tac (have_gen_tac [](move ["size_gt0"]))));
   ((((use_arg_then2 ("size_eq0", [size_eq0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_not_nil", [mem_not_nil]))(thm_tac (new_rewrite [] [])))));
   (((fun arg_tac -> arg_tac (Arg_term (`FST r`))) (term_tac exists_tac)) THEN (((use_arg_then2 ("mem_list_of_elements", [mem_list_of_elements]))(thm_tac (new_rewrite [] [])))));
   (((fun arg_tac -> arg_tac (Arg_term (`SND r`))) (term_tac exists_tac)) THEN (((use_arg_then2 ("pair_expand", [pair_expand]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`sizel (list_of_elements L) <= CARD (node_set H DELETE n) `))) (term_tac (have_gen_tac []ALL_TAC))));
   ((((use_arg_then2 ("CARD_DELETE", [CARD_DELETE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("FINITE_HYPERMAP_ORBITS", [FINITE_HYPERMAP_ORBITS]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("n_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("lemma_in_node_set", [lemma_in_node_set]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("r_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
   ((((use_arg_then2 ("size_gt0", [])) (disch_tac [])) THEN (clear_assumption "size_gt0") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
   ((((use_arg_then2 ("card_set_of_list_uniq", [card_set_of_list_uniq]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uniq_list_of_elements", [uniq_list_of_elements]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("elements_of_list", [elements_of_list]))(gsym_then (thm_tac (new_rewrite [] []))))));
   ((fun arg_tac -> (use_arg_then2 ("Hypermap_iso.surj_imp_card_le", [Hypermap_iso.surj_imp_card_le])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`\x. FST (CHOICE x)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac apply_tac));
   ((((use_arg_then2 ("FINITE_DELETE", [FINITE_DELETE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FINITE_HYPERMAP_ORBITS", [FINITE_HYPERMAP_ORBITS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))));
   (((use_arg_then2 ("surj_delete", [surj_delete])) (thm_tac apply_tac)) THEN (((fun arg_tac -> arg_tac (Arg_term (`node H a`))) (term_tac exists_tac)) THEN (simp_tac)));
   ((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [1; 2] []))))) THEN (((use_arg_then2 ("surj_fst_nodes_hypermap_of_list", [surj_fst_nodes_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fst_choice_node_hypermap_of_list", [fst_choice_node_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
   ((fun arg_tac -> arg_tac (Arg_term (`a IN dart H`))) (term_tac (have_gen_tac [](move ["a_in2"]))));
   ((((use_arg_then2 ("hypL", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))));
   ((((use_arg_then2 ("a_in", [])) (disch_tac [])) THEN (clear_assumption "a_in") THEN BETA_TAC) THEN (((((use_arg_then2 ("s_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((((use_arg_then2 ("n_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("lemma_in_node_set", [lemma_in_node_set]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("a_in2", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("r_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN (((use_arg_then2 ("fst_choice_node_hypermap_of_list", [fst_choice_node_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
   ((((use_arg_then2 ("lemma_different_nodes", [lemma_different_nodes]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("n_eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((simp_tac THEN TRY done_tac)));
   ((((use_arg_then2 ("a_in", [])) (disch_tac [])) THEN (clear_assumption "a_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("s_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac));
];;

(* Lemma plain_hypermap_of_list *)
let plain_hypermap_of_list = Sections.section_proof ["L"]
`good_list L ==> plain_hypermap (hypermap_of_list L)`
[
   ((BETA_TAC THEN (move ["goodL"])) THEN ((fun arg_tac -> (use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list])) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["hypL"]))));
   (((((use_arg_then2 ("plain_hypermap", [plain_hypermap]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hypL", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_list_ext_involution", [e_list_ext_involution]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma edge_CARD_dart *)
let edge_CARD_dart = Sections.section_proof ["H"]
`plain_hypermap H /\ is_edge_nondegenerate H
	==> CARD (dart H) = 2 * number_of_edges H`
[
   (((((use_arg_then2 ("plain_hypermap", [plain_hypermap]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("is_edge_nondegenerate", [is_edge_nondegenerate]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((move ["plain"]) THEN (move ["edge_nd"]))));
   ((((use_arg_then2 ("number_of_edges", [number_of_edges]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("edge_set", [edge_set]))(thm_tac (new_rewrite [] [])))));
   ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("lemma_card_eq", [lemma_card_eq])) (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))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("number_of_orbits", [number_of_orbits]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
   (((repeat_tactic 1 9 (((use_arg_then2 ("edge_map_and_darts", [edge_map_and_darts]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["x"]) THEN (move ["x_in"]));
   ((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL lemma_orbit_of_size_2))) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (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 ("edge_map_and_darts", [edge_map_and_darts]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
   (((((use_arg_then2 ("edge_nd", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) 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 ("plain", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("I_THM", [I_THM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma good_list_nodes_size_condition *)
let good_list_nodes_size_condition = Sections.section_proof ["L"]
`good_list L /\ planar_hypermap (hypermap_of_list L)
     /\ connected_hypermap (hypermap_of_list L) /\ is_edge_nondegenerate (hypermap_of_list L)
	==> (good_list_nodes L <=> 
		2 * (sizel (list_of_elements L) + sizel (list_of_faces L)) =
			sizel (list_of_darts L) + 4)`
[
   (BETA_TAC THEN (case THEN (move ["goodL"])) THEN (case THEN (move ["planarL"])) THEN (case THEN (move ["connL"])) THEN (move ["nondL"]));
   ((((use_arg_then2 ("good_list_nodes_condition", [good_list_nodes_condition]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
   ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list L`))) (term_tac (set_tac "H")));
   ((THENL_FIRST) ((((use_arg_then2 ("number_of_nodes", [number_of_nodes]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("eqn_pmul2l", [eqn_pmul2l])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [])))))) ((arith_tac) THEN (done_tac)));
   ((((use_arg_then2 ("planarL", [])) (disch_tac [])) THEN (clear_assumption "planarL") THEN ((use_arg_then2 ("connL", [])) (disch_tac [])) THEN (clear_assumption "connL") THEN BETA_TAC) THEN (((((use_arg_then2 ("planar_hypermap", [planar_hypermap]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("connected_hypermap", [connected_hypermap]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))));
   ((THENL_FIRST) (((fun arg_tac -> (use_arg_then2 ("eqn_pmul2l", [eqn_pmul2l])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) ((arith_tac) THEN (done_tac)));
   ((repeat_tactic 1 9 (((use_arg_then2 ("muln_addr", [muln_addr]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("edge_CARD_dart", [edge_CARD_dart]))(gsym_then (thm_tac (new_rewrite [] []))))));
   (((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN (((use_arg_then2 ("plain_hypermap_of_list", [plain_hypermap_of_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   ((((use_arg_then2 ("card_faces_of_list", [card_faces_of_list]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("number_of_faces", [number_of_faces]))(gsym_then (thm_tac (new_rewrite [] []))))));
   ((((use_arg_then2 ("card_darts_of_list", [card_darts_of_list]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))));
   ((arith_tac) THEN (done_tac));
];;

(* Lemma face_of_list *)
let face_of_list = Sections.section_proof ["L";"d"]
`good_list L /\ MEM d (list_of_darts L)
	==> face (hypermap_of_list L) d = set_of_list (find_face L d)`
[
   (BETA_TAC THEN (case THEN ((move ["good_s"]) THEN (move ["mem_d"]))));
   ((fun arg_tac -> (use_arg_then2 ("face_set_eq_list", [face_set_eq_list])) (fun fst_arg -> (use_arg_then2 ("good_s", [])) (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 ("face_set", [face_set]))(thm_tac (new_rewrite [] [])))) THEN (((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 [] []))))));
   ((((use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))));
   ((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN ((fun arg_tac ->  (conv_thm_tac DISCH_THEN)  (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`face (hypermap_of_list L) d`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac MP_TAC)));
   ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`face _1 d IN _2`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac))))) (((((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN (done_tac)));
   (((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("faces_of_list", [faces_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM_MAP", [MEM_MAP]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["f"])) THEN (case THEN (move ["mem_f"])) THEN (move ["face_eq"]));
   ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("mem_face_lemma", [mem_face_lemma])) (fun fst_arg -> (use_arg_then2 ("good_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem_f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["d2"]) THEN (case THEN (move ["mem_d2"])) THEN (move ["f_eq"])))));
   (((((use_arg_then2 ("face_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] []))))) THEN ((congr_tac (`_1 _2`)) THEN ((TRY done_tac))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] [])))));
   ((use_arg_then2 ("mem_find_face_imp_faces_eq", [mem_find_face_imp_faces_eq])) (thm_tac apply_tac));
   ((((use_arg_then2 ("good_s", [])) (disch_tac [])) THEN (clear_assumption "good_s") THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac)));
   (((((use_arg_then2 ("f_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("face_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("face_refl", [face_refl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma card_face_of_list *)
let card_face_of_list = Sections.section_proof ["L";"d"]
`good_list L /\ MEM d (list_of_darts L)
	==> CARD (face (hypermap_of_list L) d) = sizel (find_face L d)`
[
   (BETA_TAC THEN (case THEN ((move ["good_s"]) THEN (move ["mem_d"]))));
   ((((use_arg_then2 ("face_of_list", [face_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("card_set_of_list_uniq", [card_set_of_list_uniq]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("uniq_find_face", [uniq_find_face]))(thm_tac (new_rewrite [] [])))));
   ((((use_arg_then2 ("good_s", [])) (disch_tac [])) THEN (clear_assumption "good_s") THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma list_of_faces_k *)
let list_of_faces_k = Sections.section_proof ["L";"k"]
`good_list L
	==> face_set_k k (hypermap_of_list L) =
		set_of_list (MAP set_of_list (filter (\f. sizel f = k) (list_of_faces L)))`
[
   ((BETA_TAC THEN (move ["good_s"])) THEN (((use_arg_then2 ("good_s", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniq_s"])) THEN (move ["_"])));
   ((((use_arg_then2 ("face_set_k", [face_set_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("face_set", [face_set]))(thm_tac (new_rewrite [] [])))) THEN (((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 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
   ((((use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))));
   (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("MEM_MAP", [MEM_MAP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] []))))) THEN (move ["f"]) THEN (simp_tac));
   ((THENL) (split_tac) [((case THEN (move ["g"])) THEN (case THEN ALL_TAC) THEN (case THEN ALL_TAC) THEN (case THEN (move ["d"])) THEN (case THEN (move ["mem_d"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (move ["card_eq"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))); ((case THEN (move ["g"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["size_g"])) THEN (move ["mem_g"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))]);
   ((fun arg_tac -> arg_tac (Arg_term (`find_face L d`))) (term_tac exists_tac));
   (((((use_arg_then2 ("mem_find_face", [mem_find_face]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("face_of_list", [face_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("card_face_of_list", [card_face_of_list]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
   ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("mem_face_lemma", [mem_face_lemma])) (fun fst_arg -> (use_arg_then2 ("good_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem_g", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["d"]) THEN (case THEN (move ["mem_d"])) THEN (move ["g_eq"])))));
   ((((fun arg_tac -> arg_tac (Arg_term (`set_of_list g`))) (term_tac exists_tac)) THEN (simp_tac)) THEN (split_tac));
   (((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("face_of_list", [face_of_list]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
   (((((use_arg_then2 ("card_set_of_list_uniq", [card_set_of_list_uniq]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("g_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("uniq_find_face", [uniq_find_face]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma darts_k_union_face_set_k *)
let darts_k_union_face_set_k = Sections.section_proof ["H";"k"]
`darts_k k H = UNIONS (face_set_k k H)`
[
   (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNIONS", [IN_UNIONS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_k", [darts_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("face_set_k", [face_set_k]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("Hypermap_iso.inE", [Hypermap_iso.inE]))(thm_tac (new_rewrite [] [])))))) THEN (move ["d"]));
   ((THENL) (split_tac) [(move ["h"]); ((case THEN (move ["t"])) THEN (case THEN ALL_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 ["card_eq"]) THEN (move ["d_in"]))]);
   (((fun arg_tac -> arg_tac (Arg_term (`face H d`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("lemma_in_face_set", [lemma_in_face_set]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("face_refl", [face_refl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`face H x = face H d`))) (term_tac (have_gen_tac [](move ["eq"])))));
   (((((use_arg_then2 ("eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("card_eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((fun arg_tac -> (use_arg_then2 ("Hypermap_iso.IN_TRANS", [Hypermap_iso.IN_TRANS])) (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 (((use_arg_then2 ("lemma_face_subset", [lemma_face_subset]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (((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))) (disch_tac [])) THEN (exact_tac));
];;

(* Lemma set_of_list_flatten_map *)
let set_of_list_flatten_map = Sections.section_proof ["s"]
`set_of_list (flatten s) 
	= UNIONS (set_of_list (map set_of_list s))`
[
   (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNIONS", [IN_UNIONS]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mapP", [mapP]))(thm_tac (new_rewrite [] []))))) THEN (move ["x"]));
   ((THENL) (split_tac) [((case THEN (move ["l"])) THEN (move ["h"])); ((case THEN (move ["t"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["l2"])) THEN (case THEN (move ["mem_l2"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))]);
   (((fun arg_tac -> arg_tac (Arg_term (`set_of_list l`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("l", [])) (term_tac exists_tac)) THEN (done_tac));
   (((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (move ["mem_x"])) THEN ((use_arg_then2 ("l2", [])) (term_tac exists_tac)) THEN (done_tac));
];;

(* Lemma list_of_darts_k *)
let list_of_darts_k = Sections.section_proof ["L";"k"]
`good_list L
	==> darts_k k (hypermap_of_list L) 
		= set_of_list (flatten (filter (\f. sizel f = k) (list_of_faces L)))`
[
   ((BETA_TAC THEN (move ["goodL"])) THEN (((use_arg_then2 ("darts_k_union_face_set_k", [darts_k_union_face_set_k]))(thm_tac (new_rewrite [] [])))));
   (((((use_arg_then2 ("list_of_faces_k", [list_of_faces_k]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("set_of_list_flatten_map", [set_of_list_flatten_map]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Lemma darts3_eq_list_of_darts3 *)
let darts3_eq_list_of_darts3 = Sections.section_proof ["L"]
`good_list L
	==> darts_k 3 (hypermap_of_list L) = set_of_list (list_of_darts3 L)`
[
   (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("list_of_darts_k", [list_of_darts_k])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`3`))) (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 ((((use_arg_then2 ("list_of_darts3", [list_of_darts3]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces3", [list_of_faces3]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Seq.size", [Seq.size]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma darts4_eq_list_of_darts4 *)
let darts4_eq_list_of_darts4 = Sections.section_proof ["L"]
`good_list L
	==> darts_k 4 (hypermap_of_list L) = set_of_list (list_of_darts4 L)`
[
   (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("list_of_darts_k", [list_of_darts_k])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`4`))) (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 ((((use_arg_then2 ("list_of_darts4", [list_of_darts4]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces4", [list_of_faces4]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Seq.size", [Seq.size]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma darts5_eq_list_of_darts5 *)
let darts5_eq_list_of_darts5 = Sections.section_proof ["L"]
`good_list L
	==> darts_k 5 (hypermap_of_list L) = set_of_list (list_of_darts5 L)`
[
   (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("list_of_darts_k", [list_of_darts_k])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`5`))) (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 ((((use_arg_then2 ("list_of_darts5", [list_of_darts5]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces5", [list_of_faces5]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Seq.size", [Seq.size]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma darts6_eq_list_of_darts6 *)
let darts6_eq_list_of_darts6 = Sections.section_proof ["L"]
`good_list L
	==> darts_k 6 (hypermap_of_list L) = set_of_list (list_of_darts6 L)`
[
   (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("list_of_darts_k", [list_of_darts_k])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`6`))) (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 ((((use_arg_then2 ("list_of_darts6", [list_of_darts6]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces6", [list_of_faces6]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Seq.size", [Seq.size]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma rot_list_pairs *)
let rot_list_pairs = Sections.section_proof ["s";"n"]
`rot n (list_pairs s) = list_pairs (rot n s)`
[
   (((((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rot_zip", [rot_zip]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("rot_rot", [rot_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_pairs", [list_pairs]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Lemma rotr_list_pairs *)
let rotr_list_pairs = Sections.section_proof ["s";"n"]
`rotr n (list_pairs s) = list_pairs (rotr n s)`
[
   (((((use_arg_then2 ("rotr", [rotr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rot_list_pairs", [rot_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rotr", [rotr]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Lemma list_pairs_rot *)
let list_pairs_rot = Sections.section_proof ["s";"n"]
`perm_eq (list_pairs (rot n s)) (list_pairs s)`
[
   (((((use_arg_then2 ("rot_list_pairs", [rot_list_pairs]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("perm_eq_rot", [perm_eq_rot]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma find_pair_list_empty *)
let find_pair_list_empty = Sections.section_proof ["L";"d"]
`find_pair_list L d = [] <=> ~(MEM d (list_of_darts L))`
[
   (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("find_pair_list", [find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("list_of_darts_nil", [list_of_darts_nil]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))));
   ((((use_arg_then2 ("list_of_darts_cons", [list_of_darts_cons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negb_or", [negb_or]))(thm_tac (new_rewrite [] [])))));
   ((THENL_LAST) (((fun arg_tac -> arg_tac (Arg_term (`MEM d _`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) ((((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
   ((((use_arg_then2 ("implybF", [implybF]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (move ["h_eq"]));
   ((((use_arg_then2 ("mem_d", [])) (disch_tac [])) THEN (clear_assumption "mem_d") THEN BETA_TAC) THEN ((((use_arg_then2 ("h_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("zip", [zip]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma list_of_darts_perm *)
let list_of_darts_perm = Sections.section_proof ["L1";"L2"]
`perm_eq L1 L2 ==> perm_eq (list_of_darts L1) (list_of_darts L2)`
[
   ((BETA_TAC THEN (move ["perm"])) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))))));
   (((((use_arg_then2 ("perm_eq_flatten", [perm_eq_flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("perm_eq_map", [perm_eq_map]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma good_list_perm *)
let good_list_perm = Sections.section_proof ["L1";"L2"]
`perm_eq L1 L2 /\ good_list L1 ==> good_list L2`
[
   ((repeat_tactic 1 9 (((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["perm"])) THEN (case THEN (move ["uniq1"])) THEN (case THEN (move ["all1"])) THEN (move ["sym1"]));
   ((fun arg_tac -> (use_arg_then2 ("list_of_darts_perm", [list_of_darts_perm])) (fun fst_arg -> (use_arg_then2 ("perm", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["perm_darts"])));
   ((((fun arg_tac -> (use_arg_then2 ("perm_eq_uniq", [perm_eq_uniq])) (fun fst_arg -> (use_arg_then2 ("perm_darts", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("uniq1", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("all_perm_eq", [all_perm_eq])) (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 ("all1", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))));
   ((BETA_TAC THEN (move ["d"])) THEN ((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("perm_eq_mem", [perm_eq_mem])) (fun fst_arg -> (use_arg_then2 ("perm_darts", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("sym1", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (done_tac));
];;

(* Lemma find_face_cons *)
let find_face_cons = Sections.section_proof ["h";"t";"d"]
`find_face (h :: t) d = if MEM d (list_pairs h) then (list_pairs h) else find_face t d`
[
   (((repeat_tactic 1 9 (((use_arg_then2 ("find_face", [find_face]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("MAP", [MAP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_list", [find_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma find_face_eq *)
let find_face_eq = Sections.section_proof ["L";"d";"f"]
`uniq (list_of_darts L) /\ MEM d (list_of_darts L)
	==> (find_face L d = f <=> MEM f (list_of_faces L) /\ MEM d f)`
[
   ((BETA_TAC THEN (case THEN ((move ["uniqL"]) THEN (move ["mem_d"])))) THEN ((THENL) (split_tac) [(((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))); ALL_TAC]));
   (((((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_find_face", [mem_find_face]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (((((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mapP", [mapP]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["s"])) THEN (case THEN (move ["mem_s"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("find_pair_list_unique", [find_pair_list_unique])) (fun fst_arg -> (use_arg_then2 ("uniqL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (move ["eq"]));
   (((((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;

(* Close the module *)
end;;