From 9066ee48013a4351dd687c82ba5ddcf7712afd25 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Fri, 16 Jun 2017 14:34:52 -0400
Subject: [PATCH] feat(trunc): simplify proof

unreachable code was reached with the old proof in some builds
---
 hott/types/trunc.hlean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean
index aff7fcd9e..ef4993521 100644
--- a/hott/types/trunc.hlean
+++ b/hott/types/trunc.hlean
@@ -303,9 +303,7 @@ namespace is_trunc
     fapply is_trunc_equiv_closed_rev, { apply eq_equiv_equiv},
     induction n,
     { apply @is_contr_of_inhabited_prop,
-      { apply is_trunc_is_embedding_closed,
-        { apply is_embedding_to_fun} ,
-        { reflexivity}},
+      { apply is_trunc_equiv },
       { apply equiv_of_is_contr_of_is_contr}},
     { apply is_trunc_is_embedding_closed,
       { apply is_embedding_to_fun},