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