proposition: Lemma swap_prop_s3 : forall {G : CFGV} {vc : VarSym G} (a a' : vType vc), (tSwap (vleaf vc a) [(a,a')] = vleaf vc a') * (pSwap (pvleaf vc a) [(a,a')] = pvleaf vc a').
proof: Proof. introv; simpl; DDeqs; sp. Qed.
imports: Swap AssociationList Eqdep_dec