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?
Definition l := forall x y : nat, x = y \/ forall x:nat, x < y. Print l.
l = forall x y : nat, x = y \/ (forall x0 : nat, x0 < y) : Prop