proposition: Lemma perm_evalseq s t : perm_eq s t = (evalseq s == evalseq t).
proof: Proof. apply/idP/idP => [Hperm | /eqP]. - rewrite -!evalseq_countE /evalseq_count /=. rewrite !foldr_maxn (perm_big _ Hperm) /=. apply/eqP; apply eq_map => i. by move: Hperm => /permP ->. rewrite -!evalseq_countE /evalseq_count /=. set mx := foldr _ _ _ => H. have:= congr1 size H; rewrite !size_map !size_iota => Hmax. rewrite /perm_eq; apply /allP => i /= Hi. have {}Hi : i < mx. move: Hi; rewrite mem_cat => /orP[]. + rewrite /mx; elim s => // s0 s' IHs /=. rewrite inE => /orP[/eqP-> | Hi]; first exact: leq_maxl. rewrite leq_max; apply/orP; right. exact: IHs. + rewrite Hmax; elim t => // t0 t' IHt /=. rewrite inE => /orP[/eqP-> | Hi]; first exact: leq_maxl. rewrite leq_max; apply/orP; right. exact: IHt. move/(congr1 (fun s => nth 0 s i)) : H. rewrite (nth_map 0); last by rewrite size_iota. rewrite (nth_map 0); last by rewrite -Hmax size_iota. rewrite (nth_iota _ _ Hi) nth_iota; last by rewrite -Hmax. by rewrite !add0n => ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass partition