anchor.diff:                          defn)
                   succDefnR
   
  -        let indHoldsR = bind runDownclosureCheck checkR
  -
  -        bind
  -            (fun indHolds ->
  -                if indHolds
  -                then ok deferred
  -                else
  -                    bind
  -                        (fun succDefn ->
  -                            fail (InductiveDownclosureError ([func], succDefn, defn)))
  -                        succDefnR)
  +        let indHoldsR = lift runDownclosureCheck checkR
  +
  +        bind2
  +            (fun succDefn indHolds ->
  +                match indHolds with
  +                | Proven -> ok deferred
  +                | Refuted -> fail (InductiveDownclosureError ([func], succDefn, defn))
  +                | Inconclusive reason ->
  +                    ok (NeedsInductiveDownclosure (func, reason)::deferred))
  +            succDefnR
               indHoldsR
   
       /// <summary>
  
positive.code:                The definition of emp can only mention global variables, so it
                 need not need to be freshened. *)
              let checkR = lift (mkImplies ed) baseDefnR
              let baseHoldsR = bind runDownclosureCheck checkR
              bind
                  (fun baseHolds ->
                      if baseHolds
                      then ok deferred
                      else fail (BaseDownclosureError ([func], defn, ed)))
                  baseHoldsR
  
      /// <summary>
  
negative.code:         | MissingIterator view ->
              fmt "constraint '{0}' should have an iterator, but does not"
                  [ printDView view ]
          | Traversal err -> printTraversalError printError err
          |> error
  