anchor.diff:          | _ -> true) in
         g'@inversions, env
   
  -    | Sig_let((is_rec, [(Inr flid, t1, e)]), _, _) when not is_rec -> 
  +    | Sig_let((is_rec, [(Inr flid, t1, e)]), _, _) -> 
           if Util.is_lemma t1 then encode_lemma env flid t1, env else
           let t1_norm = whnf env t1 |> Util.compress_typ in
           let (f, ftok), decls, env = declare_top_level_let env flid t1 t1_norm in
  
positive.code:     | Some s -> s
  let push_free_var env (x:lident) fname ftok = 
      {env with bindings=Binding_fvar(x, fname, ftok)::env.bindings}
  let lookup_free_var env a = lookup_lid env a.v |> snd
  let lookup_free_var_name env a = lookup_lid env a.v |> fst
  let lookup_free_var_sym env a = 
      let name, sym = lookup_lid env a.v in
  
negative.code:     let new_var pp rn = mk_unique <| pp.idText ^ "__" ^ rn.idText in
      let new_fvar lid = mk_unique lid.str in
      let next_id () = incr ctr; !ctr in
      let fresh pfx = format2 "%s_%s" pfx (string_of_int <| next_id()) in
      let string_const s = match Util.find_map !scopes (fun (_, strings) -> Util.smap_try_find strings s) with
          | Some f -> f
          | None -> 
  