proposition: Lemma wf_CAnd : forall r1 r2, wf_re r1 -> wf_re r2 -> wf_re (mkAnd r1 r2).
proof: Proof. move => r1 r2. case: (toolmkAnd r1). - move => heq; rewrite (eqP heq); clear heq r1. by rewrite mkAnd_CVoid_lt. - move => heq; rewrite (eqP heq); clear heq r1. by rewrite mkAnd_CAll_lt. - case => l1 heq; rewrite (eqP heq); clear heq r1. case : (toolmkAnd r2). * move => heq; rewrite (eqP heq); clear heq r2. by rewrite mkAnd_CVoid_rt. * move => heq; rewrite (eqP heq); clear heq r2. by rewrite mkAnd_CAll_rt. * case => l2 heq; rewrite (eqP heq) ; clear heq r2. move => h1 h2. by apply wf_CAnd_and_and. * move => hh1 hw1 hw2. by apply wf_CAnd_and_nand. - move => hh1 hw1. case: (toolmkAnd r2). * move => heq; rewrite (eqP heq). move => _. by rewrite mkAnd_CVoid_rt. * move => heq; rewrite (eqP heq); clear heq r2. by rewrite mkAnd_CAll_rt. * case => l heq. rewrite (eqP heq); clear heq. move => hw2. rewrite mkAndC. by apply wf_CAnd_and_nand. * move => hh2 hw2. by apply wf_CAnd_nand_nand. 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)