proposition: Lemma mem_mkAnd : forall r1 r2, mkAnd r1 r2 =i CAnd [:: r1; r2].
proof: Proof. move => r1 r2. case: (toolmkAnd r1). - move => heq u; rewrite (eqP heq); clear r1 heq. by rewrite mkAnd_CVoid_lt !CAnd_cons. - move => heq u; rewrite (eqP heq); clear r1 heq. rewrite mkAnd_CAll_lt. rewrite !CAnd_cons in_CAll. by rewrite andbT. - case => l heq u; rewrite (eqP heq); clear r1 heq. case: (toolmkAnd r2). * move => heq; rewrite (eqP heq); clear r2 heq. by rewrite mkAnd_CVoid_rt !CAnd_cons !in_CAnd_nil andbT andbC. * move => heq; rewrite (eqP heq); clear r2 heq. rewrite /mkAnd /= !CAnd_cons in_CAll. by rewrite !andbT. * case => l' heq; rewrite (eqP heq); clear r2 heq. rewrite /mkAnd. by rewrite CAnd_mem_match CAnd_cat !CAnd_cons in_CAnd_nil andbT. * case => h1 h2 h3. rewrite toolmkAnd2_r => //. rewrite CAnd_mem_match1. by rewrite CAnd_cat !CAnd_cons in_CAnd_nil andbT. - case => h1 h2 h3. case: (toolmkAnd r2). * move => heq u; rewrite (eqP heq); clear r2 heq. by rewrite mkAnd_CVoid_rt /= !CAnd_cons !in_CAnd_nil andbT andbC. * move => heq u; rewrite (eqP heq); clear r2 heq. rewrite mkAnd_CAll_rt. by rewrite !CAnd_cons in_CAll !andbT. * case => l' heq u; rewrite (eqP heq); clear r2 heq. rewrite toolmkAnd2_l => //. by rewrite CAnd_mem_match2 CAnd_cat !CAnd_cons !in_CAnd_nil !andbT. * case => h'1 h'2 h'3. rewrite toolmkAnd3 => //. case_eq (compare r1 r2) => hc //. + rewrite (compare_eq_axiom hc) => u. rewrite !CAnd_cons in_CAnd_nil andbT. apply/idP/andP => //=. by case. + by move => u; rewrite !CAnd_cons !in_CAnd_nil !andbT andbC. Qed.
imports: Coq(RelationClasses Setoid Morphisms) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue regexp finite_der equiv)