diff --git a/src/CubicalHott/Lemma3-11-4.agda b/src/CubicalHott/Lemma3-11-4.agda
index 4ac0334..65e8af2 100644
--- a/src/CubicalHott/Lemma3-11-4.agda
+++ b/src/CubicalHott/Lemma3-11-4.agda
@@ -7,13 +7,29 @@ open import CubicalHott.Example3-6-2 renaming (example to example3-6-2)
 
 lemma : {A : Type} → isProp (isContr A)
 lemma {A} A-contr-x @ (x , px) (y , py) i =
-  let A-is-set = isProp→isSet (isContr→isProp A-contr-x) in
   px y i , goal i where
+    A-is-set = isProp→isSet (isContr→isProp A-contr-x)
+
+    helper2 : px y i ≡ y
+    helper2 = sym (py (px y i))
+
     helper1 : isProp ((z : A) → px y i ≡ z)
-    helper1 = example3-6-2 (λ x → isContr→isProp {!   !})
+    helper1 = example3-6-2 (λ z → isContr→isProp (helper2 ∙ py z , λ q → A-is-set (px y i) z (helper2 ∙ py z) q))
+
+    wtf : (z : A) → sym (px z) ∙∙ px y ∙∙ py z ≡ refl {x = z}
+    wtf z = A-is-set z z (sym (px z) ∙∙ px y ∙∙ py z) refl
+
+    helper3 : (z : A) → PathP (λ i → px z i ≡ py z i) (px y) (sym (px z) ∙∙ px y ∙∙ py z)
+    helper3 z = doubleCompPath-filler (sym (px z)) (px y) (py z)
+
+    helper5 : (z : A) → PathP (λ i → px z i ≡ py z i) (px y) (refl {x = z})
+    helper5 z = helper3 z ▷ wtf z
+
+    goal2 : (z : A) → PathP (λ i → px y i ≡ z) (px z) (py z)
+    goal2 z i j = helper5 z j i
 
     goal : PathP (λ i → (z : A) → px y i ≡ z) px py
-    goal i z = {! helper1  !}
+    goal i z j = funExt (λ z → goal2 z i) j z
 
 
-  -- λ y' j → isProp→isSet (isContr→isProp A-contr-x) (px y i) y' {!   !} {!   !} j i
\ No newline at end of file
+  -- λ y' j → isProp→isSet (isContr→isProp A-contr-x) (px y i) y' {!   !} {!   !} j i  
\ No newline at end of file