proposition: Lemma MakeLAbsSwapCommute: forall (mp : MixtureParam) (sw : Swapping vc) (m : Mixture mp) (lbv : list (list vcType)), swapLAbs (MakeAbstractions m lbv) sw = MakeAbstractions (mSwap m sw) (swapLLVar sw lbv).
proof: Proof. intros np sw m. induction m; destruct lbv; allsimpl;auto; try(f_equal; auto; fail);[|]; specialize (IHm []); allsimpl; f_equal; cpx. Qed.
imports: Swap