diff --git a/src/CubicalHott/Lemma7-3-1.agda b/src/CubicalHott/Lemma7-3-1.agda
new file mode 100644
index 0000000..513a5ac
--- /dev/null
+++ b/src/CubicalHott/Lemma7-3-1.agda
@@ -0,0 +1,11 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Lemma7-3-1 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.HITs.Truncation
+open import Data.Nat
+
+lemma : {A : Type} → (n : ℕ) → isOfHLevel n (∥ A ∥ n)
+lemma {A} n = {!   !}
\ No newline at end of file
diff --git a/src/CubicalHott/Theorem7-1-11.agda b/src/CubicalHott/Theorem7-1-11.agda
index 616c482..0826a80 100644
--- a/src/CubicalHott/Theorem7-1-11.agda
+++ b/src/CubicalHott/Theorem7-1-11.agda
@@ -73,10 +73,13 @@ lemma zero (A , a , Acontr) (B , b , Bcontr) i =
     --       in hfill u (inS (a≡b {! j  !})) j
     --   in {!   !}
 
+lemma (suc zero) (A , A-prop) (B , B-prop) p q =
+  let IH = lemma zero in
+  {!   !}
 
-lemma (suc zero) (A , A-prop) (B , B-prop) x y i j = {!   !}
-
-lemma (suc (suc n)) x y = {!   !}
+lemma (suc (suc n)) x y p q =
+  let IH = lemma (suc n) in
+  {!   !}
 
 -- lemma : ∀ {l} → (n : HLevel) → isOfHLevel (suc n) (TypeOfHLevel l n)
 -- lemma zero (A , a , Acontr) (B , b , Bcontr) i = G , g , contr where