anchor.diff:                   ViewDefiner<SVBoolExpr option>>, Error> =
       model
       |> mapAxioms (mapTerm id (reifyView model.ViewProtos model.ViewDefs) id)
  -    |> tryMapViewDefs Downclosure.check
  +    |> tryMapViewDefs (Downclosure.check model.ViewProtos)
   
   
   /// <summary>
  
positive.code:         | MixedFuncType view ->
              fmt "constraint '{0}' mixes iterated and non-iterated views"
                  [ printDView view ]
  
negative.code: ///     </para>
  /// </summary>
  module Downclosure =
      /// Adapts Instantiate.lookup to the downclosure checker's needs.
      let lookupFunc (protos : FuncDefiner<ProtoInfo>) (func : Func<_>)
        : Result<ProtoInfo, Error> =
          // TODO(CaptainHayashi): proper doc comment
          // TODO(CaptainHayashi): merge with Modeller.lookupFunc?
          protos
          |> Core.Instantiate.lookup func
          |> mapMessages (curry LookupError func.Name)
          |> bind (function
                   | Some (_, info) -> info |> ok
                   | None -> func.Name |> NoSuchView |> fail)
  
      /// TODO
      let checkDownclosure (func : IteratedDFunc) (defn : BoolExpr<Sym<Var>> option)
          : Result<DView * BoolExpr<Sym<Var>> option, Error> =
          // TODO(CaptainHayashi): implement this.
          ok ([func], defn)
  
      /// <summary>
      ///     Performs iterated view well-formedness checking on the left of a
      ///     view definition.
      /// </summary>
      /// <param name="def">The definition being checked.</param>
      /// <returns>
      ///     The view definition if all checks passed; errors otherwise.
      /// </returns>
      let checkDef
        (vprotos : FuncDefiner<ProtoInfo>)
        (def : DView * BoolExpr<Sym<Var>> option)
        : Result<DView * BoolExpr<Sym<Var>> option, Error> =
          let (lhs, rhs) = def
  
          trial {
              (* First, we check the prototypes of the views in the lhs to see which
                 are iterated. *)
  
              let iterprotos, normprotos =
                  List.partition (fun func -> func.Iterator <> None) lhs
  
              match (iterprotos, normprotos) with
              (* Correct non-iterated view definition.
                 No more checking necessary. *)
              | [], _ -> return def
              (* Correct iterated view definition, as long as i is actually an
                 iterated func.
                 Need to check inductive and base downclosure. *)
              | [i], [] ->
                  let! iInfo = lookupFunc vprotos i.Func
                  if iInfo.IsIterated
                  then return! (checkDownclosure i rhs)
                  else return! fail (IteratorOnNonIterated i)
  
              // Over-large iterated view definition (for now, anyway).
              | xs, [] -> return! fail (TooManyIteratedFuncs (lhs, List.length xs))
              // Mixed view definition (currently not allowed).
              | _, _ -> return! fail (MixedFuncType lhs)
          }
  
      /// <summary>
      ///     Performs all downclosure and well-formedness checking on iterated
      ///     constraints.
      /// </summary>
      /// <param name="definer">
      ///     The definer whose constraints are being checked.
      /// </param>
      /// <returns>
      ///     The definer if all checks passed; errors otherwise.
      /// </returns>
      let check
        (vprotos : FuncDefiner<ProtoInfo>)
        (definer : ViewDefiner<BoolExpr<Sym<Var>> option>)
          : Result<ViewDefiner<BoolExpr<Sym<Var>> option>, Error> =
  
          (* Currently, we don't actually modify the definer, but this may
             change in future. *)
  
          let checkEach def definer =
              ok def >>= checkDef vprotos >>= (fun _ -> ok definer)
  
          definer |> ViewDefiner.toSeq |> seqBind checkEach definer
  
  /// Splits an iterated GFunc into a pair of guard and iterated func.
  let iterGFuncTuple
  