proposition: Lemma lBoundVars_swap : forall {G : CFGV} {vc : VarSym G} (lgs : list (bool * GSym G)) (m : Mixture lgs) bsl s, lBoundVars vc bsl (mSwap m s) = swapLLVar s (lBoundVars vc bsl m).
proof: Proof. induction bsl; simpl; auto; introv. rw IHbsl. apply eq_cons; auto. rewrite swapLVar_flat_map; unfold compose. apply eq_flat_maps; introv i. destruct x; simpl; auto; apply getBVarsNth_swap. Qed.
imports: Swap AssociationList Eqdep_dec