anchor.diff:      //tcs is the list of type constructors, datas is the list of data constructors
   
       //this is the folding function for tcs
  -    //list<term> is the list of haseq axioms we are accumulating
  +    //list<lident * term> is the list of lidents and formulas of haseq axioms we are accumulating
       //env is the environment in which the next two terms are well-formed
       //term is the lhs of the implication for soundness
       //term is the soundness condition derived from all the data constructors of this type
  -    let haseq_ty (acc:(list<term> * env * term * term)) (ty:sigelt) :list<term> * env * term * term =
  +    let haseq_ty (acc:(list<lident * term> * env * term * term)) (ty:sigelt) :list<lident * term> * env * term * term =
           let lid, bs, t, d_lids =
               match ty with
                   | Sig_inductive_typ (lid, _, bs, t, _, d_lids, _, _) -> lid, bs, t, d_lids
  
positive.code:         let env, cond = List.fold_left haseq_data (env, U.t_true) t_datas in
  
          //return new accumulator
          l_axioms @ [fml], env, U.mk_conj guard' guard, U.mk_conj cond' cond
      in
  
      //prep env0
  
      let _ =
          if env.curmodule.ident.idText = "Test" then
              let env = Env.push_sigelt env0 sig_bndle in
              env.solver.push "haseq";
              env.solver.encode_sig env sig_bndle;
              let env = Env.push_univ_vars env us in
  
              let axioms, env, guard, cond = List.fold_left haseq_ty ([], env, U.t_true, U.t_true) tcs in
              
              //later make an implication of guard ==> cond, and tc that
              //let guard, _ = tc_trivial_guard env guard in
              //let cond, _ = tc_trivial_guard env cond in
  
              let phi = U.mk_imp guard cond in
  
              let phi, _ = tc_trivial_guard env phi in
  
              Util.print_string "Checking haseq soundness\n\n";
              Rel.force_trivial_guard env (Rel.guard_of_guard_formula (NonTrivial phi));
  
              //Util.print1 "Guard: %s\n\n" (PP.term_to_string guard);
              //Util.print1 "Cond: %s\n\n" (PP.term_to_string cond);
  
              env.solver.pop "haseq"
          else ()
      in
  
      sig_bndle
  
  let rec tc_decl env se = match se with
      | Sig_inductive_typ _
  
negative.code:       se, env
  
      | Sig_assume(lid, phi, quals, r) ->
        let se = tc_assume env lid phi quals r in
        let env = Env.push_sigelt env se in
        se, env
  
  