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
  .