proposition: Lemma lBoundVarsSameSSubstAux : forall (l : MixtureParam) (m : Mixture l) (sub: SSubstitution vc) (la : list (list nat)) (lbv : list (list (vType vc))), lBoundVars vc la m = lBoundVars vc la (mSSubstAux m lbv sub).
proof: Proof. intros. apply lBoundVarsSameifNth. pose proof bindersSSubstAuxNoCnange. cpx. Qed.
imports: Term AssociationList