module EquationalReasoning where

open import Equality 
open import Level

infix   proof:_ 
proof:_ :
  {ℓ : Level}
  {A : Set ℓ}
  {x y : A}
  → ---------------------
  x ≡ y → x ≡ y
proof: refl = refl

-- infixr 2 _≡[_]_
-- _≡[_]_ :
--   {ℓ : Level}
--   {A : Set ℓ}
--   (x : A)
--   {y z : A}
--   → -------------------
--   x ≡ y → y ≡ z → x ≡ z
-- _ ≡[ refl ] q = q

-- optimization from
-- <https://lists.chalmers.se/pipermail/agda/2016/009090.html>
infixr  step≡
step≡ :
  {ℓ : Level}
  {A : Set ℓ}
  (x : A)
  {y z : A}
  → -------------------
  y ≡ z → x ≡ y → x ≡ z
step≡ _ refl p = p

syntax step≡ x p q  = x ≡[ q ] p

infix   _qed 
_qed :
  {ℓ : Level}
  {A : Set ℓ}
  (x : A)
  → ---------
  x ≡ x
_ qed = refl