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.

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

displays:

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