proposition: Lemma swap_prop_s1_aux : forall {G : CFGV} {vc : VarSym G}, (forall (gs : GSym G) (t : Term gs) (s : Swapping vc), isReflSwapping s -> tSwap t s = t) * (forall (gs : GSym G) (p : Pattern gs) (s : Swapping vc), isReflSwapping s -> pSwap p s = p) * (forall (lgs : list (bool * GSym G)) (m : Mixture lgs) (s : Swapping vc), isReflSwapping s -> mSwap m s = m).
proof: Proof. introv. apply GInduction; auto; introv. - intro isr; simpl. ddeq; auto. subst; simpl. rewrite swapVar_prop_s1; auto. - introv mix isr; simpl. rw mix; auto. - intro isr; simpl. destruct (DeqVarSym vc vc0); auto. subst; simpl. rewrite swapVar_prop_s1; auto. - introv tm isr; simpl. rw tm; auto. - introv mix isr; simpl. rw mix; auto. - introv tm mix isr; simpl. rw tm; auto. rw mix; auto. - introv pat tm isr; simpl. rw pat; auto. rw tm; auto. Qed.
imports: Swap AssociationList Eqdep_dec