anchor.diff:           |> THEN <| ASM_REWRITE_TAC [EX; ALL; DE_MORGAN_THM])
   
   let ALL_MAP = 
  +#if BUGGY
       prove
           ((parse_term @"!P f l. ALL P (MAP f l) <=> ALL (P << f) l"), 
            GEN_TAC
            |> THEN <| GEN_TAC
            |> THEN <| LIST_INDUCT_TAC
            |> THEN <| ASM_REWRITE_TAC [ALL; MAP; o_THM])
  +#else
  +    Sequent([],parse_term @"!P f l. ALL P (MAP f l) <=> ALL (P << f) l")
  +#endif
   
   let ALL_T = 
       prove((parse_term @"!l. ALL (\x. T) l"), LIST_INDUCT_TAC
  
positive.code:          |> THEN <| ASM_REWRITE_TAC [LENGTH; REPLICATE])
  
  let EX_MAP = 
      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])
  
  let EXISTS_EX = 
      prove
  
negative.code:          |> THEN <| ASM_REWRITE_TAC [MAP; FILTER; o_THM]
           |> THEN <| COND_CASES_TAC
           |> THEN <| REWRITE_TAC [MAP])
  #else
      Sequent([],parse_term @"!P f l. FILTER P (MAP f l) = MAP f (FILTER (P << f) l)")
  #endif
  
  let MEM_FILTER = 
      prove
  