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