proposition: Lemma swapLVarRevCancel : forall {G : CFGV} {vc : VarSym G} (sub : list (vType vc)) (sw : Swapping vc), swapLVar (sw ++ (rev sw)) sub= sub.
proof: Proof. intros. induction sub; cpx;[]. allsimpl. f_equal; sp; auto. simpl. autorewrite with fast;refl. Qed.
imports: Swap AssociationList Eqdep_dec