anchor.diff:                   ("flatten", Request.Flatten)
                    ("semantics", Request.Semantics)
                    ("termOptimise", Request.TermOptimise)
  -                 ("proof", Request.Proof)
  +                 ("symproof", Request.SymProof)
                    ("reifyZ3", Request.Z3 Backends.Z3.Types.Request.Translate)
                    ("z3", Request.Z3 Backends.Z3.Types.Request.Combine)
                    ("sat", Request.Z3 Backends.Z3.Types.Request.Sat)
  
positive.code: let printResult pOk pBad =
      either (printOk pOk pBad) (printErr pBad)
  
  /// Shorthand for the proof-output stage.
  let proof = bind (Core.Instantiate.Phase.run >> mapMessages Error.ModelFilterError)
  
  /// Shorthand for the HSF stage.
  let hsf = bind (Backends.Horn.hsfModel >> mapMessages Error.HSF)
  
negative.code:     /// The result of term optimisation.
      | TermOptimise of UFModel<STerm<SMGView, SMVFunc>>
      /// Output a fully-instantiated proof.
      | SymProof of Model<SFTerm, unit>
      /// The result of Z3 backend processing.
      | Z3 of Backends.Z3.Types.Response
      /// The result of MuZ3 backend processing.
  