proposition: Lemma AllVarsEquivariant : forall {G : CFGV} {vc : VarSym G}, (forall (gs : GSym G), EquiVariantFn (@tSwap _ vc gs) (fun x s => swapLVar s x) (tAllVars )) * (forall (gs : GSym G), EquiVariantFn (@pSwap _ vc gs) (fun x s => swapLVar s x) (pAllVars )) * (forall (lgs : list (bool * GSym G)), EquiVariantFn (@mSwap _ vc lgs) (fun x s => swapLVar s x) (mAllVars )).
proof: Proof. introv. GInduction; auto; introns Hyp; intros; allsimpl ; auto. - simpl. rewrite DeqSym. symmetry. rewrite DeqSym. destruct_head_match; try subst; cpx. - simpl. rewrite DeqSym. symmetry. rewrite DeqSym. destruct_head_match; try subst; cpx. - unfold swapLVar. rw map_app. unfold swapLVar in Hyp0. unfold swapLVar in Hyp. f_equal; cpx. - unfold swapLVar. rw map_app. unfold swapLVar in Hyp0. unfold swapLVar in Hyp. f_equal; cpx. Qed.
imports: Swap AssociationList Eqdep_dec