Skip to content

Commit c781fc1

Browse files
committed
tighten up
1 parent 8ad7b41 commit c781fc1

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

src/Data/Fin/Properties.agda

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,8 @@ open import Relation.Binary.PropositionalEquality.Core as ≡
4545
using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst; _≗_)
4646
open import Relation.Binary.PropositionalEquality.Properties as ≡
4747
using (module ≡-Reasoning)
48-
open import Relation.Binary.PropositionalEquality using (≡-≟-identity)
48+
open import Relation.Binary.PropositionalEquality as ≡
49+
using (≡-≟-identity)
4950
open import Relation.Nullary.Decidable as Dec
5051
using (Dec; _because_; yes; no; _×-dec_; _⊎-dec_; map′)
5152
open import Relation.Nullary.Negation.Core using (¬_; contradiction)

0 commit comments

Comments
 (0)