proposition: Lemma swapVarRevNoRep : forall (sw : Swapping vc) (v : vType vc), no_repeats (ALDom sw) -> no_repeats (ALRange sw) -> disjoint (ALDom sw) (ALRange sw) -> swapVar sw v = swapVar (rev sw) v.
proof: Proof. induction sw as [|(l,r) sw Hind]; auto;[]. introv H1nr H2nr Hdis. allsimpl. 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. assert (!LIn l (ALDom (rev sw))) by (allunfold ALDom; introv Hc; eauto 3 with SetReasoning). assert (!LIn r (ALDom (rev sw))) by (allunfold ALDom; introv Hc; eauto 3 with SetReasoning). assert (!LIn l (ALRange (rev sw))) by (allunfold ALRange; introv Hc; eauto 3 with SetReasoning). assert (!LIn r (ALRange (rev sw))) by (allunfold ALRange; introv Hc; eauto 3 with SetReasoning). ddeq; try subst; cpx. - rw Hind; auto. rewrite <- swapVar_app. simpl. ddeq; try (subst; cpx; fail). + rewrite swapVarNoChange; cpx. + rewrite swapVarNoChange in n; cpx. + rewrite swapVarNoChange in n; cpx. - rw Hind; auto. rewrite <- swapVar_app. simpl. ddeq; try (subst; cpx; fail). + applysym swapVarImplies in e. cpx. + rewrite swapVarNoChange; cpx. + rewrite swapVarNoChange in n1; cpx. - rw Hind; auto. rewrite <- swapVar_app. simpl. ddeq; try (subst; cpx; fail). + applysym swapVarImplies in e. cpx. + applysym swapVarImplies in e. cpx. Qed.
imports: Swap AssociationList Eqdep_dec