anchor.diff:      ///     otherwise.
       /// </returns>
       let checkBaseDownclosure
  -      (empDefn : BoolExpr<Sym<Var>>)
  +      (empDefn : BoolExpr<Sym<Var>> option)
         (iterator : Var)
         (func : IteratedDFunc)
         (defn : BoolExpr<Sym<Var>>)
  
positive.code:             let checkedDefnR =
                  bind
                      (fun i ->
                          checkBaseDownclosure empDefnT i func d
                          >>= uncurry (checkInductiveDownclosure i))
                      checkedIterR
              lift (pairMap id Some) checkedDefnR
  
negative.code:             | Some (Int v) -> ok v
              | Some v -> fail (BadIteratorType ([func], typeOf v))
  
          (* 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
  