proposition: Lemma size_invar_congr u (a b1 b2 c : word) : invar invcont_size b1 b2 -> invar invcont_size u (a ++ b1 ++ c) -> invar invcont_size u (a ++ b2 ++ c).
proof: Proof. Proof using. by rewrite /= !size_cat => /eqP ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK