anchor.diff:          | InductiveDownclosureError of view : DView * def : BoolExpr<Sym<Var>>
           /// <summary>
           ///     An iterated view definition failed the base downclosure
  -        ///     property.
  +        ///     property with regards to the given definition of 'emp'.
           ///
           ///     <para>
           ///         This is the property that a view definition, when
  
positive.code:     open Starling.Core.Pretty
      open Starling.Core.Expr.Pretty
      open Starling.Core.Symbolic.Pretty
      open Starling.Core.Var.Pretty
      open Starling.Core.View.Pretty
  
  
negative.code: ///     </para>
  /// </summary>
  module Downclosure =
      open Starling.Core.ExprEquiv
      open Starling.Core.Sub
  
      /// Adapts Instantiate.lookup to the downclosure checker's needs.
      let lookupFunc (protos : FuncDefiner<ProtoInfo>) (func : Func<_>)
        : Result<ProtoInfo option, Error> =
          // TODO(CaptainHayashi): proper doc comment
          // TODO(CaptainHayashi): merge with Modeller.lookupFunc?
          protos
          |> Core.Instantiate.lookup func
          |> mapMessages (curry LookupError func.Name)
          |> lift (Option.map snd)
  
      let downclosureMap (f : Var -> IntExpr<Sym<Var>>)
        : BoolExpr<Sym<Var>> -> BoolExpr<Sym<Var>> =
          let m = Mapper.make f (Reg >> BVar) |> liftVToSym |> onVars
          Mapper.mapBoolCtx m NoCtx >> snd
  
      let checkBaseDownclosure
        (empDefn : BoolExpr<Sym<Var>>)
        (iterator : Var)
        (func : IteratedDFunc)
        (defn : BoolExpr<Sym<Var>>)
        : Result<IteratedDFunc * BoolExpr<Sym<Var>>, Error> =
          (* To do the base downclosure, we need to replace all instances of the
             iterator in the definition with 0. *)
          let subZero v = if v = iterator then AInt 0L else AVar (Reg v)
  
          let baseDefn = downclosureMap subZero defn
  
          (* Base downclosure for a view V[n](x):
               D(emp) => D(V[0](x))
             That is, the definition of V when the iterator is 0 can be no
             stricter than the definition of emp.
  
             The definition of emp can only mention global variables, so it does
             not need to be freshened. *)
          let check = mkImplies empDefn baseDefn
  
          // Expression equivalence cannot handle symbols, so try remove them.
          // TODO(CaptainHayashi): is it sound to approximate here?
          bind
              (fun chk ->
                  // Pose that the check is a tautology, and use Z3 to check it.
                  let closed = equivHolds id (equiv chk BTrue)
  
                  if closed
                  then ok (func, defn)
                  else fail (BaseDownclosureError ([func], defn, empDefn)))
              (check
               |> Mapper.mapBoolCtx (tsfRemoveSym SymInIteratedConstraint) NoCtx
               |> snd)
  
      let checkInductiveDownclosure (iterator : Var)
        (func : IteratedDFunc)
        (defn : BoolExpr<Sym<Var>>)
        : Result<IteratedDFunc * BoolExpr<Sym<Var>>, Error> =
          ok (func, defn)
  
      /// <summary>
      ///     Checks the base and inductive downclosure properties on a given
      ///     arity-1 view definition.
      /// </summary>
      /// <param name="func">The view definition's lone defined func.</param>
      /// <param name="empDefn">The definition of 'emp', if one exists.</param>
      /// <param name="defn">The definition of <paramref name="func"/>.</param>
      /// <returns>
      ///     The view definition itself, if it obeys downclosure; an error
      ///     stating which property failed, otherwise.
      /// </returns>
      let checkDownclosure (func : IteratedDFunc)
          (empDefn : BoolExpr<Sym<Var>> option)
          (defn : BoolExpr<Sym<Var>> option)
          : Result<IteratedDFunc * BoolExpr<Sym<Var>> option, Error> =
          let checkIterator =
              function
              | None -> fail (MissingIterator [func])
              | Some (Int v) -> ok v
              | Some v -> fail (BadIteratorType ([func], typeOf v))
  
          (* No point checking base downclosure if 'emp' is undefined.
             This is because the downclosure property would become
               D(V[0](x)) => true
             which is trivially true. *)
          let checkBase i (f, d) =
              match empDefn with
              | Some e -> checkBaseDownclosure e i f d
              | None -> ok (f, d)
  
          (* No point checking downclosure of an indefinite viewdef.
             This job is delegated to the indefinite-proof backends, like HSF and
             MuZ3, which must make sure their synthesised definitions are
             downclosed. *)
          match defn with
          | None -> ok (func, None)
          | Some d ->
              func.Iterator
              |> checkIterator
              |> bind
                  (fun i ->
                      checkBase i (func, d)
                      >>= uncurry (checkInductiveDownclosure i))
              |> lift (fun (f, d) -> f, Some d)
  
      /// <summary>
      ///     Performs iterated view well-formedness checking on the left of a
      ///     view definition.
      /// </summary>
      /// <param name="empDefn">The definition, if any, of 'emp'.</param>
      /// <param name="vprotos">The view prototypes in use.</param>
      /// <param name="def">The definition being checked.</param>
      /// <returns>
      ///     The view definition if all checks passed; errors otherwise.
      /// </returns>
      let checkDef
        (empDefn : BoolExpr<Sym<Var>> option)
        (vprotos : FuncDefiner<ProtoInfo>)
        (def : DView * BoolExpr<Sym<Var>> option)
        : Result<DView * BoolExpr<Sym<Var>> option, Error> =
  