Add rules for bisimulation, sliding, and denesting #1
Description
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 = {! !}