proposition: Lemma swap_prop_s1 : forall {G : CFGV} {vc : VarSym G}, (forall (gs : GSym G) (t : Term gs) (a : vType vc), tSwap t [(a,a)] = t) * (forall (gs : GSym G) (p : Pattern gs) (a : vType vc), pSwap p [(a,a)] = p) * (forall (lgs : list (bool * GSym G)) (m : Mixture lgs) (a : vType vc), mSwap m [(a,a)] = m).
proof: Proof. introv. pose proof (@swap_prop_s1_aux G vc) as h; repnd. dands; introv. - apply h1; sp. - apply h0; sp. - apply h; sp. Qed.
imports: Swap AssociationList Eqdep_dec