anchor.diff:              mkImplies
                   (mkLe (AInt 0L) (AVar (Reg iterator)))
                   (mkImplies succDefn defn)
  -
  -        // 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
  +            (fun indHolds ->
  +                if indHolds
                   then ok (func, defn)
                   else fail (InductiveDownclosureError ([func], succDefn, defn)))
  -            (check
  -             |> Mapper.mapBoolCtx (tsfRemoveSym SymInIteratedConstraint) NoCtx
  -             |> snd)
  +            (runDownclosureCheck check)
   
       /// <summary>
       ///     Checks the base and inductive downclosure properties on a given
  
positive.code: 
          (* This is needed for base downclosure checking.
             If it doesn't exist, then we don't do those checks. *)
          let empDefn =
              definer
              |> ViewDefiner.toSeq
              |> Seq.tryFind (fst >> List.isEmpty)
              |> Option.bind snd
  
          let checkEach def definer =
              ok def >>= checkDef empDefn vprotos >>= (fun _ -> ok definer)
  
          definer |> ViewDefiner.toSeq |> seqBind checkEach definer
  
  /// Splits an iterated GFunc into a pair of guard and iterated func.
  let iterGFuncTuple
  
negative.code:            The definition of emp can only mention global variables, so it does
             not need to be freshened. *)
          let check = mkImplies empDefn baseDefn
          bind
              (fun baseHolds ->
                  if baseHolds
                  then ok (func, defn)
                  else fail (BaseDownclosureError ([func], defn, empDefn)))
              (runDownclosureCheck check)
  
      /// <summary>
      ///     Checks the inductive downclosure property.
      ///     <para>
      ///         This states that, for all iterated views <c>A(x)[n]</c>,
      ///         for all positive <c>n</c>, <c>D(A(x)[n+1]) => D(A(x)[n])</c>:
      ///         iterated view definitions must be monotonic over the iterator.
      ///         This, coupled with base downclosure, allows us to consider only
      ///         the highest iterator of an iterated func during reification,
      ///         instead of needing to take all funcs with an iterator less than
      ///         or equal to it.
      ///     </para>
      /// </summary>
      /// <param name="iterator">The iterator variable, <c>n</c>.</param>
      /// <param name="func">The iterated func to check, <c>A(x)[n]</c>.</param>
      /// <param name="defn">The definition to check, <c>D(A(x)[n])</c>.</param>
      /// <returns>
      ///     The original definition if inductive downclosure holds; an error
      ///     otherwise.
      /// </returns>
      let checkInductiveDownclosure (iterator : Var)
        (func : IteratedDFunc)
        (defn : BoolExpr<Sym<Var>>)
        : Result<IteratedDFunc * BoolExpr<Sym<Var>>, Error> =
          (* To do the inductive downclosure, we need to replace all instances of
             the iterator in the definition with (iterator + 1) in one version. *)
          let increment v = mkAdd2 (AVar (Reg v)) (AInt 1L)
          let succDefn = mapOverIteratorUses increment iterator defn
  
          (* Inductive downclosure for a view V[n](x):
               (0 <= n) => (D(V[n+1](x)) => D(V[n](x)))
             That is, the definition of V when the iterator is n+1 implies the
             definition of V when the iterator is n, for all positive n. *)
  