proposition: Lemma swap_app : forall {G : CFGV} {vc : VarSym G}, (forall (gs : GSym G) (t : Term gs) (s1 s2 : Swapping vc), tSwap (tSwap t s1) s2 = tSwap t (s1 ++ s2)) * (forall (gs : GSym G) (p : Pattern gs) (s1 s2 : Swapping vc), pSwap (pSwap p s1) s2 = pSwap p (s1 ++ s2)) * (forall (lgs : list (bool * GSym G)) (m : Mixture lgs) (s1 s2 : Swapping vc), mSwap (mSwap m s1) s2 = mSwap m (s1 ++ s2)).
proof: Proof. introv. apply GInduction; auto; introv. - simpl. ddeq; auto. subst; simpl. rewrite swapVar_app; auto. - introv mix; introv; simpl. rw mix; auto. - simpl. ddeq; auto; subst; simpl. rewrite swapVar_app; auto. - introv tm; introv; simpl. rw tm; auto. - introv mix; introv; simpl. rw mix; auto. - introv tm mix; introv; simpl. rw tm; auto. rw mix; auto. - introv pat tm; introv; simpl. rw pat; auto. rw tm; auto. Qed.
imports: Swap AssociationList Eqdep_dec