Alpha-conversion for lambda terms with explicit weakenings

George Cherevichenko

Using explicit weakenings, we can define alpha-conversion by simple equations without any mention of free variables.