diff --git a/cs3234/labs/week-03_structural-induction-over-binary-trees.v b/cs3234/labs/week-03_structural-induction-over-binary-trees.v
index 4f65d36..cc5b715 100644
--- a/cs3234/labs/week-03_structural-induction-over-binary-trees.v
+++ b/cs3234/labs/week-03_structural-induction-over-binary-trees.v
@@ -199,6 +199,9 @@ Proof.
     reflexivity.
   - rewrite -> (S_Node V t1 t2).
     Check (mirror_is_involutory mirror S_mirror V t1).
+    (* TODO: Figure this out *)
+
+    Abort.
 
 
 
@@ -233,60 +236,8 @@ Qed.
 
 (* ********** *)
 
-Definition specification_of_number_of_leaves (number_of_leaves : forall V : Type, binary_tree V -> nat) : Prop :=
-  (forall (V : Type)
-          (v : V),
-      number_of_leaves V (Leaf V v) =
-      1)
-  /\
-  (forall (V : Type)
-          (t1 t2 : binary_tree V),
-      number_of_leaves V (Node V t1 t2) =
-      number_of_leaves V t1 + number_of_leaves V t2).
-
-(* ***** *)
-
-(* Exercise 09b *)
-
-Proposition there_is_at_most_one_number_of_leaves_function :
-  forall number_of_leaves1 number_of_leaves2 : forall V : Type, binary_tree V -> nat,
-    specification_of_number_of_leaves number_of_leaves1 ->
-    specification_of_number_of_leaves number_of_leaves2 ->
-    forall (V : Type)
-           (t : binary_tree V),
-      number_of_leaves1 V t = number_of_leaves2 V t.
-Proof.
-Abort.
-
-(* ***** *)
-
-Definition specification_of_number_of_nodes (number_of_nodes : forall V : Type, binary_tree V -> nat) : Prop :=
-  (forall (V : Type)
-          (v : V),
-      number_of_nodes V (Leaf V v) =
-      0)
-  /\
-  (forall (V : Type)
-          (t1 t2 : binary_tree V),
-      number_of_nodes V (Node V t1 t2) =
-      S (number_of_nodes V t1 + number_of_nodes V t2)).
-
-(* ***** *)
-
 (* Exercise 09c *)
 
-Proposition there_is_at_most_one_number_of_nodes_function :
-  forall number_of_nodes1 number_of_nodes2 : forall V : Type, binary_tree V -> nat,
-    specification_of_number_of_nodes number_of_nodes1 ->
-    specification_of_number_of_nodes number_of_nodes2 ->
-    forall (V : Type)
-           (t : binary_tree V),
-      number_of_nodes1 V t = number_of_nodes2 V t.
-Proof.
-Abort.
-
-(* ***** *)
-
 Theorem about_the_relative_number_of_leaves_and_nodes_in_a_tree :
   forall number_of_leaves : forall V : Type, binary_tree V -> nat,
     specification_of_number_of_leaves number_of_leaves ->