{-# OPTIONS --type-in-type #-}

open import NeilPrelude

module EquationalEq where

import Equational
open Equational _≡_ refl trans public


-- open import NatProps
-- open import Nat

-- exampleLem1 : (n : ℕ) → (n + O) + n ≡ (n + n) + O
-- exampleLem1 n =  n + O + n
--                     ⟨ comm {n + O}⟩
--                  n + (n + O)
--                     ⟨ assocR {n} ⟩
--                  (n + n) + O 
--                     QED