Add rules for bisimulation, sliding, and denesting

[subttle]

Roughly these rules which depend on a proof ax≡xb

bisimulation : ∀ {a b x : A} → a   ∙ x ≡ x ∙ b
                             → a * ∙ x ≡ x ∙ b *
bisimulation {a} {b} {x} ax≡xb = {!   !}

And then something like this (but I should double check):

-- sliding rule
sliding : ∀ {a b : A} → (a ∙ b) * ≡ a ∙ (b ∙ a) *
sliding {a} {b} = {!   !}

-- denesting rule
denesting : ∀ {x y z : A} → (x + y) * ≡ x * ∙ (y ∙ x *) *
denesting = {!   !}

[subttle]

Also, perhaps the Church-Rosser theorem:

  church-rosser : ∀ {a b : A} → b * ∙ a * ≤ a * ∙ b * → (a + b) * ≤ a * ∙ b *
  church-rosser = {!   !}

See "Church-Rosser Made Easy" by D. Kozen https://www.cs.cornell.edu/~kozen/Papers/ChurchRosser.pdf

There are also papers by Georg Struth (et. al) on Church-Rosser via Kleene Algebra, slides: http://events.cs.bham.ac.uk/mgs2012/lectures/StruthSlides.pdf

"Kleene Algebra" by Alasdair Armstrong, Georg Struth, Tjark Weber https://pdfs.semanticscholar.org/1f26/ccae8a47250407acebc87305e1a3b5ac5121.pdf

[subttle]

Arden's lemma: Let R, S, T be regular languages where ε∉S. Then, we have that R ≡ S · R + T iff R ≡ S∗ · T

from "Solving of Regular Equations Revisited (extended version)" https://arxiv.org/pdf/1908.03710.pdf