anchor.diff:              decls@karr@[Util.mkAssume(mkForall (Ident.range_of_lid t) ([[tapp]], vars, mkImp(guard, k)), None, ("kinding_"^ttok))] in
           let aux =
               kindingAx
  -            @(inversion_axioms tapp vars)
  +            @(inversion_axioms tapp vars formals)
               @[pretype_axiom (Ident.range_of_lid t) env tapp vars] in
   
           let g = decls
  
positive.code:                     let indices, decls' = encode_args indices env in
                      if List.length indices <> List.length vars
                      then failwith "Impossible";
                      let eqs = List.map2 (fun v a -> mkEq(mkFreeV v, a)) vars indices |> mk_and_l in
                      mkOr(out, mkAnd(mk_data_tester env l xx, eqs)), decls@decls') (mkFalse, []) in
                  let ffsym, ff = fresh_fvar "f" Fuel_sort in
                  let fuel_guarded_inversion =
  
negative.code:                  [Term.DeclFun(name, args |> List.map (fun (_, sort, _) -> sort), Term_sort, None)]
              else constructor_to_decl (Ident.range_of_lid t) c in
  
          let inversion_axioms tapp vars (formals:S.binders) =
              if datas |> BU.for_some (fun l -> Env.try_lookup_lid env.tcenv l |> Option.isNone) //Q: Why would this happen?
              then []
              else
  