From f93278eab845f311d8d05b2441218b604e5bc922 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 19 Dec 2014 19:01:07 -0800
Subject: [PATCH] fix(hott/init/hedberg): remove unnecessary import

---
 hott/init/hedberg.hlean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/hott/init/hedberg.hlean b/hott/init/hedberg.hlean
index bd2dab47b..681b045b1 100644
--- a/hott/init/hedberg.hlean
+++ b/hott/init/hedberg.hlean
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 Hedberg's Theorem: every type with decidable equality is a hset
 -/
 prelude
-import init.nat init.trunc
+import init.trunc
 open eq eq.ops nat truncation sigma
 
 -- TODO(Leo): move const coll and path_coll to a different file?