diff --git a/src/bin/expect_tests/contract_tests.ml b/src/bin/expect_tests/contract_tests.ml
index 8d614c9aac..a0f8c6f165 100644
--- a/src/bin/expect_tests/contract_tests.ml
+++ b/src/bin/expect_tests/contract_tests.ml
@@ -1159,7 +1159,7 @@ File "../../test/contracts/negative/create_contract_toplevel.mligo", line 5, cha
       ^^^^^^^^
  10 |   in
 
-Not all free variables could be inlined in Tezos.create_contract usage: gen#430. |}];
+Not all free variables could be inlined in Tezos.create_contract usage: gen#474. |}];
   run_ligo_good [ "compile"; "contract"; contract "create_contract_var.mligo" ];
   [%expect
     {|
@@ -1251,7 +1251,7 @@ Not all free variables could be inlined in Tezos.create_contract usage: gen#430.
           ^^^^^^^^^^
      15 |   ([toto.0], store)
 
-    Not all free variables could be inlined in Tezos.create_contract usage: gen#431. |}];
+    Not all free variables could be inlined in Tezos.create_contract usage: gen#475. |}];
   run_ligo_bad [ "compile"; "contract"; bad_contract "create_contract_no_inline.mligo" ];
   [%expect
     {|
@@ -1314,7 +1314,7 @@ Not all free variables could be inlined in Tezos.create_contract usage: gen#430.
           ^^^^^^^
      15 |   let toto : operation list = [op] in
 
-    Not all free variables could be inlined in Tezos.create_contract usage: foo#445. |}];
+    Not all free variables could be inlined in Tezos.create_contract usage: foo#489. |}];
   run_ligo_good [ "compile"; "contract"; contract "create_contract.mligo" ];
   [%expect
     {|
diff --git a/src/passes/15-self_mini_c/inline.ml b/src/passes/15-self_mini_c/inline.ml
index e1c9c319bb..ac942485c1 100644
--- a/src/passes/15-self_mini_c/inline.ml
+++ b/src/passes/15-self_mini_c/inline.ml
@@ -3,158 +3,6 @@ open Mini_c
 open Helpers
 module Ligo_pair = Simple_utils.Ligo_pair
 
-(* Reference implementation:
-   https://www.cs.cornell.edu/courses/cs3110/2019sp/textbook/interp/lambda-subst/main.ml
-
-   ...but, it has at least one bug: in subst,
-   `let new_body = replace e' y fresh in ...` should be:
-   `let new_body = replace e' fresh y in ...`,
-   due to the arg order choice for replace.
-
-   Below, this bug is fixed by adopting the other order choice for
-   replace (as well as subst).  *)
-
-let replace_var : var_name -> var_name -> var_name -> var_name =
- fun v x y -> if Value_var.equal v x then y else v
-
-
-(* replace in `e` the variable `x` with `y`.
-
-   It would be fine -- better? -- to only replace the _free_ x.
-*)
-let rec replace : expression -> var_name -> var_name -> expression =
- fun e x y ->
-  let replace e = replace e x y in
-  let return content = { e with content } in
-  let replace_var v = replace_var v x y in
-  match e.content with
-  | E_literal _ -> e
-  | E_closure { binder; body } ->
-    let body = replace body in
-    let binder = replace_var binder in
-    return @@ E_closure { binder; body }
-  | E_rec { func = { binder; body }; rec_binder } ->
-    let body = replace body in
-    let binder = replace_var binder in
-    let rec_binder = replace_var rec_binder in
-    return @@ E_rec { func = { binder; body }; rec_binder }
-  | E_constant c ->
-    let args = List.map ~f:replace c.arguments in
-    return @@ E_constant { cons_name = c.cons_name; arguments = args }
-  | E_application (f, x) ->
-    let f, x = Ligo_pair.map ~f:replace (f, x) in
-    return @@ E_application (f, x)
-  | E_variable z ->
-    let z = replace_var z in
-    return @@ E_variable z
-  | E_iterator (name, ((v, tv), body), expr) ->
-    let body = replace body in
-    let expr = replace expr in
-    let v = replace_var v in
-    return @@ E_iterator (name, ((v, tv), body), expr)
-  | E_fold (((v, tv), body), collection, initial) ->
-    let body = replace body in
-    let collection = replace collection in
-    let initial = replace initial in
-    let v = replace_var v in
-    return @@ E_fold (((v, tv), body), collection, initial)
-  | E_fold_right (((v, tv), body), (collection, elem_tv), initial) ->
-    let body = replace body in
-    let collection = replace collection in
-    let initial = replace initial in
-    let v = replace_var v in
-    return @@ E_fold_right (((v, tv), body), (collection, elem_tv), initial)
-  | E_if_bool (c, bt, bf) ->
-    let c = replace c in
-    let bt = replace bt in
-    let bf = replace bf in
-    return @@ E_if_bool (c, bt, bf)
-  | E_if_none (c, bt, ((v, tv), bf)) ->
-    let c = replace c in
-    let bt = replace bt in
-    let bf = replace bf in
-    let v = replace_var v in
-    return @@ E_if_none (c, bt, ((v, tv), bf))
-  | E_if_cons (c, bf, (((v1, tv1), (v2, tv2)), bt)) ->
-    let c = replace c in
-    let bf = replace bf in
-    let v1 = replace_var v1 in
-    let v2 = replace_var v2 in
-    let bt = replace bt in
-    return @@ E_if_cons (c, bf, (((v1, tv1), (v2, tv2)), bt))
-  | E_if_left (c, ((v1, tv1), bt), ((v2, tv2), bf)) ->
-    let c = replace c in
-    let bf = replace bf in
-    let v1 = replace_var v1 in
-    let v2 = replace_var v2 in
-    let bt = replace bt in
-    return @@ E_if_left (c, ((v1, tv1), bt), ((v2, tv2), bf))
-  | E_let_in (e1, inline, ((v, tv), e2)) ->
-    let v = replace_var v in
-    let e1 = replace e1 in
-    let e2 = replace e2 in
-    return @@ E_let_in (e1, inline, ((v, tv), e2))
-  | E_tuple exprs ->
-    let exprs = List.map ~f:replace exprs in
-    return @@ E_tuple exprs
-  | E_let_tuple (expr, (vtvs, body)) ->
-    let expr = replace expr in
-    let vtvs = List.map ~f:(fun (v, tv) -> replace_var v, tv) vtvs in
-    let body = replace body in
-    return @@ E_let_tuple (expr, (vtvs, body))
-  | E_proj (expr, i, n) ->
-    let expr = replace expr in
-    return @@ E_proj (expr, i, n)
-  | E_update (expr, i, update, n) ->
-    let expr = replace expr in
-    let update = replace update in
-    return @@ E_update (expr, i, update, n)
-  | E_raw_michelson code -> return @@ E_raw_michelson code
-  | E_inline_michelson (code, args') ->
-    let args' = List.map ~f:replace args' in
-    return @@ E_inline_michelson (code, args')
-  | E_global_constant (hash, args) ->
-    let args = List.map ~f:replace args in
-    return @@ E_global_constant (hash, args)
-  | E_create_contract (p, s, ((x, t), code), args) ->
-    let args = List.map ~f:replace args in
-    let x = replace_var x in
-    let code = replace code in
-    return @@ E_create_contract (p, s, ((x, t), code), args)
-  (* Mutable stuff. We treat immutable and mutable variables
-     identically because they share the context (e.g. a mutable
-     variables might need to be renamed for capture-avoidance during
-     substitution of an immutable variable.) *)
-  | E_let_mut_in (e1, ((v, tv), e2)) ->
-    let v = replace_var v in
-    let e1 = replace e1 in
-    let e2 = replace e2 in
-    return @@ E_let_mut_in (e1, ((v, tv), e2))
-  | E_deref v ->
-    let v = replace_var v in
-    return @@ E_deref v
-  | E_assign (v, e) ->
-    let v = replace_var v in
-    let e = replace e in
-    return @@ E_assign (v, e)
-  | E_for (start, final, incr, ((x, a), body)) ->
-    let start = replace start in
-    let final = replace final in
-    let incr = replace incr in
-    let x = replace_var x in
-    let body = replace body in
-    return @@ E_for (start, final, incr, ((x, a), body))
-  | E_for_each (coll, coll_type, (xs, body)) ->
-    let coll = replace coll in
-    let xs = List.map ~f:(fun (x, a) -> replace_var x, a) xs in
-    let body = replace body in
-    return @@ E_for_each (coll, coll_type, (xs, body))
-  | E_while (cond, body) ->
-    let cond = replace cond in
-    let body = replace body in
-    return @@ E_while (cond, body)
-
-
 (** Set with free variables. *)
 module Fvs = Set.Make (Value_var)
 
diff --git a/src/passes/15-self_mini_c/rename.ml b/src/passes/15-self_mini_c/rename.ml
new file mode 100644
index 0000000000..60d81e1abe
--- /dev/null
+++ b/src/passes/15-self_mini_c/rename.ml
@@ -0,0 +1,163 @@
+open Mini_c
+open Ligo_prim
+module Var_map = Map.Make (Value_var)
+
+(** Global alpha renaming *)
+
+(**
+  The main goal is to ensures that every binder has a unique name globally.
+  
+  The main advantage is that a transformation such
+    as moving a let will never capture a variable.
+
+  let x = (let y = M in N) in K ↦ let y = M; let x = N in K
+*)
+let rec rename ~substs expr =
+  let self expr = rename ~substs expr in
+  let with_binder ~substs v =
+    let v' = Value_var.fresh_like v in
+    v', Map.update substs v ~f:(fun _ -> v')
+  in
+  let self_with_binder v ~body =
+    let v, substs = with_binder ~substs v in
+    let body = rename ~substs body in
+    v, body
+  in
+  let self_with_binder_pair (v1, v2) ~body =
+    let v1, substs = with_binder ~substs v1 in
+    let v2, substs = with_binder ~substs v2 in
+    let body = rename ~substs body in
+    (v1, v2), body
+  in
+  let self_with_binders vs ~body =
+    let rev_vs, substs =
+      List.fold_left vs ~init:([], substs) ~f:(fun (rev_vs, substs) (v, vt) ->
+          let v, substs = with_binder ~substs v in
+          let rev_vs = (v, vt) :: rev_vs in
+          rev_vs, substs)
+    in
+    let body = rename ~substs body in
+    List.rev rev_vs, body
+  in
+  let solve_variable v =
+    match Map.find substs v with
+    | Some v' -> v'
+    | None ->
+      (* TODO: why does this happen? *)
+      v
+  in
+  let return_expr content = { expr with content } in
+  match expr.content with
+  (* Here actual substitutions are created. *)
+  | E_let_in (expr, inline, ((v, tv), body)) ->
+    let expr = self expr in
+    let v, body = self_with_binder v ~body in
+    return_expr @@ E_let_in (expr, inline, ((v, tv), body))
+  | E_let_mut_in (expr, ((v, tv), body)) ->
+    let expr = self expr in
+    let v, body = self_with_binder v ~body in
+    return_expr @@ E_let_mut_in (expr, ((v, tv), body))
+  (* Variables and dereferencing. *)
+  | E_variable v ->
+    let v = solve_variable v in
+    return_expr @@ E_variable v
+  | E_deref v ->
+    let v = solve_variable v in
+    return_expr @@ E_deref v
+  (* Other stuff. *)
+  | E_closure { binder; body } ->
+    let binder, body = self_with_binder binder ~body in
+    return_expr @@ E_closure { binder; body }
+  | E_rec { func = { binder; body }; rec_binder } ->
+    let (binder, rec_binder), body = self_with_binder_pair (binder, rec_binder) ~body in
+    return_expr @@ E_rec { func = { binder; body }; rec_binder }
+  | E_tuple exprs ->
+    let exprs = List.map ~f:self exprs in
+    return_expr @@ E_tuple exprs
+  | E_let_tuple (expr, (vtvs, body)) ->
+    let expr = self expr in
+    let vtvs, body = self_with_binders vtvs ~body in
+    return_expr @@ E_let_tuple (expr, (vtvs, body))
+  | E_proj (expr, i, n) ->
+    let expr = self expr in
+    return_expr @@ E_proj (expr, i, n)
+  | E_update (expr, i, update, n) ->
+    let expr = self expr in
+    let update = self update in
+    return_expr @@ E_update (expr, i, update, n)
+  | E_iterator (s, ((name, tv), body), collection) ->
+    let collection = self collection in
+    let name, body = self_with_binder name ~body in
+    return_expr @@ E_iterator (s, ((name, tv), body), collection)
+  | E_fold (((name, tv), body), collection, init) ->
+    let collection = self collection in
+    let init = self init in
+    let name, body = self_with_binder name ~body in
+    return_expr @@ E_fold (((name, tv), body), collection, init)
+  | E_fold_right (((name, tv), body), (collection, elem_tv), init) ->
+    let collection = self collection in
+    let init = self init in
+    let name, body = self_with_binder name ~body in
+    return_expr @@ E_fold_right (((name, tv), body), (collection, elem_tv), init)
+  | E_if_none (c, n, ((name, tv), s)) ->
+    let c = self c in
+    let n = self n in
+    let name, s = self_with_binder name ~body:s in
+    return_expr @@ E_if_none (c, n, ((name, tv), s))
+  | E_if_cons (c, n, (((hd, hdtv), (tl, tltv)), cons)) ->
+    let c = self c in
+    let n = self n in
+    let (hd, tl), cons = self_with_binder_pair (hd, tl) ~body:cons in
+    return_expr @@ E_if_cons (c, n, (((hd, hdtv), (tl, tltv)), cons))
+  | E_if_left (c, ((name_l, tvl), l), ((name_r, tvr), r)) ->
+    let c = self c in
+    let name_l, l = self_with_binder name_l ~body:l in
+    let name_r, r = self_with_binder name_r ~body:r in
+    return_expr @@ E_if_left (c, ((name_l, tvl), l), ((name_r, tvr), r))
+  | E_raw_michelson code -> return_expr @@ E_raw_michelson code
+  | E_inline_michelson (code, args) ->
+    let args' = List.map ~f:self args in
+    return_expr @@ E_inline_michelson (code, args')
+  | E_literal _ -> expr
+  | E_constant { cons_name; arguments } ->
+    let arguments = List.map ~f:self arguments in
+    return_expr @@ E_constant { cons_name; arguments }
+  | E_application (farg1, farg2) ->
+    let farg1 = self farg1 in
+    let farg2 = self farg2 in
+    return_expr @@ E_application (farg1, farg2)
+  | E_if_bool (cab1, cab2, cab3) ->
+    let cab1 = self cab1 in
+    let cab2 = self cab2 in
+    let cab3 = self cab3 in
+    return_expr @@ E_if_bool (cab1, cab2, cab3)
+  | E_global_constant (hash, args) ->
+    let args = List.map ~f:self args in
+    return_expr @@ E_global_constant (hash, args)
+  | E_create_contract (p, s, ((x, t), code), args) ->
+    let args = List.map ~f:self args in
+    let x, code = self_with_binder x ~body:code in
+    return_expr @@ E_create_contract (p, s, ((x, t), code), args)
+  (* Mutable stuff. We allow substituting mutable variables which
+      aren't mutated because it was easy. Hmm. *)
+  | E_assign (v, e) ->
+    let v = solve_variable v in
+    let e = self e in
+    return_expr @@ E_assign (v, e)
+  | E_for (start, final, incr, ((x, a), body)) ->
+    let start = self start in
+    let final = self final in
+    let incr = self incr in
+    let x, body = self_with_binder x ~body in
+    return_expr @@ E_for (start, final, incr, ((x, a), body))
+  | E_for_each (coll, coll_type, (xs, body)) ->
+    let coll = self coll in
+    let xs, body = self_with_binders xs ~body in
+    return_expr @@ E_for_each (coll, coll_type, (xs, body))
+  | E_while (cond, body) ->
+    let cond = self cond in
+    let body = self body in
+    return_expr @@ E_while (cond, body)
+
+
+let rename expr = rename ~substs:Var_map.empty expr
diff --git a/src/passes/15-self_mini_c/self_mini_c.ml b/src/passes/15-self_mini_c/self_mini_c.ml
index c00839742a..d803922daf 100644
--- a/src/passes/15-self_mini_c/self_mini_c.ml
+++ b/src/passes/15-self_mini_c/self_mini_c.ml
@@ -150,15 +150,13 @@ let beta : bool ref -> expression -> expression =
   (* (let x = (let y = e1 in e2) in e3) ↦ (let y = e1 in let x = e2 in e3) *)
   | E_let_in ({ content = E_let_in (e1, inline2, ((y, b), e2)); _ }, inline1, ((x, a), e3))
     ->
-    let y' = Value_var.fresh_like y in
-    let e2 = Inline.replace e2 y y' in
     changed := true;
     { e with
       content =
         E_let_in
           ( e1
           , inline2
-          , ((y', b), { e with content = E_let_in (e2, inline1, ((x, a), e3)) }) )
+          , ((y, b), { e with content = E_let_in (e2, inline1, ((x, a), e3)) }) )
     }
   (* note: E_let_tuple/E_let_in and E_let_in/E_let_tuple conversions
      not implemented yet because they don't seem important (?) *)
@@ -166,23 +164,16 @@ let beta : bool ref -> expression -> expression =
   | E_application ({ content = E_let_in (e1, inline, ((x, a), e2)); _ }, e3) ->
     if is_pure e1 || is_pure e3
     then (
-      let x' = Value_var.fresh_like x in
-      let e2 = Inline.replace e2 x x' in
       changed := true;
       { e with
         content =
-          E_let_in (e1, inline, ((x', a), { e with content = E_application (e2, e3) }))
+          E_let_in (e1, inline, ((x, a), { e with content = E_application (e2, e3) }))
       })
     else e
   (* (let (x, y, ...) = e1 in e2)@e3 ↦ let (x, y, ...) = e1 in e2@e3  (if e1 or e3 is pure) *)
   | E_application ({ content = E_let_tuple (e1, (vars, e2)); _ }, e3) ->
     if is_pure e1 || is_pure e3
     then (
-      let vars = List.map ~f:(fun (x, a) -> x, Value_var.fresh_like x, a) vars in
-      let e2 =
-        List.fold_left vars ~init:e2 ~f:(fun e2 (x, x', _a) -> Inline.replace e2 x x')
-      in
-      let vars = List.map ~f:(fun (_x, x', a) -> x', a) vars in
       changed := true;
       { e with
         content = E_let_tuple (e1, (vars, { e with content = E_application (e2, e3) }))
@@ -295,6 +286,7 @@ let rec all_expression ~raise (options : Compiler_options.t) : expression -> exp
   else (
     let changed = ref false in
     let e = inline_lets changed e in
+    let e = Rename.rename e in
     let e = betas changed e in
     let e = etas changed e in
     let e = not_comparable ~raise e in
diff --git a/src/test/contracts/bytes_arithmetic.jsligo b/src/test/contracts/bytes_arithmetic.jsligo
index 1aba4c8f6d..8d773b5235 100644
--- a/src/test/contracts/bytes_arithmetic.jsligo
+++ b/src/test/contracts/bytes_arithmetic.jsligo
@@ -1,3 +1,5 @@
 let concat_op = (s: bytes): bytes => Bytes.concat(s, 0x7070);
+let nested_concat_op = (s: bytes): bytes =>
+  Bytes.concat(Bytes.concat(s, 0x5faaaa), 0xcd);
 let slice_op = (s: bytes): bytes => Bytes.sub(1n, 2n, s);
 let hasherman = (s: bytes): bytes => Crypto.sha256(s);
diff --git a/src/test/contracts/bytes_arithmetic.mligo b/src/test/contracts/bytes_arithmetic.mligo
index dbdc2a1474..425133bda0 100644
--- a/src/test/contracts/bytes_arithmetic.mligo
+++ b/src/test/contracts/bytes_arithmetic.mligo
@@ -1,3 +1,6 @@
+
 let concat_op (s : bytes) : bytes = Bytes.concat s 0x7070
+let nested_concat_op (s : bytes) : bytes =
+  Bytes.concat (Bytes.concat s 0x5faaaa) 0xcd
 let slice_op  (s : bytes) : bytes = Bytes.sub 1n 2n s
 let hasherman (s : bytes) : bytes = Crypto.sha256 s
diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml
index 0efd137e88..c89872b4bf 100644
--- a/src/test/integration_tests.ml
+++ b/src/test/integration_tests.ml
@@ -292,8 +292,11 @@ let bytes_arithmetic ~raise f : unit =
   let tata = e_bytes_hex_ez ~loc "ff7a7aff" in
   let at = e_bytes_hex_ez ~loc "7a7a" in
   let ba = e_bytes_hex_ez ~loc "ba" in
+  let ab = e_bytes_hex_ez ~loc "ab" in
+  let ab5faaaacd = e_bytes_hex_ez ~loc "ab5faaaacd" in
   let () = expect_eq ~raise program "concat_op" foo foototo in
   let () = expect_eq ~raise program "concat_op" empty toto in
+  let () = expect_eq ~raise program "nested_concat_op" ab ab5faaaacd in
   let () = expect_eq ~raise program "slice_op" tata at in
   let () = expect_fail ~raise program "slice_op" foo in
   let () = expect_fail ~raise program "slice_op" ba in