proposition: Lemma ssim1_PlusC : forall r s, ssim1 (Plus r s) (Plus s r).
proof: Proof. rewrite /ssim1 => r s. rewrite -ssublr /=. rewrite ssublPlusr ?ssubl_refl => //=. rewrite ssublPlusl ?ssubl_refl => //=. rewrite ssublPlusr ?ssubl_refl => //=. by rewrite ssublPlusl ?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)