(* Fan summary file created by thales Dec 7, 2009 *)

(* mark unfinished material *)

let NOT_FOUND  = 
  let NOT_IN_SYSTEM = define `NOT_IN_SYSTEM = F` in
  let FALSE_ALL = prove(`NOT_IN_SYSTEM ==> x`,MESON_TAC[NOT_IN_SYSTEM]) in
  fun x -> INST [(x,`x:bool`)] FALSE_ALL ;;


(* FAN DEFINED *)


let CTVTAQA_t = `! V E E'. FANO(V,E) /\ (E' SUBSET E) ==> FANO(V,E')`;;
let CTVTAQA = NOT_FOUND CTVTAQA_t ;;

XOHLED;;

(* remarks follow in text, formal proof? *)

AAUHTVE;; (* contains the essential content of the lemma *)

ULEKUUB;;  (* from chapter on trig. phrased in terms of hypermaps.  The lemma isn't exactly proved. *)


VBTIKLP;;


IBZWFFH;;

(* JGIYDLE;; not done *)