anchor.diff:  
               | _ -> None
               end
  +        | _ -> None
  +    in
  +    let is_forall_const (phi : term) : option<term> =
  +        match U.destruct_typ_as_formula phi with
  +        | Some (QAll ([(bv, _)], pats, phi')) ->
  +            is_quantified_const bv phi'
           | _ -> None
       in
       let is_const_match (phi : term) : option<bool> =
  
positive.code:         | _ -> false
      in
      let simplify arg = (simp_t (fst arg), arg) in
      match is_quantified_const tm with
      (* We need to recurse, and maybe reduce further! *)
      | Some tm -> maybe_simplify_aux cfg env stack (norm cfg env [] tm)
      (* Otherwise try to simplify this point *)
  
negative.code:                 | None ->
                      begin match is_applied_maybe_squashed bs phi with
                      // Case 3)
                      | Some bv' when S.bv_eq bv bv' ->
                          let ftrue = U.abs bs U.t_true (Some (U.residual_tot U.ktype0)) in
                          Some (SS.subst [NT (bv, ftrue)] q)
                      | _ ->
                          None
                      end
                  | Some (BaseConn (lid, [(p, _)])) when Ident.lid_equals lid PC.not_lid ->
                      begin match is_applied_maybe_squashed bs p with
                      // Case 4)
                      | Some bv' when S.bv_eq bv bv' ->
                          let ffalse = U.abs bs U.t_false (Some (U.residual_tot U.ktype0)) in
                          Some (SS.subst [NT (bv, ffalse)] q)
                      | _ ->
  