proposition: Lemma swapVar_s2stronger2 : forall {G : CFGV} {vc : VarSym G} (sw : Swapping vc) (v : vType vc), swapVar (sw++(rev sw)) v = v.
proof: Proof. intros. remember (rev sw) as rsw. rewrite <- rev_involutive with (l:=sw). subst. apply swapVar_s2stronger. Qed.
imports: Swap AssociationList Eqdep_dec