anchor.diff:      //strict positivity check
       (if Options.no_positivity () || Options.lax ()  then ()  //skipping positivity check if lax mode
        else
  -       let env = push_sigelt env0 sig_bndle in
  +       let env = push_sigelt env sig_bndle in
          let b = List.iter (fun ty ->
            let b = TcInductive.check_positivity ty env in
            if not b then
  
positive.code: 
      let ses', ses_elaborated = tc_decl env se in
      let ses' = ses' |> List.map (N.elim_uvars env) in
      let env = ses' |> List.fold_left (fun env se -> add_sigelt_to_env env se) env in
      FStar.Syntax.Unionfind.reset();
  
      if (Options.log_types()) || Env.debug env <| Options.Other "LogTypes"
      then BU.print1 "Checked: %s\n" (List.fold_left (fun s se -> s ^ Print.sigelt_to_string se ^ "\n") "" ses');
  
      List.iter (fun se -> env.solver.encode_sig env se) ses';
  
  
negative.code:         failwith (BU.format1 "Unexpected lex_t: %s\n" (Print.sigelt_to_string (mk_sigelt (Sig_bundle(ses, lids)))))
      end
  
  let tc_assume (env:env) (lid:lident) (phi:formula) (quals:list<qualifier>) (r:Range.range) :sigelt =
      let env = Env.set_range env r in
      let k, _ = U.type_u() in
      let phi = tc_check_trivial_guard env phi k |> N.normalize [N.Beta; N.Eager_unfolding] env in
  