proposition: Lemma mkConc_unfold3 : forall r1 r2, [/\ r1 != CVoid, r1 != CEps & (forall l, r1 != CConc l) ] -> [/\ r2 != CVoid, r2 != CEps & (forall l, r2 != CConc l) ] -> mkConc r1 r2 = CConc [::r1 ; r2].
proof: Proof. case => [ | | | s | c | l | l | l | c ] /=. - by move => r2 []. - by move => r2 []. - case => [ | | | t | d | k | k | k | d ] //= _. by case. by case. case => _ _ h. move/negP: (h k); by case. - case => [ | | | t | d | k | k | k | d ] //= _. by case. by case. case => _ _ h. move/negP: (h k); by case. - case => [ | | | t | d | k | k | k | d ] //= _. by case. by case. case => _ _ h. move/negP: (h k); by case. - case => [ | | | t | d | k | k | k | d ] //= _. by case. by case. case => _ _ h. move/negP: (h k); by case. - case => [ | | | t | d | k | k | k | d ] //= _. by case. by case. case => _ _ h. move/negP: (h k); by case. - move => r2 [_ _ h]. move/negP: (h l); by case. - case => [ | | | t | d | k | k | k | d ] //= _. by case. by case. case => _ _ h. move/negP: (h k); by case. 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)