remove unused imports
[~helmut/bidiragda.git] / Precond.agda
index 81c204b..ebb5412 100644 (file)
@@ -20,11 +20,8 @@ open Data.List.Any.Membership-≡ using (_∉_)
 open import Data.Maybe using (just)
 open import Data.Product using (∃ ; _,_ ; proj₂)
 open import Function using (flip ; _∘_ ; id)
-open import Function.Equality using (_⟶_ ; _⟨$⟩_)
-open import Function.Injection using (module Injection) renaming (Injection to _↪_)
-open Injection using (to)
 open import Relation.Binary using (Setoid)
-open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym ; decSetoid) renaming (setoid to EqSetoid)
+open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym ; decSetoid)
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 open import Relation.Nullary using (yes ; no)