proposition: Lemma MakeAbsPNodeCommute: forall (p: PatProd G) (m : Mixture (map (fun x : GSym G => (true, x)) (ppRhsSym p))) (sw: Swapping vc), swapLAbs (MakeAbstractions m []) sw = MakeAbstractions (mSwap m sw) [].
proof: Proof. intros. unfold MakeAbstractionsPNode. apply MakeLAbsSwapCommute. Qed.
imports: Swap