proposition: Lemma swapPreservesSize :forall {G : CFGV} {vc : VarSym G} (sw : Swapping vc), ( (forall (s : GSym G) (t : Term s), tSize (tSwap t sw) = tSize t ) * (forall (s : GSym G) (pt : Pattern s), pSize (pSwap pt sw) = pSize pt) * (forall (l : @MixtureParam G) (m : Mixture l), mSize (mSwap m sw) = mSize m)).
proof: Proof. intros. GInduction; intros; allsimpl; auto. Qed.
imports: Swap AssociationList Eqdep_dec