proposition: Lemma swapRevNoRep : (forall (gs : GSym G) (t : Term gs) (sw : Swapping vc), no_repeats (ALDom sw) -> no_repeats (ALRange sw) -> disjoint (ALDom sw) (ALRange sw) -> tSwap t sw = tSwap t (rev sw)) * (forall (gs : GSym G) (p : Pattern gs) (sw : Swapping vc), no_repeats (ALDom sw) -> no_repeats (ALRange sw) -> disjoint (ALDom sw) (ALRange sw) -> pSwap p sw = pSwap p(rev sw)) * (forall (lgs : list (bool * GSym G)) (m : Mixture lgs) (sw : Swapping vc), no_repeats (ALDom sw) -> no_repeats (ALRange sw) -> disjoint (ALDom sw) (ALRange sw) -> mSwap m sw = mSwap m (rev sw)).
proof: Proof. introv. GInduction; auto; introv; allsimpl ; introns Hyp; allsimpl; cpx. - simpl. f_equal. rewrite DeqSym. symmetry. rewrite DeqSym. symmetry. ddeq; auto. subst. simpl. apply swapVarRevNoRep; auto. - rw Hyp; auto. - simpl. f_equal. rewrite DeqSym. symmetry. rewrite DeqSym. symmetry. ddeq; auto. subst. simpl. apply swapVarRevNoRep; auto. - rw Hyp; auto. - rw Hyp; auto. - rw Hyp; auto. rw Hyp0; auto. - rw Hyp; auto. rw Hyp0; auto. Qed.
imports: Swap AssociationList Eqdep_dec