anchor.diff:  /// command semantics, as well as a globals environment.
   let hsfConditionSingle dvs env q body =
       lift (fun qH -> { Head = qH ; Body = body })
  -         (hsfGuarMultiset dvs env aAfter q)
  +         (Option.get (hsfGuarMultiset dvs env aAfter q))
   
   /// Constructs a series of Horn clauses for a term.
   /// Takes the environment of active global variables.
  
positive.code:     let psH =
          ps
          |> Multiset.toSeq
          |> Seq.map (hsfGuarMultiset dvs env aBefore)
          |> collect
          |> lift List.ofSeq
  
  
negative.code:     // defining views is to be held true.
      match (findDefOfView dvs ms) with
          | Some _ ->
              Some (lift2 (fun cR msR -> ite cR msR True)
                      (boolExpr c)
                      (predOfMultiset env (marker >> ok) tryArithExpr ms))
          | None -> None
  
  /// Constructs the body for a set of condition pair Horn clauses,
  /// given the defining views, preconditions and semantics clause.
  