proposition: Lemma transP y l : all invar l -> reflect (exists x, x \in l /\ rewrite_path x y) (y \in trans l).
proof: Proof. Proof using. move=> Hl; apply: (iffP idP). - move: Hl; apply trans_ind => //=. + move=> s _ Hsz IH Hall Hy. case (IH (invar_step Hall) Hy) => x [Hx Hrew]. move: Hx; rewrite /step mem_undup mem_cat => /orP[]; first by exists x. move/flatten_mapP=> [z Hyins Hxy]. exists z; split; first exact Hyins. move: Hrew => [path Hpath Hlast]. by apply: (Rew (x :: path)); first by rewrite /= Hxy Hpath. + move=> s _ x <-; case (ltnP (size (undup s)) (size (step s))) => // Hsz _. have:= uniq_min_size (undup_uniq s) (subset_undup_step (s:= s)) Hsz. move=> [Heq _ _]; rewrite mem_undup => Hy. by exists y; split => //=; exact: (Rew [::]). + by move=> s x <-; rewrite invar_undupE; case (all invar s). - move: Hl y; apply trans_ind => //=. + move=> s _ Hsz IH Hinv y [x] [Hxins] []. case. * by move=> Hpath /= ->; apply: subset_s_trans_s; apply: subset_step. * move=> z pat /= /andP[Hz Hpath] ->. apply: IH; first exact: invar_step. exists z; split; first exact: (step_mem Hz). exact: (Rew _ Hpath). + move=> s _ x <-; case (ltnP (size (undup s)) (size (step s))) => // Hsz _. have:= uniq_min_size (undup_uniq s) (subset_undup_step (s:= s)) Hsz. move=> [_ Heq] _ y [{}x] [Hx Hrew]. by rewrite mem_undup; exact: (step_closed Heq Hx). + by move=> s x <-; rewrite invar_undupE; case (all invar s). Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK