proposition: Lemma swapVar_app : forall {G : CFGV} {vc : VarSym G} (s1 s2 : Swapping vc) (v : vType vc), swapVar s2 (swapVar s1 v) = swapVar (s1 ++ s2) v.
proof: Proof. induction s1 as [|x s1]; introv; simpl; sp. Qed.
imports: Swap AssociationList Eqdep_dec