proposition: Lemma mLSwapTermEmbedSameLBV : forall {G : CFGV} {vc : VarSym G} {mp : MixtureParam} (m : Mixture mp) (lla llb : list (list (vType vc))) (lln : list (list nat)), lBoundVars vc lln m = lBoundVars vc lln (mLSwapTermEmbed m lla llb).
proof: Proof. intros. apply lBoundVarsSameifNth. apply mLSwapTermEmbedSameNthBinder. Qed.
imports: AlphaEqProps Omega