proposition: Lemma exseqP (p : pred rT) : reflect (exists x, p (f x)) (exseqb p).
proof: Proof. apply: (iffP idP); last case. - case/existsP => n. case/existsP => x Hx. by exists x. - apply: (size_induction (measure := size)) => x IHx px. case H: (size x < #|rT|.+1). + apply/existsP. exists (Ordinal H). apply/existsP. by exists (in_tuple x). + have: ~ injective (fun i : 'I_(size x) => f (take i x)). { move/leq_card. by rewrite -ltnS /= card_ord H. } move/injectiveP/injectivePn => [i [j]] Hij. wlog ltn_ij : i j {Hij} / i < j => [W|] E. { move: Hij. rewrite neq_ltn. case/orP => l; exact: W l _. } apply: (IHx (take i x ++ drop j x)); last by rewrite RC_rep. by rewrite size_cat size_take size_drop ltn_ord -ltn_subRL ltn_sub2l. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)