proposition: Lemma ssubl_refl : forall r, ssubl r r.
proof: Proof. elim => [ | | | s | c hc | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c hc ] // . - by rewrite /= !eq_refl. - rewrite ssublPlus2. by rewrite (ssublPlusl c2 hc1) (ssublPlusr c1 hc2). - by rewrite ssublAnd hc1 hc2. - by rewrite ssublConc hc1 hc2. by rewrite ssublNot -ssublr hc. Qed.
imports: Coq(RelationClasses Setoid Morphisms Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(regexp finite_der equiv)