proposition: Lemma freevarsEquivariant : forall {G : CFGV} {vc : VarSym G}, (forall (gs : GSym G), EquiVariantFn (@tSwap _ vc gs) (fun x s => swapLVar s x) (tfreevars vc)) * (forall (gs : GSym G), EquiVariantFn (@pSwap _ vc gs) (fun x s => swapLVar s x) (pfreevars vc )) * (forall (lgs : list (bool * GSym G)), EquiVariantFn2 (@mSwap _ vc lgs) (fun x s => swapLLVar s x) (fun x s => swapLVar s x) (@mfreevars _ _ _)).
proof: Proof. introv. GInduction; auto; introns Hyp; intros; allsimpl ; auto. - Case "vleaf". simpl. rewrite DeqSym. symmetry. rewrite DeqSym. destruct_head_match; try subst; cpx. - Case "tnode". unfold allBndngVars. rewrite <- (lBoundVars_equivariant). cpx. - Case "pnode". rewrite Hyp. simpl. refl. - Case "mtcons". rewrite <- Hyp. rewrite <- lheadEquivariant. rewrite <- swapLVar_subtractv. rewrite swapLVar_app. f_equal; cpx. rewrite <- tailEquivariant. cpx. - Case "mpcons". rewrite <- Hyp. rewrite <- lheadEquivariant. rewrite <- swapLVar_subtractv. rewrite swapLVar_app. f_equal; cpx. rewrite <- tailEquivariant. cpx. Qed.
imports: Swap AssociationList Eqdep_dec