anchor.diff:                  bdBeforeR
           bind mkProc baseDefnR
       | _ ->
  -        fail 
  +        fail
               (CannotCheckDeferred
                   (NeedsBaseDownclosure (func, reason), "emp is indefinite"))
   
  
positive.code:         | _ -> None
  
      /// Print all the Grasshopper queries that haven't been eliminated by Z3.
      let printQuery (model: GrassModel) : Doc = 
          let axseq = Map.toSeq model.Axioms
          let tseq = Seq.map (fun (name,term) -> printGrassTerm name term) axseq
          let pragseq = Seq.choose printPragma model.Pragmata 
          let docseq = Seq.append pragseq tseq
  
          VSep (docseq, VSkip)
  
  
  /// <summary>
  ///     Get the set of accessed variables in a term. 
  /// </summary>
  let findTermVars (term : Backends.Z3.Types.ZTerm)
    : Result<CTyped<MarkedVar> list, Error> =
  
negative.code:                  <+> String why)
          | Traversal err -> printTraversalError printError err
  
      /// Print infix operator (generic)
      let infexprG (combine : string -> Doc -> Doc) (op : string) (pxs : 'x -> Doc) (xs : seq<'x>) : Doc =
          let mapped = Seq.map pxs xs
          let resseq = Seq.map (combine op) (Seq.tail mapped)
          parened (hsep [Seq.head mapped; (hsep resseq)])
  
      /// Print infix operator across multiple lines
      let infexprV (op : string) (pxs : 'x -> Doc) (xs : seq<'x>) : Doc =
          infexprG (fun o x -> vsep [(String o); Indent x]) op pxs xs
  
      /// Print infix operator on one line
      let infexpr (op : string) (pxs : 'x -> Doc) (xs : seq<'x>) : Doc =
          infexprG (fun o x -> hsep [(String o); x]) op pxs xs
  
      /// Prints a marked Var
      let printMarkedVarGrass (v : MarkedVar) : Doc =
          match v with
          | Before s -> String "before_" <-> String s
          | After s -> String "after_" <-> String s
          | Intermediate (i, s) -> String "inter_" <-> String (sprintf "%A_" i) <-> String s
          | Goal (i, s) -> String "goal_" <-> String (sprintf "%A_" i) <-> String s
  
      /// <summary>
      ///     Prints a shadow variable.
  