proposition: Lemma swapVarNonChangeRev: forall {G : CFGV} {vc : VarSym G} (sw : Swapping vc) (v: (vType vc)), swapVar sw v = v -> swapVar (rev sw) v = v.
proof: Proof. introv Hin. rewrite <- Hin at 1. autorewrite with SwapAppR. autorewrite with fast. refl. Qed.
imports: Swap AssociationList Eqdep_dec