anchor.diff:      let data_ops_ses = List.map (TcInductive.mk_data_operations quals env tcs) datas |> List.flatten in
   
       //strict positivity check
  -    (if Options.no_positivity () || Options.lax ()  then ()  //skipping positivity check if lax mode
  +    (if Options.no_positivity () || (not (Env.should_verify env))  then ()  //skipping positivity check if lax mode
        else
          let env = push_sigelt env sig_bndle in
          let b = List.iter (fun ty ->
  
positive.code:             else e_lax
            | _ -> e_lax  //leave recursive lets as is
          in
          tc_maybe_toplevel_term ({ env0 with lax = true }) e |> (fun (e, _, _) -> e) |> N.remove_uvar_solutions env0 |> drop_lbtyp
        else e
      in
  
  
negative.code:   | Sig_new_effect(ne) ->
      let ne =
        if Options.use_two_phase_tc () && Env.should_verify env then
          let ne = tc_eff_decl ({ env with lax = true }) ne |> (fun ne -> { se with sigel = Sig_new_effect ne }) |> N.elim_uvars env |> U.eff_decl_of_new_effect in
          if Env.debug env <| Options.Other "TwoPhases" then BU.print1 "Effect decl after phase 1: %s\n" (Print.sigelt_to_string { se with sigel = Sig_new_effect ne });
          ne
        else ne
      in
      let ne = tc_eff_decl env ne in
  