proposition: Lemma swapvarImplies2 : forall (vs1 vs2 : list vcType), length vs1 = length vs2 -> forall v, let w := swapVar (combine vs1 vs2) v in w = v [+] LIn w vs1 [+] LIn w vs2.
proof: Proof. simpl; induction vs1 as [| va vs1 IHvs1]; introv len; introv; allsimpl; destruct vs2 as [|vb vs2]; allsimpl; cpx. ddeq; sp; subst. - pose proof (IHvs1 vs2 len vb) as h; sp. - pose proof (IHvs1 vs2 len va) as h; sp. - pose proof (IHvs1 vs2 len v) as h; sp. Qed.
imports: Swap AssociationList Eqdep_dec