proposition: Lemma SwapEmbedSameBinders : forall {G : CFGV} {vc : VarSym G}, (forall (s : GSym G) (ta : Term s), True) * (forall (s : GSym G) (pt : Pattern s) (sw: Swapping vc), pBndngVars vc pt = pBndngVars vc (pSwapEmbed pt sw)) * (forall (l : MixtureParam) (ma: Mixture l) (sw : Swapping vc), mBndngVars vc ma = mBndngVars vc (mSwapEmbed ma sw)).
proof: Proof. intros. GInduction; cpx;[]. Case "mpcons". introns Hyp. intros. allsimpl. f_equal; sp. Qed.
imports: Swap AssociationList Eqdep_dec