anchor.diff:           |> THEN <| ASM_REWRITE_TAC [LENGTH; REPLICATE])
   
   let EX_MAP = 
  +#if BUGGY
       prove
           ((parse_term @"!P f l. EX P (MAP f l) <=> EX (P << f) l"), 
            GEN_TAC
            |> THEN <| GEN_TAC
            |> THEN <| LIST_INDUCT_TAC
            |> THEN <| ASM_REWRITE_TAC [MAP; EX; o_THM])
  +#else
  +    Sequent([],parse_term @"!P f l. EX P (MAP f l) <=> EX (P << f) l")
  +#endif
   
   let EXISTS_EX = 
       prove
  
positive.code:          |> THEN <| ASM_REWRITE_TAC [MAP; FILTER; o_THM]
           |> THEN <| COND_CASES_TAC
           |> THEN <| REWRITE_TAC [MAP])
  
  let MEM_FILTER = 
      prove
  
negative.code:          |> THEN <| ASM_REWRITE_TAC [APPEND])
  
  let FILTER_MAP = 
  #if BUGGY
      prove
          ((parse_term @"!P f l. FILTER P (MAP f l) = MAP f (FILTER (P << f) l)"), 
           GEN_TAC
  