diff --git a/hott/homotopy/LES_of_homotopy_groups.hlean b/hott/homotopy/LES_of_homotopy_groups.hlean
index c926fcb26..39688d4b8 100644
--- a/hott/homotopy/LES_of_homotopy_groups.hlean
+++ b/hott/homotopy/LES_of_homotopy_groups.hlean
@@ -710,7 +710,7 @@ namespace chain_complex
   end
 
   definition LES_isomorphism_of_trivial_dom (n : ℕ) [H : is_succ n]
-    (HX1 : is_contr (πg[n] X)) (HX2 : is_contr (πg[n+1] X)) : πg[n+1] (Y) ≃g πg[n] (pfiber f) :=
+    (HX1 : is_contr (πg[n] X)) (HX2 : is_contr (πg[n+1] X)) : πg[n+1] Y ≃g πg[n] (pfiber f) :=
   begin
     induction H with n,
     refine isomorphism.mk (homomorphism_LES_of_homotopy_groups_fun (n, 2)) _,
diff --git a/hott/homotopy/homotopy_group.hlean b/hott/homotopy/homotopy_group.hlean
index 73e3a12f8..9d1acd6a4 100644
--- a/hott/homotopy/homotopy_group.hlean
+++ b/hott/homotopy/homotopy_group.hlean
@@ -152,7 +152,6 @@ namespace is_trunc
   begin
     apply whitehead_principle n, rexact H 0,
     intro a k, revert a, apply is_conn.elim -1,
-    { intro a, apply is_prop_is_equiv },
     have is_equiv (π→[k + 1] (pointed_eta_pequiv B ⬝e* (pequiv_of_eq_pt (respect_pt f))⁻¹ᵉ*)
            ∘* π→[k + 1] f ∘* π→[k + 1] (pointed_eta_pequiv A)⁻¹ᵉ*),
     begin