# Alpha-conversion for lambda terms with explicit weakenings

## TL;DR

This paper introduces a new alpha-conversion method for lambda calculus with explicit weakenings, simplifying the process by eliminating the need to reference free variables.

## Contribution

It presents a novel alpha-conversion approach that uses explicit weakenings and simple equations, streamlining lambda calculus manipulations.

## Key findings

- Alpha-conversion defined without free variables
- Simplifies lambda calculus reasoning
- Potentially improves formal proof techniques

## Abstract

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