proposition: Lemma congrrule_invar u v : invar inv u v -> all (invar inv u) (congrrule v).
proof: Proof. Proof using Hinvar_congr. move=> Huv. apply/allP => w /flatten_mapP[[[i j1] k]] /=. rewrite -cat3_equiv_cut3 /= => /eqP Hv; subst v. move=> /mapP[j2 Hj2 ->]. apply: (Hinvar_congr _ Huv). exact: (allP (Hinvar_all (Hinvar_refl inv j1)) _ Hj2). Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK