proposition: Lemma swapVar_in : forall l1 l2 v, LIn v l1 -> disjoint l1 l2 -> length l1 = length l2 -> no_repeats l2 -> LIn (@swapVar G vc (combine l1 l2) v) l2.
proof: Proof. induction l1 as [|x1 l1]; introv i1 disj len norep; allsimpl; tcsp. destruct l2 as [|x2 l2]; allsimpl; cpx. allrw disjoint_cons_l; allrw disjoint_cons_r; repnd; allsimpl. allrw not_over_or; repnd. allrw no_repeats_cons; repnd. DDeqs; sp; GC; rw (swapVar_unchanged x2); auto. Qed.
imports: AlphaEquality SwapProps Eqdep_dec