anchor.diff:      in
       let rec un (t0:term) (w:bool) norm : option<list<'a>> =
           let t = U.unmeta_safe t0 in
  -        lazy_unembed t t_list_a (fun t ->
  +        lazy_unembed printer t t_list_a (fun t ->
           let hd, args = U.head_and_args t in
           match (U.un_uinst hd).n, args with
           | Tm_fvar fv, _
  
positive.code:             Err.log_issue t0.pos (Err.Warning_NotEmbedded, (BU.format1 "Not an embedded pair: %s" (Print.term_to_string t0)));
              None)
      in
      mk_emb em un (S.t_tuple2_of (type_of ea) (type_of eb))
  
  let e_list (ea:embedding<'a>) =
      let t_list_a =
          let t_list = U.fvar_const PC.list_lid in
          S.mk_Tm_app t_list [S.as_arg ea.typ] None Range.dummyRange
      in
      let rec em (l:list<'a>) (rng:range) shadow_l norm : term =
          lazy_embed rng t_list_a l (fun () ->
          let t = S.iarg (type_of ea) in
          match l with
          | [] ->
  
negative.code:                 | None -> raise Embedding_failure
                  | Some app -> norm (BU.Inr app))
          in
          lazy_embed (fun _ -> "<fun>") rng t_arrow f_wrapped (fun () ->
          match force_shadow shadow_f with
          | None -> raise Embedding_failure //TODO: dodgy
          | Some repr_f -> norm (BU.Inr repr_f))
      in
      let un (f:term) w norm : option<('a -> 'b)> =
          lazy_unembed printer f t_arrow (fun f ->
          let f_wrapped (a:'a) : 'b =
              let a_tm = embed ea a f.pos None norm in
              let b_tm = norm (BU.Inr (S.mk_Tm_app f [S.as_arg a_tm] None f.pos)) in
  