anchor.diff:  
       (* and strengthen its VC with and well-formedness condition on its annotated type *)
       //NS: Maybe redundant strengthen
  -    // let c1, guard_f = c1, wf_annot in 
  -    let c1, guard_f = TcUtil.strengthen_precondition
  -                        (Some (fun () -> return_all Err.ill_kinded_type))
  -                        (Env.set_range env1 e1.pos) e1 c1 wf_annot in
  +    let c1, guard_f = c1, wf_annot in 
  +    // let c1, guard_f = TcUtil.strengthen_precondition
  +    //                     (Some (fun () -> return_all Err.ill_kinded_type))
  +    //                     (Env.set_range env1 e1.pos) e1 c1 wf_annot in
       let g1 = Env.conj_guard g1 guard_f in
   
       if Env.debug env Options.Extreme
  
positive.code:           let e = mk_Tm_app head args None r  in
            let c = if ghost then S.mk_GTotal res_t |> TcComm.lcomp_of_comp else TcComm.lcomp_of_comp c in
            //NS: maybe redundant strengthen
            // let c, g = c, guard in
            let c, g = TcUtil.strengthen_precondition None env e c guard in
            e, c, g
  
          | _ -> //fallback
  
negative.code: 
        (* Each conjunct in g is already labeled *)
        //NS: Maybe redundant strengthen      
        let comp, g = comp, guard in
        // let comp, g = TcUtil.strengthen_precondition None env app comp guard in
        if Env.debug env Options.Extreme then BU.print2 "(d) Monadic app: type of app\n\t(%s)\n\t: %s\n"
          (Print.term_to_string app)
          (TcComm.lcomp_to_string comp);
  