proposition: Lemma fpred_conc_incl : r_incl (neq eqtemp) (r_prod (r_prod nsim nsim) neqs).
proof: Proof. case => [[e f] l] [[e' f'] l']. rewrite /nsim /neq /eqtemp /eq_prod /r_prod => hneq. case: (sim_dec e e') => he. case: (sim_dec f f') => hf. - right. apply : n_eql2neql. + by apply sim_dec. move => hl; apply: hneq. by split. - by left; right. by left; left. 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)