proposition: Lemma mLSwapTermEmbedSameNthBinder : forall {G : CFGV} {vc : VarSym G} {mp : MixtureParam} (m : Mixture mp) (lla llb : list (list (vType vc))) (nn : nat), getBVarsNth vc m nn = getBVarsNth vc (mLSwapTermEmbed m lla llb) nn.
proof: Proof. induction m; cpx; intros ; destruct nn; allsimpl; cpx. apply (pcase SwapEmbedSameBinders). Qed.
imports: AlphaEqProps Omega