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