proposition: Lemma swap_prop_e1Stronger : forall {G : CFGV} {vc : VarSym G}, (forall (gs : GSym G) (t : Term gs) (swa swb : Swapping vc), tSwap t (swa ++ swb) = tSwap t (swb ++ (swapSwap swb swa))) * (forall (gs : GSym G) (t : Pattern gs) (swa swb : Swapping vc), pSwap t (swa ++ swb) = pSwap t (swb ++ (swapSwap swb swa))) * (forall (lgs : list (bool * GSym G)) (m : Mixture lgs) (swa swb : Swapping vc), mSwap m (swa ++ swb) = mSwap m (swb ++ (swapSwap swb swa))).
proof: Proof. introv. apply GInduction; auto; introv. - simpl. f_equal. destruct_head_match; auto. subst. simpl. apply swapVar_e1stronger. - introv mix; introv; simpl. rw mix; simpl; auto. - simpl. f_equal. destruct_head_match; auto. subst. simpl. apply swapVar_e1stronger. - introv tm; introv; simpl. rw tm; simpl; auto. - introv mix; introv; simpl. rw mix; simpl; auto. - introv tm mix; introv; simpl. rw mix; rw tm; simpl; auto. - introv pat tm; introv; simpl. rw pat; rw tm; simpl; auto. Qed.
imports: Swap AssociationList Eqdep_dec