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. unfold lBoundVars. apply eq_maps. intros n Hin. apply eq_flat_maps. intros nn Hinn. clear dependent n. clear dependent la. apply (mcase lbShallowNoChange). Qed.
imports: SubstAux AlphaEqProps