proposition: Lemma swapVar_prop_s1 : forall {G : CFGV} {vc : VarSym G} (s : Swapping vc) (v : vType vc), isReflSwapping s -> swapVar s v = v.
proof: Proof. induction s as [|x s]; introv isr; allsimpl; auto. destruct x as [a b]. apply isReflSwapping_cons in isr; repnd; subst. rewrite oneSwapVar_prop_s1; sp. Qed.
imports: Swap AssociationList Eqdep_dec