Is this definition of $\alpha$-equivalence correct? I want to extend $\alpha$-equivalence to cover substitution.
That is, I will implement runSubst_Term : Subst -&gt; Tm -&gt; 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
    | [] =&gt; Var iv0
    | (iv, tm) :: sub' =&gt;
      if Nat.eq_dec iv iv0
      then tm
      else runSubst_Var sub' iv0
    end
  .
  Inductive AlphaSubst : Subst -&gt; Tm -&gt; Tm -&gt; Prop :=
  | AlphaSubstVar :
    forall sub : Subst,
    forall iv : IVar,
    forall tm : Tm,
    runSubst_Var sub iv = tm -&gt;
    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 -&gt;
    AlphaSubst sub tm1_2 tm2_2 -&gt;
    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 -&gt;
    AlphaSubst sub (Abs iv1 tm1) (Abs iv2 tm2)
  .
  Definition AlphaEquiv (tm1 : Tm) (tm2 : Tm) : Prop :=
    AlphaSubst [] tm1 tm2
  .
The approach itself makes sense, but the relationship with runSubst_Var probably makes proofs more difficult.
I think it's better to work on De Bruijn indices for alpha-equivalent semantics.