proposition: Lemma swapLVarDisjoint2: forall (swl swr lv: list (vType vc)), disjoint lv swr -> length swl = length swr -> no_repeats swr -> disjoint swl swr -> disjoint (swapLVar (combine swl swr) lv) swl.
proof: Proof. intros. pose proof (swapLVarDisjoint (combine swl swr)) as XX. specialize (XX lv). autorewrite with fast in XX; try congruence. apply XX; auto. Qed.
imports: Swap AssociationList Eqdep_dec