proposition: Lemma mBndngVarsAsNth {G : CFGV} { vc : VarSym G} : forall (mp: @MixtureParam G) (m : Mixture mp), mBndngVars vc m = flat_map (getBVarsNth vc m) (seq 0 (length mp)).
proof: Proof. intros. induction m; cpx; allsimpl. - simpl. rw IHm. rw <- seq_shift. rw flat_map_map. unfold compose. auto. - rw IHm. rw <- seq_shift. rw flat_map_map. unfold compose. auto. Qed.
imports: CFGV Omega