proposition: Lemma swapVar_s2stronger : forall {G : CFGV} {vc : VarSym G} (sw : Swapping vc) (v : vType vc), swapVar ((rev sw)++sw) v = v.
proof: Proof. intros G vc sw. induction sw as [|sh sw]. - intros. simpl. trivial. - intros. simpl. rw <- app_assoc. rw (cons_as_app _ sh sw). rewrite <- swapVar_app. rewrite <- swapVar_app. rewrite <- swapVar_app. remember (swapVar (rev sw) v) as sv. rewrite (swapVar_app [sh] [sh]). rewrite swapVar_S2app. subst. rewrite swapVar_app. trivial. Qed.
imports: Swap AssociationList Eqdep_dec