Assume freshness of fresh.

Author: gebner

src/checker/Pulse.Checker.WithLocalArray.fst

@@ -133,12 +133,7 @@ let check
     else
       let x = fresh g in
       let px = binder.binder_ppname, x in
-      if x `Set.mem` freevars_st body
-      then fail g
-                (Some body.range)
-                (Printf.sprintf "withlocalarray: %s is free in body"
-                  (T.unseal binder.binder_ppname.name))
-      else
+      assume ~(x `Set.mem` freevars_st body);
         let x_tm = term_of_nvar px in
         let g_extended = push_binding g x binder.binder_ppname (mk_array init_t) in
         let body_pre = comp_withlocal_array_body_pre pre init_t x_tm init len in
@@ -147,10 +142,7 @@ let check
         // elaborating this post here,
         //   so that later we can check the computed post to be equal to this one
         let post : post_hint_for_env g = post in
-        if x `Set.mem` freevars post.post
-        then fail g None "Impossible! check_withlocal: unexpected name clash in with_local,\
-                          please file a bug-report"
-        else
+        assume ~(x `Set.mem` freevars post.post);
           let body_post = extend_post_hint g post init_t x in
           let (| opened_body, c_body, body_typing |) =
             let r =