proposition: Lemma MakeLAbsSwapCommute: forall {G : CFGV} {vc : VarSym G} (mp : MixtureParam) (sw : Swapping vc) (m : Mixture mp) (lbv : list (lVars vc)), swapEmbedLAbs (MakeAbstractions vc m lbv) sw = MakeAbstractions vc (mSwapEmbed m sw) lbv.
proof: Proof. unfold swapEmbedLAbs. intros G vc np sw m. induction m; intros; allsimpl; cpx; f_equal; cpx; destruct lbv; allsimpl; cpx. Qed.
imports: AlphaEqProps Omega