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},