anchor.diff:      in
       let un (w:bool) (t0:term) : option<('a * 'b)> =
           let t = U.unmeta_safe t0 in
  -        let hd, args = U.head_and_args t in
  +        let hd, args = U.head_and_args' t in
           match (U.un_uinst hd).n, args with
           | Tm_fvar fv, [_; _; (a, _); (b, _)] when S.fv_eq_lid fv PC.lid_Mktuple2 ->
               BU.bind_opt (unembed' w ea a) (fun a ->
  
positive.code:     in
      let rec un (w:bool) (t0:term) : option<list<'a>> =
          let t = U.unmeta_safe t0 in
          let hd, args = U.head_and_args t in
          match (U.un_uinst hd).n, args with
          | Tm_fvar fv, _
              when S.fv_eq_lid fv PC.nil_lid -> Some []
  
negative.code:     in
      let un (w:bool) (t0:term) : option<norm_step> =
          let t = U.unmeta_safe t0 in
          let hd, args = U.head_and_args' t in
          match (U.un_uinst hd).n, args with
          | Tm_fvar fv, [] when S.fv_eq_lid fv PC.steps_simpl ->
              Some Simpl
  