proposition: Lemma swapSwitch : (forall (gs : GSym G) (t : Term gs) (sw : Swapping vc), tSwap t sw = tSwap t (ALSwitch sw)) * (forall (gs : GSym G) (p : Pattern gs) (sw : Swapping vc), pSwap p sw = pSwap p(ALSwitch sw)) * (forall (lgs : list (bool * GSym G)) (m : Mixture lgs) (sw : Swapping vc), mSwap m sw = mSwap m (ALSwitch sw)).
proof: Proof. introv. GInduction; auto; introv; allsimpl ; cpx. - simpl. f_equal. rewrite DeqSym. symmetry. rewrite DeqSym. symmetry. ddeq; auto. subst. simpl. apply swapVarSwitch. - introv mix; introv; simpl. rw mix; auto. - simpl. f_equal. rewrite DeqSym. symmetry. rewrite DeqSym. symmetry. ddeq; auto. subst. simpl. apply swapVarSwitch. - introv tm; introv; simpl. rw tm; auto. - introv mix; introv; simpl. rw mix; auto. - introv tm mix; introv; simpl. rw mix; rw tm; auto. - introv pat tm; introv; simpl. rw pat; rw tm; auto. Qed.
imports: Swap AssociationList Eqdep_dec