proposition: Lemma swapVarNoChange2 : forall v (vsa vsb : list vcType), !LIn v vsa -> !LIn v vsb -> swapVar (combine vsa vsb) v = v.
proof: Proof. induction vsa; simpl; introv ni1 ni2; auto. allrw not_over_or; repnd. destruct vsb; simpl; auto. allsimpl; allrw not_over_or; repnd. ddeq; sp. Qed.
imports: Swap AssociationList Eqdep_dec