anchor.diff:        DISCH_THEN(MP_TAC << AP_TERM (parse_term @"EVEN")) |>THEN<|
         REWRITE_TAC[EVEN_MULT; EVEN_ADD; ARITH; EVEN])
       let allsimps = 
  -     itlist (fun x y -> Choice.get <| mk_rewrites false x y) [EQ_ADD_RCANCEL; EQ_ADD_LCANCEL;
  +     Choice.List.fold (fun acc x -> mk_rewrites false x acc) 
  +      [EQ_ADD_RCANCEL; EQ_ADD_LCANCEL;
          EQ_ADD_RCANCEL_0; EQ_ADD_LCANCEL_0;
          LSYM EQ_ADD_RCANCEL_0; LSYM EQ_ADD_LCANCEL_0;
          EQ_MULT_RCANCEL; EQ_MULT_LCANCEL;
  
positive.code:                          |> THEN <| REWRITE_TAC [MEASURE; MEASURE_LE]
                           |> THEN <| REWRITE_TAC [FORALL_PAIR_THM]
                           |> THEN <| GUESS_MEASURE_THEN tac))(asl, w)
        let PRE_GUESS_TAC = 
            CONV_TAC(BINDER_CONV(DEPTH_BINOP_CONV (parse_term @"(/\)") (TRY_CONV SIMPLIFY_WELLDEFINEDNESS_CONV
                                                                        |> THENC <| TRY_CONV FORALL_UNWIND_CONV)))
        let GUESS_ORDERING_TAC = 
            let false_tm = (parse_term @"\x:A y:A. F")
            W(fun (asl, w) -> 
                let ty = fst(Choice.get <| dest_fun_ty(Choice.get <| type_of(fst(Choice.get <| dest_exists w))))
                EXISTS_TAC(Choice.get <| inst [ty, aty] false_tm)
                |> THEN <| REWRITE_TAC [WF_FALSE]
                |> THEN <| NO_TAC)
            |> ORELSE <| GUESS_WF_THEN(REWRITE_TAC [FORALL_PAIR_THM]
                                       |> THEN <| ARITH_TAC)
        fun etm -> 
        let th = pure_prove_recursive_function_exists etm
        try 
            let wtm = Option.get <| find is_exists (hyp <| Choice.get th)
            let wth = prove(wtm, PRE_GUESS_TAC
                                 |> THEN <| GUESS_ORDERING_TAC)
            PROVE_HYP wth th
        with
        | Failure _ -> th
    
    in
  
  
negative.code:     let false_tm = (parse_term @"F") in 
      let and_tm = (parse_term @"(/\)")
      let eq_refl = EQT_INTRO(SPEC_ALL EQ_REFL)
  
      fun tm -> 
          choice {
          let! allsimps = allsimps
          let! net = Choice.List.fold (fun acc x -> net_of_thm false x acc) (!basic_rectype_net) allsimps
  
          let RECTYPE_ARITH_EQ_CONV = TOP_SWEEP_CONV(REWRITES_CONV net)
                                      |> THENC <| GEN_REWRITE_CONV DEPTH_CONV [AND_CLAUSES; OR_CLAUSES]
  
          let SIMPLIFY_CASE_DISTINCTNESS_CLAUSE tm = 
              choice {
              let avs, bod = strip_forall tm
              let! ant, cons = dest_imp bod
              let! ath = RECTYPE_ARITH_EQ_CONV ant
              let! atm = rand(concl ath)
              let bth = 
                  CONJ (Choice.result ath) 
                           (if atm = false_tm then REFL cons
                            else 
                                DISCH atm (PURE_REWRITE_CONV [eq_refl; ASSUME atm] cons))
              let cth = 
                  choice { 
                      return! simp1 bth 
                  } 
                  |> Choice.bindError(function 
                          | Failure _ -> 
                              choice { 
                                  return! simp2 bth 
                              } 
                              |> Choice.bindError(function 
                                      | Failure _ -> simp3 bth
                                      | e -> Choice.error e)
                          | e -> Choice.error e)
              return! itlist MK_FORALL avs cth
              }
  
          return! 
              (DEPTH_BINOP_CONV and_tm SIMPLIFY_CASE_DISTINCTNESS_CLAUSE
               |> THENC <| GEN_REWRITE_CONV DEPTH_CONV [FORALL_SIMP; AND_CLAUSES]) tm
          }
         
         in
  
  (* ------------------------------------------------------------------------- *)
  (* Simplify an existential question about a pattern.                         *)
  