proposition: Lemma eq_subtractv : forall vs1 vs2 l1 l2 l, disjoint l vs1 -> disjoint l vs2 -> disjoint l l1 -> disjoint l l2 -> length l = length l1 -> length l = length l2 -> no_repeats l -> @swapLVar G vc (combine l1 l) vs1 = swapLVar (combine l2 l) vs2 -> subtractv vs1 l1 = subtractv vs2 l2.
proof: Proof. induction vs1; introv disj1 disj2 disj3 disj4 len1 len2 norep e; allsimpl; destruct vs2; allsimpl; allrw subtractv_nil; allrw subtractv_nil_l; auto; inj. allapply cons_inj; repnd. repeat (rewrite subtractv_cons). allrw disjoint_cons_r; repnd. DDeqs; try (complete (eapply IHvs1; eauto)). - rw (swapVar_unchanged v) in e0; auto. pose proof (@swapVar_in l1 l a) as h; repeat (autodimp h hyp); try (complete (apply disjoint_sym; auto)). rw e0 in h; sp. - rw (swapVar_unchanged a) in e0; auto. pose proof (@swapVar_in l2 l v) as h; repeat (autodimp h hyp); try (complete (apply disjoint_sym; auto)). rw <- e0 in h; sp. - rw (swapVar_unchanged v) in e0; auto. rw (swapVar_unchanged a) in e0; auto. subst. apply eq_cons; auto. apply IHvs1 with (l := l); auto. Qed.
imports: AlphaEquality SwapProps Eqdep_dec