proposition: Lemma ssim1_PlusA : forall r s t, ssim1 (Plus (Plus r s) t) (Plus r (Plus s t)).
proof: Proof. rewrite /ssim1 => r s t. rewrite -ssublr /=. apply/and4P; split. - rewrite ssublPlusl ?ssubl_refl => //=. rewrite ssublPlusr ?ssubl_refl => //=. + rewrite ssublPlusr ?ssubl_refl => //=. by rewrite ssublPlusr ? ssubl_refl. by rewrite ssublPlusl ? ssubl_refl. - rewrite ssublPlusl ?ssubl_refl => //=. by rewrite ssublPlusl ?ssubl_refl. - rewrite ssublPlusl ?ssubl_refl => //=. by rewrite ssublPlusr ?ssubl_refl. by rewrite ssublPlusr ?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)