anchor.diff:  (* Instantiate theorem by matching part of it to a term.                     *)
   (* The GEN_PART_MATCH version renames free vars to avoid clashes.            *)
   (* ------------------------------------------------------------------------- *)
  +// PART_MATCH: Instantiates a theorem by matching part of it to a term.
  +// GEN_PART_MATCH: Instantiates a theorem by matching part of it to a term.
   let PART_MATCH, GEN_PART_MATCH = 
       let rec match_bvs t1 t2 acc = 
           try 
  
positive.code: (* ------------------------------------------------------------------------- *)
  (* First order unification (no type instantiation -- yet).                   *)
  (* ------------------------------------------------------------------------- *)
  let (term_unify : term list -> term -> term -> instantiation) = 
      let augment1 sofar (s, x) = 
          let s' = subst sofar s
  
negative.code: (* ------------------------------------------------------------------------- *)
  (* Derived principle of definition justifying |- c x1 .. xn = t[x1,..,xn]    *)
  (* ------------------------------------------------------------------------- *)
  /// Declare a new constant and a definitional axiom.
  let new_definition tm = 
      let avs, bod = strip_forall tm
      let l, r = 
  