Is this definition of $\alpha$-equivalence correct?

Question

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 (sub : Subst) (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 (iv : IVar) : Tm
| App (tm1 : Tm) (tm2 : Tm) : Tm
| Lam (iv : IVar) (tm1 : Tm) : Tm.

Definition Subst : Set := list (IVar * 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 (sub : Subst) : Tm -> Tm -> Prop :=
| AlphaSubstVar (iv : IVar) (tm : Tm)
  (SUBST_iv : runSubst_Var sub iv = tm)
  : AlphaSubst sub (Var iv) tm
| AlphaSubstApp (tm1_1 : Tm) (tm1_2 : Tm) (tm2_1 : Tm) (tm2_2 : Tm)
  (SUBST_tm1 : AlphaSubst sub tm1_1 tm2_1)
  (SUBST_tm2 : AlphaSubst sub tm1_2 tm2_2)
  : AlphaSubst sub (App tm1_1 tm1_2) (App tm2_1 tm2_2)
| AlphaSubstLam (iv1 : IVar) (iv2 : IVar) (tm1 : Tm) (tm2 : Tm)
  (SUBST_tm : AlphaSubst ((iv1, Var iv2) :: sub) tm1 tm2)
  : AlphaSubst sub (Lam iv1 tm1) (Lam iv2 tm2).

Definition AlphaEquiv (tm1 : Tm) (tm2 : Tm) : Prop :=
  AlphaSubst [] tm1 tm2.

Answer 1

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.

Answer 2

That is wrong. Because:

Example counter_ex : AlphaEquiv (Lam 2 (Lam 0 (Var 2))) (Lam 1 (Lam 1 (Var 1))).