proposition: Lemma swapLVar_subset : forall l1 l2 l, length l1 = length l2 -> disjoint l1 l2 -> disjoint l2 l -> no_repeats l2 -> subset (@swapLVar G vc (combine l1 l2) l) (subtractv l l1 ++ l2).
proof: Proof. introv len disj1 disj2 norep. induction l; simpl; auto. apply subset_cons_l. allrw disjoint_cons_r; repnd. rewrite subtractv_cons; DDeqs; dands; tcsp. - pose proof (swapVarIn (combine l1 l2) a) as h. autorewrite with fast in h; try congruence;[]. repeat (autodimp h hyp). apply in_app_iff; sp. - rw swapVarNoChange; auto; autorewrite with fast; try congruence. Qed.
imports: Swap AssociationList Eqdep_dec