anchor.diff:  (* ------------------------------------------------------------------------- *)
   (* Pre-simplification.                                                       *)
   (* ------------------------------------------------------------------------- *)
  +
   /// Applies basic propositional simpli cations and some miniscoping.
   let PRESIMP_CONV = 
  
positive.code:             let th = MK_COMB(AP_TERM op (substrongdnf l), substrongdnf r)
              TRANS th (distribute(Choice.get <| rand(concl <| Choice.get th)))
          | _ -> REFL tm
      and strongdnf tm = 
          let th = substrongdnf tm
          TRANS th (strengthen(Choice.get <| rand(concl <| Choice.get th)))
      weakdnf, strongdnf
  
  (* ------------------------------------------------------------------------- *)
  (* Likewise for CNF.                                                         *)
  (* ------------------------------------------------------------------------- *)
  // WEAK_CNF_CONV: Converts a term already in negation normal form into conjunctive normal form.
  // CNF_CONV: Converts a term already in negation normal form into conjunctive normal form.
  let WEAK_CNF_CONV, CNF_CONV = 
  
negative.code:                     let hop, args = strip_comb tm
                      let len = length args
                      let newheads = 
                          if is_const hop || mem hop lconsts then 
                              (insert (hop, len) cheads, vheads)
                          elif len > 0 then 
                              (cheads, insert (hop, len) vheads)
                          else sofar
                      itlist (get_heads lconsts) args newheads
  
      let get_thm_heads th sofar = get_heads (freesl(hyp <| Choice.get th)) (concl <| Choice.get th) sofar
  
      let APP_CONV = 
          let th = 
              prove((parse_term @"!(f:A->B) x. f x = I f x"), REWRITE_TAC [I_THM])
          REWR_CONV th
  
      let rec APP_N_CONV n tm = 
          if n = 1 then APP_CONV tm
          else (RATOR_CONV(APP_N_CONV(n - 1))
                |> THENC <| APP_CONV) tm
  
      let rec FOL_CONV hddata tm = 
          if is_forall tm then 
              BINDER_CONV (FOL_CONV hddata) tm
          elif is_conj tm || is_disj tm then 
              BINOP_CONV (FOL_CONV hddata) tm
          else 
              let op, args = strip_comb tm
              let th = rev_itlist (C(curry MK_COMB)) (map (FOL_CONV hddata) args) (REFL op)
              let tm' = Choice.get <| rand(concl <| Choice.get th)
              let n = 
                  // OPTIMIZE : Replace the entire 'match' statement below with:
                  //assoc op hddata
                  //|> Option.map (fun x -> length args - x)
                  //|> Option.fill 0
                  match assoc op hddata with
                  | None -> 0
                  | Some x -> length args - x
              if n = 0 then th
              else TRANS th (APP_N_CONV n tm')
  
      let GEN_FOL_CONV(cheads, vheads) = 
          let hddata = 
              if vheads = [] then 
                  let hops = setify(map fst cheads)
                  let getmin h = 
                      let ns = 
                          mapfilter (fun (k, n) -> 
                              if k = h then Some n
                              else None) cheads
                      if length ns < 2 then fail()
                      else h, end_itlist min ns
                  mapfilter (Some << getmin) hops
              else 
                  map (fun t -> 
                      if is_const t && fst(Choice.get <| dest_const t) = "=" then t, 2
                      else t, 0) (setify(map fst (vheads @ cheads)))
          FOL_CONV hddata
  
      fun (asl, w as gl) -> 
              let headsp = itlist (get_thm_heads << snd) asl ([], [])
              RULE_ASSUM_TAC (CONV_RULE(GEN_FOL_CONV headsp)) gl
  