proposition: Lemma ssim1_Plus_id : forall r, ssim1 (Plus r r) r.
proof: Proof. move => r; rewrite ssim1C /ssim1. rewrite -ssublr. rewrite ssublPlusl /=. - by rewrite !ssubl_refl. by rewrite ssubl_refl. 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)