proposition: Lemma swapSubApp : forall {G : CFGV} {vc : VarSym G} (sub : SSubstitution vc) (sa sb : Swapping vc), swapSub (swapSub sub sa) sb = swapSub sub (sa ++ sb).
proof: Proof. intros. induction sub; cpx;[]. allsimpl. f_equal; sp; auto. simpl. f_equal; autorewrite with SwapAppR; refl. Qed.
imports: Term AssociationList Swap AlphaEqProps SubstAux