proposition: Lemma mRenlBinderShallowSame : forall {G : CFGV} {vc : VarSym G} (l : MixtureParam) (m : Mixture l) (lvA : list (vType vc)) (la : list (list nat)), lBoundVars vc la m = lBoundVars vc la (mRenAlpha m lvA).
proof: Proof. intros. apply lBoundVarsSameifNth. apply (mcase lbShallowNoChange). Qed.
imports: AlphaEqProps Omega