# Does Coq do alpha conversion on it's own?

**URL:** <https://discourse.rocq-prover.org/t/does-coq-do-alpha-conversion-on-its-own/1366>\
**Category:** Using Rocq\
**Created:** [June 25, 2021, 3:54pm UTC](https://discourse.rocq-prover.org/t/does-coq-do-alpha-conversion-on-its-own/1366 "2021-06-25T15:54:35Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![brando90](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/brando90/32/183_2.png) [@brando90](https://discourse.rocq-prover.org/u/brando90)\
**Post date:** [June 25, 2021, 3:54pm UTC](https://discourse.rocq-prover.org/t/does-coq-do-alpha-conversion-on-its-own/1366/1 "2021-06-25T15:54:36Z")

</div>

I recently discovered the `Eval cbv in term` strategy for reduction but I noticed that my terms were already printed with unique names (alpha-conversion). Does Coq already do alpha-conversion on it’s own?

e.g.

```auto
  Definition l := forall x y : nat, x = y \/ forall x:nat, x < y.

  Print l.

```

displays:

```auto
l = forall x y : nat, x = y \/ (forall x0 : nat, x0 < y)
     : Prop

```

---

<div class="post-metadata">

**Author:** ![MevenBertrand](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/mevenbertrand/32/555_2.png) [@MevenBertrand](https://discourse.rocq-prover.org/u/MevenBertrand)\
**Post date:** [June 25, 2021, 4:06pm UTC](https://discourse.rocq-prover.org/t/does-coq-do-alpha-conversion-on-its-own/1366/2 "2021-06-25T16:06:21Z")

</div>

Coq performs a form of α-conversion to avoid confusion between identifiers. Here for instance x is already bound when it is encountered again in the second forall, and so it is renamed. But maybe what you had in mind was

```auto
Definition l := (forall x y ; nat, x = y) \/ (forall x : nat, x < y).

```

? In that case, Coq would be perfectly happy keeping x twice, as there is no risk of confusion.

---

<div class="post-metadata">

**Author:** ![Matafou](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/matafou/32/18_2.png) [@Matafou](https://discourse.rocq-prover.org/u/Matafou)\
**Post date:** [June 28, 2021, 7:26am UTC](https://discourse.rocq-prover.org/t/does-coq-do-alpha-conversion-on-its-own/1366/3 "2021-06-28T07:26:45Z")

</div>

To be precise, internal representation of coq terms use DeBuijn Indices for bound variables so alpha conversion is not even necessary there. Names are only there for the user and on-the-fly renaming is performed at printing for readiness.