proposition: Lemma MakeAbsTNodeCommute: forall (p: TermProd G) (m :Mixture (tpRhsAugIsPat p)) (sw: Swapping vc), swapLAbs (MakeAbstractions m (lBoundVars vc (bndngPatIndices p) m)) sw = MakeAbstractions (mSwap m sw) (lBoundVars vc (bndngPatIndices p) (mSwap m sw)).
proof: Proof. intros. rw <- swapLBoundVarsCommute. apply MakeLAbsSwapCommute. Qed.
imports: Swap