proposition: Lemma finite_pred_singl : forall P, Finite (pred_singl P).
proof: Proof. move => P. apply: cBar => G1. rewrite /In /pred_singl => h1. apply cBar => G2. case => []. move => h2. case. move: h1 h2. rewrite /sim. move => h1 h2. transitivity P => //. by symmetry. Qed.
imports: Coq(RelationClasses Setoid Morphisms Permutation) Coq(SetoidList Mergesort Orders) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp)