proposition: Lemma lBoundVars_equivariant : forall {G : CFGV} {vc : VarSym G} (lgs : list (bool * GSym G)) bsl, EquiVariantFn (fun m s => mSwap m s) (fun l s => swapLLVar s l) (@lBoundVars G vc lgs bsl).
proof: Proof. intros. unfold EquiVariantFn; introv. rewrite lBoundVars_swap; auto. Qed.
imports: Swap AssociationList Eqdep_dec