proposition: Lemma wf_CPlus : forall r1 r2, wf_re r1 -> wf_re r2 -> wf_re (mkPlus r1 r2).
proof: Proof. move => r1 r2. case: (toolmkPlus r1). - move => heq; rewrite (eqP heq); clear heq r1. by rewrite mkPlus_CVoid_lt. - case => l1 heq; rewrite (eqP heq); clear heq r1. case : (toolmkPlus r2). * move => heq; rewrite (eqP heq); clear heq r2. by rewrite mkPlus_CVoid_rt. * case => l2 heq; rewrite (eqP heq) ; clear heq r2. move => h1 h2. by apply wf_CPlus_plus_plus. * move => h hw1 hw2; by apply wf_CPlus_plus_nplus. - move => hh1 hw1. case: (toolmkPlus r2). * move => heq; rewrite (eqP heq). move => _. by rewrite mkPlus_CVoid_rt. * case => l heq. rewrite (eqP heq); clear heq. move => h2. rewrite mkPlusC. by apply wf_CPlus_plus_nplus. * move => hh2 hw2. by apply wf_CPlus_nplus_nplus. 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)