proposition: Lemma swapVar_S2app : forall {G : CFGV} {vc : VarSym G} (sh :vType vc * vType vc) (v : vType vc), swapVar ([sh] ++ [sh]) v = v.
proof: Proof. intros. destruct sh. simpl. simpl. ddeq; subst; auto; tcsp. Qed.
imports: Swap AssociationList Eqdep_dec