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 cc5b715..4f13107 100644
--- a/cs3234/labs/week-03_structural-induction-over-binary-trees.v
+++ b/cs3234/labs/week-03_structural-induction-over-binary-trees.v
@@ -197,24 +197,11 @@ Proof.
   - rewrite <- M_t_t'.
     rewrite ->  (mirror_is_involutory mirror S_mirror V t).
     reflexivity.
-  - rewrite -> (S_Node V t1 t2).
-    Check (mirror_is_involutory mirror S_mirror V t1).
-    (* TODO: Figure this out *)
+  - rewrite <- M_t_t'.
+    rewrite -> (mirror_is_involutory mirror S_mirror V t).
+    reflexivity.
 
-    Abort.
-
-
-
-
-
-Proposition mirror_reverses_itself :
-  forall mirror : forall V : Type, binary_tree V -> binary_tree V,
-    specification_of_mirror mirror ->
-    forall (V : Type)
-           (t t' : binary_tree V),
-      mirror V t = t' ->
-      mirror V t' = t.
-Proof.
+  Restart.
   intros mirror S_mirror V t t' M_t_t'.
 
   assert (f_equal :