proposition: Lemma swapVar_unchanged : forall v l1 l2, !LIn v l1 -> !LIn v l2 -> @swapVar G vc (combine l1 l2) v = v.
proof: Proof. induction l1; introv ni1 ni2; allsimpl; auto. allrw not_over_or; repnd. destruct l2; allsimpl; auto. allrw not_over_or; repnd. DDeqs; sp. Qed.
imports: AlphaEquality SwapProps Eqdep_dec