proposition: Lemma swapSubFilterCommute: forall {G : CFGV} {vc : VarSym G} (sub : SSubstitution vc) (sw : Swapping vc) (l : list (vType vc)), ALFilter (DeqVtype vc) (swapSub sub sw) (swapLVar sw l) = swapSub (ALFilter (DeqVtype vc) sub l) sw.
proof: Proof. intros. unfold swapSub. rewrite <- ALEndoMapFilterCommute;[refl|]. introv Hq; apply swapVarInj in Hq; trivial. Qed.
imports: Term AssociationList Swap AlphaEqProps SubstAux