proposition: Lemma swapLBoundVarsCommute : forall (l : MixtureParam) (m : Mixture l) (sw: Swapping vc) (la: list (list nat)), (swapLLVar sw) (lBoundVars vc la m) = lBoundVars vc la (mSwap m sw).
proof: Proof. intros. unfold lBoundVars. unfold swapLLVar, swapLVar. rw map_map. apply eq_maps. intros n Hin. unfold compose. rw map_flat_map. apply eq_flat_maps. intros nn Hinn. clear dependent n. clear dependent la. unfold compose. pose proof swapBndngVarsCommute as XX. unfold swapLVar in XX. exrepnd. cpx. Qed.
imports: Swap