154
154
module ≡-Reasoning where
156
module Dummy {a} {A : Set a} where
157
open EqR (setoid A) public
158
hiding (_≡⟨_⟩_) renaming (_≈⟨_⟩_ to _≡⟨_⟩_)
155
module _ {a} {A : Set a} where
156
open EqR (setoid A) public
157
hiding (_≡⟨_⟩_) renaming (_≈⟨_⟩_ to _≡⟨_⟩_)