anchor.diff:          // make a Var term'
           A.Var (lid_of_path [a] r)
       in
  -    let resugar_sequence (e:A.term) : A.term =  match e.tm with
  -      | A.Let(_, [p, t1], t2) ->
  -        mk (A.Seq(t1, t2))
  -      | _ -> 
  -        failwith "This case is impossible for sequence" 
  -    in
       match (SS.compress t).n with //always call compress before case-analyzing a S.term
       | Tm_delayed _ ->
         failwith "This case is impossible after compress"
  
positive.code:     | Tm_refine(x, phi) ->
        (* bv * term -> binder * term *)
        let x, phi = SS.open_term [S.mk_binder x] phi in
        let (b, _) = x.Head in 
        let b = resugar_bv_as_binder b t.pos in
        mk (A.Refine(b, resugar_term phi))
  
  
negative.code:           | Inr fv -> mk_pat (A.PatName fv.fv_name.v), term
            | Inl bv -> 
              let x, term = SS.open_term [S.mk_binder bv] term in
              let (bv, _) = List.hd x in 
              mk_pat (A.PatVar (bv_as_unique_ident bv, None)), term
          in
          if is_pat_app then
  