proposition: Theorem full_bound : forall s : seq T, all invar s -> uniq s -> size s <= size full.
proof: Proof. Proof using Hfull. move=> s /allP Hall Huniq; apply: uniq_leq_size; first exact Huniq. by move=> l Hl; exact: (Hfull (Hall _ Hl)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK