anchor.diff:  
        | Sig_inductive_typ(t, universe_names, tps, k, _, datas) ->
            let tcenv = env.tcenv in
  -         let is_injective  =
  +         let is_injective () =
                let usubst, uvs = SS.univ_var_opening universe_names in
                let env, tps, k =
                   Env.push_univ_vars tcenv uvs,
  
positive.code:                  let data_ax, decls = datas |> List.fold_left (fun (out, decls) l ->
                      let _, data_t = Env.lookup_datacon env.tcenv l in
                      let args, res = U.arrow_formals data_t in
                      let indices = match (SS.compress res).n with
                          | Tm_app(_, indices) -> indices
                          | _ -> [] in
                      let env = args |> List.fold_left
                          (fun env (x, _) -> push_term_var env x (mkApp(mk_term_projector_name l x, [xx])))
                          env in
                      let indices, decls' = encode_args indices env in
                      if List.length indices <> List.length vars
                      then failwith "Impossible";
                      let eqs =
                          if is_injective
                          then List.map2 (fun v a -> mkEq(mkFreeV v, a)) vars indices
                          else [] in
                      mkOr(out, mkAnd(mk_data_tester env l xx, eqs |> mk_and_l)), decls@decls') (mkFalse, []) in
                  let ffsym, ff = fresh_fvar "f" Fuel_sort in
                  let fuel_guarded_inversion =
  
negative.code:              in
               List.forall2 tp_ok tps us
          in
          //if Env.debug env.tcenv <| Options.Other "SMTEncoding"
          //then BU.print2 "%s injectivity for %s\n"
          //            (if is_injective then "YES" else "NO")
          //            (Ident.string_of_lid t);
          let quals = se.sigquals in
          let is_logical = quals |> BU.for_some (function Logic | Assumption -> true | _ -> false) in
          let constructor_or_logic_type_decl (c:constructor_t) =
  