proposition: Lemma swapEmbed_prop_s1_aux : forall {G : CFGV} {vc : VarSym G}, (forall (gs : GSym G) (t : Term gs) (s : Swapping vc), True) * (forall (gs : GSym G) (p : Pattern gs) (s : Swapping vc), isReflSwapping s -> pSwapEmbed p s = p) * (forall (lgs : list (bool * GSym G)) (m : Mixture lgs) (s : Swapping vc), isReflSwapping s -> mSwapEmbed m s = m).
proof: Proof. introv. apply GInduction; auto; introv; intros; allsimpl; try (f_equal;cpx); try (f_equal; apply swap_prop_s1_aux; auto; fail). Qed.
imports: Swap AssociationList Eqdep_dec