roboguy13

-- Idea:
-- (1) Define a language of normal forms:                                                       Nf
-- (2) Define translations to and from the normal form language:                                from-Nf, to-Nf
-- (3) Show that normal forms are equal if and only if they are equal in the original language: ==→~, ~→==
-- (4) Prove the theorem about normal form language:                                            thm′
-- (5) Reflect that proof back into a statement about the original language:                    thm

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality renaming (subst to Eq-subst)

roboguy13

open import Relation.Binary.PropositionalEquality
open import Data.Product

open ≡-Reasoning

module MagmaMonoid where

Associative : ∀ {A} → (A → A → A) → Set
Associative _<>_ =
  ∀ a b c →