proposition: Lemma swapVar_e1stronger : forall {G : CFGV} {vc : VarSym G} (swa swb : Swapping vc) (v : vType vc), swapVar (swa ++ swb) v = swapVar (swb ++ (swapSwap swb swa)) v.
proof: Proof. intros G vc sw. induction sw as [|sh sw]. - intros. simpl. autorewrite with fast. trivial. - intros. rw cons_as_app. rw <- app_assoc. simpl. rw IHsw. rewrite <- swapVar_app. rw cons_as_app. rw app_assoc. rewrite <- swapVar_app. f_equal. destruct sh as [sl sr]. simpl. cases_ifd Hd; subst; auto. + rewrite <- swapVar_app. simpl. ddeq; auto. cpx. + ddeq; subst; auto. * rewrite <- swapVar_app. simpl. ddeq; auto. cpx. * rewrite <- swapVar_app. simpl. ddeq; auto; cpx; apply swapVarInj in e; subst; cpx. Qed.
imports: Swap AssociationList Eqdep_dec