anchor.diff:       *)
   
       /// <summary>
  -    ///   A term, containing a command relation, weakest precondition, and goal.
  +    ///     A term, containing a command relation, weakest precondition, and
  +    ///     goal.
       /// </summary>
       /// <remarks>
  -    ///   Though these are similar to Axioms, we keep them separate for reasons of
  -    ///   semantics: Axioms are literal Hoare triples {P}C{Q}, whereas Terms are
  -    ///   some form of the actual Views axiom soundness check we intend to prove.
  +    ///     Though these are similar to Axioms, we keep them separate for
  +    ///     reasons of semantics: Axioms are literal Hoare triples {P}C{Q},
  +    ///     whereas Terms are some form of the actual Views axiom soundness
  +    ///     check we intend to prove.
       /// </remarks>
       type Term<'cmd, 'wpre, 'goal> =
           { /// The command relation of the Term.
  
positive.code: 
  /// Creates a new model that is the input model with a different axiom set.
  /// The axiom set may be of a different type.
  let withAxioms (xs : Map<string, 'y>) (model : Model<'x, 'dview>) : Model<'y, 'dview> = 
      { Globals = model.Globals
        Locals = model.Locals
        ViewDefs = model.ViewDefs
  
negative.code: ///     Type-constrained version of <c>func</c> for <c>VFunc</c>s.
  /// </summary>
  /// <parameter name="name">
  ///     The name of the <c>VFunc</c>.
  /// </parameter>
  /// <parameter name="pars">
  ///     The parameters of the <c>VFunc</c>, as a sequence.
  /// </parameter>
  /// <returns>
  ///     A new <c>VFunc</c> with the given name and parameters.
  /// </returns>
  let vfunc name (pars : Expr seq) : VFunc = func name pars
  
  /// Rewrites a Term by transforming its Cmd with fC, its WPre with fW,
  /// and its Goal with fG.
  let mapTerm fC fW fG {Cmd = c; WPre = w; Goal = g} =
  