proposition: Lemma swap_prop_s2Stronger : forall {G : CFGV} {vc : VarSym G}, (forall (gs : GSym G) (t : Term gs) (sw : Swapping vc), tSwap t (sw ++ (rev sw)) = t) * (forall (gs : GSym G) (p : Pattern gs) (sw : Swapping vc), pSwap p (sw ++ (rev sw)) = p) * (forall (lgs : list (bool * GSym G)) (m : Mixture lgs) (sw : Swapping vc), mSwap m (sw ++ (rev sw)) = m).
proof: Proof. introv. GInduction; auto; introv; allsimpl ; cpx. - simpl; ddeq; auto. subst. simpl. f_equal. apply swapVar_s2stronger2. - introv mix; introv; simpl. rw mix; auto. - simpl; ddeq; auto. subst. simpl. f_equal. apply swapVar_s2stronger2. - 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