(* 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 *)