anchor.diff:      List.find (fun e -> fst e = term_sequence) substitution
   
   // hasVar returns true iff the substitution contain a mapping to a logical variable
  -let hasVar term_sequence theta =
  +let hasVar theta =
       List.exists (function
           | _, Var _ -> true
  -        | _, Const _
  -        | _, Function (_, _)
  -        | _, Val _ -> false) theta
  +        | _        -> false) theta
   
   // base_name turns a prefix and a number into a Var
   let var base_name n =
       Var (sprintf "%s%d" base_name n)
   
  -// allSame returns true if all elements in the sequence are equal to the first one.
  -let allEqual l =
  -    let first = head l
  -    andMap (fun each -> each = first) l
  +// allEqual returns true if all elements in the sequence are equal.
  +let allEqual = function
  +    | One _ -> true
  +    | Many (x, xs) -> forall ((=) x) xs
  +
  +let functionUnifiable name1 arity = function
  +    | Function (name2, args2) -> name2 = name1 && args2.Length = arity
  +    | _                       -> false
   
   // unifiable returns true if and only if all elements in the sequence are Functions with
   // the same name and the same arity.
  -let possiblyUnifiable examples =
  -    match examples with
  -    | Many (Function (f, args), _) as examples ->
  -        (andMap (function
  -                 | Function (this_name, these_args) -> f = this_name && args.Length = these_args.Length
  -                 | _ -> false) examples)
  -    | Many (Const _, _)
  -    | Many (Val _, _)
  -    | Many (Var _, _)
  -    | One _ -> false
  +let allFunctionUnifiable = function
  +    | Many (Function (f, args), tail) -> forall (functionUnifiable f args.Length) tail
  +    | _ -> false
   
   // antiUnifyTheta is a helper for antiUnify, returning the anti-unification of a term sequence with
   // respect to a substitution map (mapping term sequences to logical variables)
  
positive.code: // TODO: At the moment, we use logical variables of the form Var "#z0", Var "#z1", Var "#z2", ... This
  // will cause problems is a user happens to also use names in this namespace.
  let rec antiUnifyTheta (theta: (TermSequence<Term<'a>> * Term<'a>) list) n = function
      | One x -> (x, theta, n) // rule 7: all examples (one of them) the same? return that example
      | Many (t, _) as examples when allEqual examples -> (t, theta, n) // rule 7: all examples the same? return the first
      | Many ((Function (f, args)), _) as examples when possiblyUnifiable examples -> // rule 8: recurse into the Function arguments.
          let s, theta', n = antiUnifyTheta theta n (heads examples)
          let tails_au, theta'', n = antiUnifyTheta theta' n (tails examples)
          let au_of_args = match tails_au with // How can we be sure we only ever have Functions and Vars here?
                           | Function (g, ss) -> Function (f, s::ss)
                           | Var name -> Function (f, (s::[Var name]))
                           | unrecognised -> failwith (sprintf "unrecognised term %A while walking function argument tails" unrecognised)
          au_of_args, theta'', n
      | Many _ as ts when hasMap ts theta -> // rule 9: return the previously mapped logical variable
          let term_sequence, mapped_var = findMap ts theta
          mapped_var, theta, n
      | Many _ as ts -> // rule 10: introduce a fresh logical variable
          let z = var "#z" n // This hardcoded base name lets us avoid passing in a name generator. A post-process step could always replace these. But what if someone wants to use "#z" prefixed names....!
          z, ((ts, z) :: theta), n + 1
      | unrecognised -> failwith (sprintf "There is no rule 11: %A" unrecognised) // Necessary because all the previous matches have when clauses, so we can't rely on F#'s exhaustiveness checking
  
  // preprocess turns all Vars into ground terms by pretending they're constant terms
  let rec preprocess = function
  
negative.code:     | Many (x, xs) -> Many (f x, map f xs)
  
  // andMap returns true iff a predicate is true for every element in a non-empty list
  let forall f xs =
      fold (&&) true (map f xs)
  
  // Given a TermSequence of Functions, heads returns a TermSequence containing the heads of the argument lists
  let heads xs =
      map (function
          | Function (name, t::ts) -> t //Function (name, [t])
          | unrecognised -> failwith (sprintf "heads can only process a Function, not %A" unrecognised)) xs
  
  // tails returns a list of Functions whose lists are the tails of the original Functions when given a term sequence (of Functions)
  let tails xs =
      map (function
          | Function (name, t::ts) -> Function (name, ts)
          | unrecognised -> failwith (sprintf "tails can only process a Function, not %A" unrecognised)) xs
  
  // hasMap returns true iff the substitution maps a term sequence
  