# lambda calculus – Is this definition of \$alpha\$-equivalence correct?

I want to extend $$alpha$$-equivalence to cover substitution.

That is, I will implement `runSubst_Term : Subst -> Tm -> Tm` and prove:

``````  Theorem runSubst_Term_main_property :
forall sub : Subst,
forall tm : Tm,
AlphaSubst sub tm (runSubst_Term sub tm).
``````

where the definitions of `Subst`, `Tm`, `AlphaSubst` are below.

But I don’t sure that `AlphaEquiv` is a correct $$alpha$$-equivalence relation.

So it would be appreciated if you could check that the definition is correct.

``````  Definition IVar : Set :=
nat
.
Inductive Tm : Set :=
| Var : forall iv : IVar, Tm
| App : forall tm1 : Tm, forall tm2 : Tm, Tm
| Abs : forall iv : IVar, forall tm1 : Tm, Tm
.
Fixpoint runSubst_Var (sub : Subst) (iv0 : IVar) : Tm :=
match sub with
| () => Var iv0
| (iv, tm) :: sub' =>
if Nat.eq_dec iv iv0
then tm
else runSubst_Var sub' iv0
end
.
Inductive AlphaSubst : Subst -> Tm -> Tm -> Prop :=
| AlphaSubstVar :
forall sub : Subst,
forall iv : IVar,
forall tm : Tm,
runSubst_Var sub iv = tm ->
AlphaSubst sub (Var iv) tm
| AlphaSubstApp :
forall sub : Subst,
forall tm1_1 : Tm,
forall tm1_2 : Tm,
forall tm2_1 : Tm,
forall tm2_2 : Tm,
AlphaSubst sub tm1_1 tm2_1 ->
AlphaSubst sub tm1_2 tm2_2 ->
AlphaSubst sub (App tm1_1 tm1_2) (App tm2_1 tm2_2)
| AlphaSubstAbs :
forall sub : Subst,
forall iv1 : IVar,
forall iv2 : IVar,
forall tm1 : Tm,
forall tm2 : Tm,
AlphaSubst ((iv1, Var iv2) :: sub) tm1 tm2 ->
AlphaSubst sub (Abs iv1 tm1) (Abs iv2 tm2)
.
Definition AlphaEquiv (tm1 : Tm) (tm2 : Tm) : Prop :=
AlphaSubst () tm1 tm2
.
``````