proposition: Lemma mLSwapTermEmbedSameBinders : forall {G : CFGV} {vc : VarSym G} {mp : MixtureParam} (m : Mixture mp) (lla llb : list (list (vType vc))), (mBndngVars vc (mLSwapTermEmbed m lla llb)) = mBndngVars vc m.
proof: Proof. induction m; cpx;[]. simpl. intros. f_equal; cpx;[]. symmetry. apply (pcase SwapEmbedSameBinders). Qed.
imports: AlphaEqProps Omega