anchor.diff:    in
     check "wp_if_then_else" (Util.abs binders wp_if_then_else None);
   
  -  [], wp_if_then_else
  +  [], normalize wp_if_then_else
   
   let tc_eff_decl env0 (ed:Syntax.eff_decl) is_for_free =
     assert (ed.univs = []); //no explicit universe variables in the source; Q: But what about re-type-checking a program?
  
positive.code:    * definitions, both [binders] and [a] are opened. This means that macros
     * close over [binders] and [a], and this means that combinators do not expect
     * [binders] and [a] when applied. *)
  
    (* Consider the predicate transformer st_wp:
     *   let st_pre_h  (heap:Type)          = heap -> GTot Type0
  
negative.code:   (* A debug / sanity check. *)
    let check str t =
      Util.print2 "Generated term for %s: %s\n" str (Print.term_to_string t);
      let t = normalize t in
      let t = SS.compress t in
      let e, { res_typ = res_typ }, _ = tc_term env t in
      Util.print2 "Inferred type for %s: %s\n" str (Print.term_to_string (normalize res_typ));
      Util.print2 "Elaborated term for %s: %s\n" str (Print.term_to_string (normalize e))
    in
  
    (* val st2_pure : #heap:Type -> #a:Type -> #t:Type -> x:t ->
  