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