anchor.diff:    let recheck_debug s env t =
       Util.print2 "Term has been %s-transformed to:\n%s\n----------\n" s (Print.term_to_string t);
       let t, _, _ = tc_term env t in
  -    Util.print1 "Re-checked; got:\n%s\n----------\n" (Print.term_to_string t)
  +    Util.print1 "Re-checked; got:\n%s\n----------\n" (Print.term_to_string t);
  +    N.normalize [ N.Beta; N.Inline; N.UnfoldUntil S.Delta_constant; N.EraseUniverses ] env t
     in
   
     // TODO: check that [_comp] is [Tot Type]
  
positive.code:     if not (Util.is_total_lcomp item_comp) then
        raise (Err ("Computation for [item] is not total!"));
      let dmff_env, (item_wp, item_elab) = DMFF.star_expr_definition dmff_env item in
      recheck_debug "*" env item_wp;
      recheck_debug "_" env item_elab;
      dmff_env, item_wp, item_elab
    in
  
  
negative.code: 
    let dmff_env = DMFF.empty env (tc_constant Range.dummyRange) in
    let dmff_env, wp_type = DMFF.star_type_definition dmff_env repr in
    let wp_type = recheck_debug "*" env wp_type in
  
    // Building: [a -> wp a -> Effect]
    let effect_signature =
  