proposition: Lemma swapVarDisjChain : forall (vsa vs vsb : list (vType vc)) (v : vType vc), length vs = length vsa -> length vs = length vsb -> no_repeats vs -> no_repeats vsb -> disjoint vs (vsa ++ vsb ++ [v]) -> disjoint vsb (vsa ++ [v]) -> swapVar ((combine vsa vs) ++ (combine vs vsb)) v = swapVar (combine vsa vsb) v.
proof: Proof. induction vsa; introv lena lenb norepa norepb disja disjb; allsimpl; destruct vs; allsimpl; cpx; destruct vsb; allsimpl; cpx. allrw disjoint_cons_l; allrw disjoint_cons_r; allrw disjoint_app_r; allrw disjoint_cons_r; allrw disjoint_app_r; allrw disjoint_singleton_r; allsimpl; allrw in_app_iff; allsimpl; allrw in_app_iff; allrw in_single_iff; allrw not_over_or; allrw no_repeats_cons; repnd; GC. ddeq; subst;try (complete cpx);[|]. - rewrite <- swapVar_app. simpl. ddeq; try subst;try (complete cpx);[| | ]. + repeat (rw swapVarNoChange2; auto). + provefalse. apply n. rw swapVarNoChange2; auto. + repeat (rw swapVarNoChange2; auto). repeat (rw swapVarNoChange2 in n; auto). cpx. - rewrite <- swapVar_app. simpl. ddeq; try subst;try (complete cpx);[| | ]. + symmetry in lena. pose proof (swapvarImplies2 vsa vs lena v) as o; simpl in o. sp. + symmetry in lena. pose proof (swapvarImplies2 vsa vs lena v) as o; simpl in o; sp. + pose proof (@in_deq vcType (DeqVtype vc) v vsa) as h. dorn h; try (complete (repeat (rw swapVarNoChange2; auto)));[]. rewrite swapVar_app. apply IHvsa; auto; allrw disjoint_app_r; allrw disjoint_singleton_r; auto. Qed.
imports: Swap AssociationList Eqdep_dec