anchor.diff:    | [], None
     | [[]], None -> t
     | _ ->
  -    let t0 = force_delayed_thunk t in
  +    let t0 = try_read_memo t in
       match t0.n with
       | Tm_unknown
       | Tm_constant _                      //a constant cannot be substituted
  
positive.code:     | Tm_meta(t, m) ->
          mk (Tm_meta(subst' s t,  m))
  
  let rec compress (t:term) =
      let t = force_delayed_thunk t in
      match t.n with
      | Tm_delayed((t, s), memo) ->
          let t' = compress (push_subst s t) in
  //        Unionfind.update_in_tx memo (Some t');
  //        memo := Some t';
          t'
      | _ -> let t' = force_uvar t in
             match t'.n with
             | Tm_delayed _ -> compress t'
             | _ -> t'
  
  
  let subst s t = subst' ([s], None) t
  
negative.code:     mk_Tm_delayed ((t, s)) t.pos
  
  (*
      force_uvar' (t:term) : term * bool
          replaces any unification variable at the head of t
          with the term that it has been fixed to, if any.
  
          Also returns `true`, if it actually resolved the uvar at the head
                       `false` otherwise
  *)
  let rec force_uvar' t =
    match t.n with
    | Tm_uvar (uv,_) ->
        (match Unionfind.find uv with
            | Some t' -> fst (force_uvar' t'), true
            | _ -> t, false)
    | _ -> t, false
  
  //wraps force_uvar' to propagate any position information
  //from the uvar to anything it may have been resolved to
  let force_uvar t =
    let t', forced = force_uvar' t in
    if not forced
    then t, forced
    else delay t' ([], Some t.pos), forced
  
  //If a delayed node has already been memoized, then return the memo
  //THIS DOES NOT PUSH A SUBSTITUTION UNDER A DELAYED NODE---see push_subst for that
  let rec try_read_memo_aux t =
    match t.n with
    | Tm_delayed(f, m) ->
      (match !m with
        | None -> t, false
        | Some t' ->
          let t', shorten = try_read_memo_aux t' in
          if shorten then m := Some t';
          t', true)
    | _ -> t, false
  let try_read_memo t = fst (try_read_memo_aux t)
  
  let rec compress_univ u = match u with
      | U_unif u' ->
  