diff --git a/cs3234/labs/midterm-project.v b/cs3234/labs/midterm-project.v
index 6856fdc..ef3587d 100644
--- a/cs3234/labs/midterm-project.v
+++ b/cs3234/labs/midterm-project.v
@@ -527,6 +527,8 @@ Fixpoint list_append (V : Type) (v1s v2s : list V) : list V :=
       v1 :: list_append V v1s' v2s
   end.
 
+Compute test_list_append list_append.
+
 (*
    c. State its associated fold-unfold lemmas.
 *)
@@ -552,7 +554,7 @@ Qed.
    d. Prove that your implementation satisfies the specification.
 *)
 
-Theorem list_append_astisfies_the_specification_of_list_append :
+Theorem list_append_satisfies_the_specification_of_list_append :
   specification_of_list_append list_append.
 Proof.
   unfold specification_of_list_append.
@@ -562,6 +564,27 @@ Proof.
   - intros V v1 v1s' v2s.
     exact (fold_unfold_list_append_cons V v1 v1s' v2s).
 Qed.
+
+Theorem there_is_at_most_one_list_append_function :
+  forall (V : Type)
+    (f g : (forall V : Type, list V -> list V -> list V)),
+    specification_of_list_append f ->
+    specification_of_list_append g ->
+    forall (v1s v2s : list V),
+      f V v1s v2s = g V v1s v2s.
+Proof.
+  unfold specification_of_list_append.
+  intros V f g [S_f_nil S_f_cons] [S_g_nil S_g_cons] v1s v2s.
+  induction v1s as [ | v1 v1s' IHv1s' ].
+  - rewrite -> (S_f_nil V v2s).
+    rewrite -> (S_g_nil V v2s).
+    reflexivity.
+  - rewrite -> (S_f_cons V v1 v1s').
+    rewrite -> IHv1s'.
+    rewrite -> (S_g_cons V v1 v1s').
+    reflexivity.
+Qed.
+
 (*
    e. Prove whether nil is neutral on the left of list_append.
 *)
@@ -695,52 +718,225 @@ Definition specification_of_list_reverse (reverse : forall V : Type, list V -> l
    a. Define a unit-test function for an implementation of the reverse function.
 *)
 
+Definition test_list_reverse (candidate : forall V : Type,  list V -> list V) :=
+  (eqb_list nat Nat.eqb (candidate nat nil) nil) &&
+  (eqb_list bool Bool.eqb (candidate bool nil) nil) &&
+  (eqb_list nat Nat.eqb (candidate nat (1 :: nil) ) (1 :: nil)) &&
+  (eqb_list bool Bool.eqb (candidate bool (true :: nil)) (true :: nil)) &&
+  (eqb_list nat Nat.eqb (candidate nat (4 :: 3 :: nil)) (3 :: 4 :: nil)) &&
+  (eqb_list bool Bool.eqb (candidate bool (true :: false :: nil)) (false :: true  :: nil)).
+
 (*
    b. Implement the reverse function recursively, using list_append.
 *)
 
-(*
-Fixpoint list_reverse (V : Type) (vs : list V) : list V :=
-...
-*)
 
+Fixpoint list_reverse (V : Type) (vs : list V) : list V :=
+  match vs with
+  | nil => nil
+  | v :: vs' => list_append V (list_reverse V vs') (v :: nil)
+  end.
+
+Compute test_list_reverse list_reverse.
 (*
    c. State the associated fold-unfold lemmas.
 *)
 
+Lemma fold_unfold_list_reverse_nil :
+  forall (V : Type),
+    list_reverse V nil = nil.
+Proof.
+  fold_unfold_tactic list_reverse.
+Qed.
+
+Lemma fold_unfold_list_reverse_cons :
+  forall (V : Type)
+    (v : V)
+    (vs : list V),
+    list_reverse V (v :: vs) = list_append V (list_reverse V vs) (v :: nil).
+Proof.
+  fold_unfold_tactic list_reverse.
+Qed.
+
 (*
    d. Prove whether your implementation satisfies the specification.
 *)
-
+Theorem list_reverse_satisfies_the_specification_of_list_reverse :
+  specification_of_list_reverse list_reverse.
+Proof.
+  unfold specification_of_list_reverse.
+  intros append S_append.
+  split.
+  - intro V.
+    exact (fold_unfold_list_reverse_nil V).
+  - intros V v vs'.
+    rewrite -> (fold_unfold_list_reverse_cons V v vs').
+    exact (there_is_at_most_one_list_append_function
+             V list_append append
+             list_append_satisfies_the_specification_of_list_append S_append
+             (list_reverse V vs') (v :: nil)).
+Qed.
 (*
    e. Prove whether list_reverse is involutory.
 *)
 
-(*
+Theorem about_list_reverse_and_list_append :
+  forall (V : Type)
+    (v : V)
+    (vs : list V),
+    list_reverse V (list_append V vs (v :: nil)) = v :: (list_reverse V vs).
+Proof.
+  intros V v vs.
+  induction vs as [ | v' vs' IHvs' ].
+  - rewrite -> (fold_unfold_list_append_nil V (v :: nil)).
+    rewrite -> (fold_unfold_list_reverse_cons V v nil).
+    rewrite -> (fold_unfold_list_reverse_nil V).
+    rewrite -> (fold_unfold_list_append_nil V (v :: nil)).
+    reflexivity.
+  - rewrite -> (fold_unfold_list_append_cons V v' vs' (v :: nil)).
+    rewrite -> (fold_unfold_list_reverse_cons V v' (list_append V vs' (v :: nil))).
+    rewrite -> (IHvs').
+    rewrite -> (fold_unfold_list_append_cons V v (list_reverse V vs') (v' :: nil)).
+    rewrite -> (fold_unfold_list_reverse_cons).
+    reflexivity.
+Qed.
+
 Proposition list_reverse_is_involutory :
   forall (V : Type)
          (vs : list V),
     list_reverse V (list_reverse V vs) = vs.
 Proof.
-Abort.
-*)
+  intros V vs.
+  induction vs as [ | v vs' IHvs' ].
+  - rewrite -> (fold_unfold_list_reverse_nil V).
+    exact (fold_unfold_list_reverse_nil V).
+  - rewrite -> (fold_unfold_list_reverse_cons V v vs').
+    rewrite -> (about_list_reverse_and_list_append V v (list_reverse V vs')).
+    rewrite -> (IHvs').
+    reflexivity.
+Qed.
 
 (*
    f. Prove whether reversing a list preserves its length.
 *)
 
+Theorem reversing_a_list_preserves_its_length :
+  forall (V : Type)
+    (vs : list V),
+    list_length V (list_reverse V vs) = list_length V vs.
+Proof.
+  intros V vs.
+  induction vs as [ | v vs' IHvs' ].
+  - rewrite -> (fold_unfold_list_reverse_nil V).
+    reflexivity.
+  - rewrite -> (fold_unfold_list_reverse_cons V v vs').
+    Search list_length.
+    rewrite -> (list_append_and_list_length_commute_with_each_other V
+      (list_reverse V vs')
+      (v :: nil)).
+    rewrite -> IHvs'.
+    rewrite -> (fold_unfold_list_length_cons V v nil).
+    rewrite -> (fold_unfold_list_length_nil V).
+    rewrite -> (fold_unfold_list_length_cons V v vs').
+    Search (_ + 1).
+    rewrite -> (Nat.add_1_r (list_length V vs')).
+    reflexivity.
+Qed.
 (*
    g. Do list_append and list_reverse commute with each other (hint: yes they do) and if so how?
-*)
+j*)
+
+Theorem list_append_and_list_reverse_commute_with_each_other :
+  forall (V : Type)
+    (v1s v2s : list V),
+    list_append V (list_reverse V v2s) (list_reverse V v1s) = list_reverse V (list_append V v1s v2s).
+Proof.
+  intros V v1s.
+  induction v1s as [ | v1 v1s' IHv1s' ]; intro v2s.
+  - rewrite -> (fold_unfold_list_reverse_nil V).
+    rewrite -> (nil_is_neutral_on_the_right_of_list_append V (list_reverse V v2s)).
+    rewrite -> (fold_unfold_list_append_nil V v2s).
+    reflexivity.
+  - rewrite -> (fold_unfold_list_reverse_cons V v1 v1s').
+    rewrite <- (list_append_is_associative V (list_reverse V v2s) (list_reverse V v1s') (v1 :: nil)).
+    rewrite -> (IHv1s' v2s).
+    rewrite -> (fold_unfold_list_append_cons V v1 v1s' v2s).
+    rewrite -> (fold_unfold_list_reverse_cons V v1 (list_append V v1s' v2s)).
+    reflexivity.
+Qed.
 
 (*
    h. Implement the reverse function using an accumulator instead of using list_append.
 *)
 
-(*
+Fixpoint list_reverse_acc (V : Type) (vs : list V) (acc : list V) : list V :=
+  match vs with
+  | nil => acc
+  | v :: vs' => list_reverse_acc V vs' (v :: acc)
+  end.
+
+
 Definition list_reverse_alt (V : Type) (vs : list V) : list V :=
-...
-*)
+  list_reverse_acc V vs nil.
+
+Lemma fold_unfold_list_reverse_acc_nil :
+  forall (V : Type)
+    (acc : list V),
+    list_reverse_acc V nil acc = acc.
+Proof.
+  fold_unfold_tactic list_reverse_acc.
+Qed.
+
+Lemma fold_unfold_list_reverse_acc_cons :
+  forall (V : Type)
+    (v : V)
+    (vs acc : list V),
+    list_reverse_acc V (v :: vs) acc = list_reverse_acc V vs (v :: acc).
+Proof.
+  fold_unfold_tactic list_reverse_acc.
+Qed.
+
+Compute test_list_reverse list_reverse_alt.
+
+Lemma about_list_reverse_acc :
+  forall (V : Type)
+    (vs acc : list V),
+    list_reverse_acc V vs acc = list_append V (list_reverse_acc V vs nil) acc.
+Proof.
+  intros V vs.
+  induction vs as [ | v vs' IHvs' ]; intro acc.
+  - rewrite -> (fold_unfold_list_reverse_acc_nil V acc).
+    rewrite -> (fold_unfold_list_reverse_acc_nil V nil).
+    rewrite -> (nil_is_neutral_on_the_left_of_list_append V acc).
+    reflexivity.
+  - rewrite -> (fold_unfold_list_reverse_acc_cons V v vs' acc).
+    rewrite -> (IHvs' (v :: acc)).
+    rewrite -> (fold_unfold_list_reverse_acc_cons V v vs' nil).
+    rewrite -> (IHvs' (v :: nil)).
+    rewrite -> (list_append_is_associative V (list_reverse_acc V vs' nil) (v :: nil) acc).
+    rewrite -> (fold_unfold_list_append_cons V v nil acc).
+    rewrite -> (fold_unfold_list_append_nil V acc).
+    reflexivity.
+Qed.
+
+Theorem list_reverse_alt_satisfies_the_specification_of_list_reverse :
+  specification_of_list_reverse list_reverse_alt.
+Proof.
+  unfold specification_of_list_reverse, list_reverse_alt.
+  intros append S_append.
+  split.
+  - intro V.
+    exact (fold_unfold_list_reverse_acc_nil V nil).
+  - intros V v vs'.
+    rewrite -> (fold_unfold_list_reverse_acc_cons V v vs' nil).
+    rewrite -> (there_is_at_most_one_list_append_function V
+                 append list_append
+                 S_append list_append_satisfies_the_specification_of_list_append
+                 (list_reverse_acc V vs' nil)
+                 (v :: nil)
+      ).
+    exact (about_list_reverse_acc V vs' (v ::nil)).
+Qed.
 
 (*
    i. Revisit the propositions above (involution, preservation of length, commutation with append)
@@ -751,6 +947,100 @@ Definition list_reverse_alt (V : Type) (vs : list V) : list V :=
       This subtask is very instructive, but optional.
 *)
 
+Theorem about_list_reverse_acc_and_cons :
+  forall (V : Type)
+    (v : V)
+    (vs acc : list V),
+    list_reverse_acc V (list_append V vs (v :: nil)) acc = v :: list_reverse_acc V vs acc.
+Proof.
+  intros V v vs.
+  induction vs as [ | v' vs' IHvs' ]; intros acc.
+  - rewrite -> (fold_unfold_list_append_nil V (v :: nil)).
+    rewrite -> (fold_unfold_list_reverse_acc_cons V v nil acc).
+    rewrite -> (fold_unfold_list_reverse_acc_nil V (v :: acc)).
+    rewrite -> (fold_unfold_list_reverse_acc_nil V acc).
+    reflexivity.
+  - rewrite -> (fold_unfold_list_append_cons V v' vs' (v :: nil)).
+    rewrite -> (fold_unfold_list_reverse_acc_cons V v' (list_append V vs' (v :: nil)) acc).
+    rewrite -> (IHvs' (v' :: acc)).
+    rewrite -> (fold_unfold_list_reverse_acc_cons V v' vs' acc).
+    reflexivity.
+Qed.
+
+Theorem list_append_and_list_reverse_acc_commute_with_each_other :
+  forall (V : Type)
+    (v1s v2s : list V),
+    list_append V (list_reverse_acc V v2s nil) (list_reverse_acc V v1s nil) = list_reverse_acc V (list_append V v1s v2s) nil.
+Proof.
+  intros V v1s.
+  induction v1s as [ | v1 v1s' IHv1s' ]; intros v2s.
+  - rewrite -> (fold_unfold_list_reverse_acc_nil V nil).
+    rewrite -> (fold_unfold_list_append_nil V v2s).
+    rewrite -> (nil_is_neutral_on_the_right_of_list_append V (list_reverse_acc V v2s nil)).
+    reflexivity.
+  - rewrite -> (fold_unfold_list_reverse_acc_cons V v1 v1s' nil).
+    rewrite -> (fold_unfold_list_append_cons V v1 v1s' v2s).
+    rewrite -> (fold_unfold_list_reverse_acc_cons V v1 (list_append V v1s' v2s) nil).
+    rewrite -> (about_list_reverse_acc V (list_append V v1s' v2s) (v1 :: nil)).
+    rewrite <- (IHv1s' v2s).
+    rewrite -> (list_append_is_associative V (list_reverse_acc V v2s nil) (list_reverse_acc V v1s' nil) (v1 :: nil)).
+    rewrite <- (about_list_reverse_acc V v1s' (v1 :: nil)).
+    reflexivity.
+Qed.
+
+Proposition list_reverse_alt_is_involutory :
+  forall (V : Type)
+         (vs : list V),
+    list_reverse_alt V (list_reverse_alt V vs) = vs.
+Proof.
+  intros V vs.
+  unfold list_reverse_alt.
+  induction vs as [ | v vs' IHvs' ].
+  - rewrite -> (fold_unfold_list_reverse_acc_nil V).
+    reflexivity.
+  - rewrite -> (fold_unfold_list_reverse_acc_cons V v vs' nil).
+    rewrite -> (about_list_reverse_acc V vs' (v :: nil)).
+    rewrite <- (list_append_and_list_reverse_acc_commute_with_each_other V (list_reverse_acc V vs' nil) (v :: nil)).
+    rewrite -> (fold_unfold_list_reverse_acc_cons V v nil nil).
+    rewrite -> (fold_unfold_list_reverse_acc_nil V (v::nil)).
+    rewrite -> IHvs'.
+    rewrite -> (fold_unfold_list_append_cons V v nil vs').
+    rewrite -> (fold_unfold_list_append_nil V vs').
+    reflexivity.
+  Restart.
+  intros V vs.
+  unfold list_reverse_alt.
+  induction vs as [ | v vs' IHvs' ].
+  - rewrite -> (fold_unfold_list_reverse_acc_nil V).
+    reflexivity.
+  - rewrite -> (fold_unfold_list_reverse_acc_cons V v vs' nil).
+    rewrite -> (about_list_reverse_acc V vs' (v :: nil)).
+    rewrite -> (about_list_reverse_acc_and_cons V v (list_reverse_acc V vs' nil) nil).
+    rewrite -> IHvs'.
+    reflexivity.
+Qed.
+
+Theorem list_reverse_alt_and_list_length_commute_with_each_other :
+  forall (V : Type)
+    (vs : list V),
+    list_length V (list_reverse_alt V vs) = list_length V vs.
+Proof.
+  intros V vs.
+  unfold list_reverse_alt.
+  induction vs as [ | v vs' IHvs' ].
+  - rewrite -> (fold_unfold_list_reverse_acc_nil V nil).
+    reflexivity.
+  - rewrite -> (fold_unfold_list_reverse_acc_cons V v vs' nil).
+    rewrite -> (about_list_reverse_acc V vs' (v :: nil)).
+    Search list_length.
+    rewrite -> (list_append_and_list_length_commute_with_each_other V (list_reverse_acc V vs' nil) (v :: nil)).
+    rewrite -> IHvs'.
+    rewrite -> (fold_unfold_list_length_cons V v nil).
+    rewrite -> (fold_unfold_list_length_nil V).
+    rewrite -> (fold_unfold_list_length_cons V v vs').
+    rewrite -> (Nat.add_1_r (list_length V vs')).
+    reflexivity.
+Qed.
 (* ********** *)
 
 (* A study of the polymorphic map function: *)
@@ -849,31 +1139,128 @@ Qed.
    e. Implement the copy function as an instance of list_map.
 *)
 
-(*
+
 Definition list_copy_as_list_map (V : Type) (vs : list V) : list V :=
-  ...
-*)
+  list_map V V (fun i => i) vs.
+
+Compute test_list_copy list_copy_as_list_map.
+
 
 (*
 Hint: Does list_copy_as_list_map satisfy the specification of list_copy?
 *)
 
+Theorem list_copy_as_list_map_satisfies_the_specification_of_list_copy :
+  specification_of_list_copy list_copy_as_list_map.
+Proof.
+  unfold specification_of_list_copy, list_copy_as_list_map.
+  split.
+  - intros V.
+    exact (fold_unfold_list_map_nil V V (fun i => i)).
+  - intros V v vs'.
+    rewrite -> (fold_unfold_list_map_cons V V (fun i => i) v vs').
+    reflexivity.
+  Qed.
 (*
    f. Prove whether mapping a function over a list preserves the length of this list.
 *)
+Theorem list_map_and_list_length_commute_with_each_other :
+  forall (V W : Type)
+    (f : V -> W)
+    (vs : list V),
+    list_length W (list_map V W f vs) = list_length V vs.
+Proof.
+  intros V W f vs.
+  induction vs as [ | v vs' IHvs' ].
+  - rewrite -> (fold_unfold_list_map_nil V W f).
+    rewrite -> (fold_unfold_list_length_nil W).
+    rewrite -> (fold_unfold_list_length_nil V).
+    reflexivity.
+  - rewrite -> (fold_unfold_list_map_cons V W f v vs').
+    rewrite -> (fold_unfold_list_length_cons W (f v) (list_map V W f vs')).
+    rewrite -> IHvs'.
+    rewrite -> (fold_unfold_list_length_cons V v vs').
+    reflexivity.
+Qed.
 
 (*
    g. Do list_map and list_append commute with each other and if so how?
 *)
+Theorem list_map_and_list_append_commute_with_each_other :
+  forall (V W : Type)
+    (f : V -> W)
+    (v1s v2s : list V),
+    list_append W (list_map V W f v1s) (list_map V W f v2s) = list_map V W f (list_append V v1s v2s).
+Proof.
+  intros V W f v1s v2s.
+  induction v1s as [ | v1 v1s' IHv1s' ].
+  - rewrite (fold_unfold_list_map_nil V W f).
+    rewrite -> (nil_is_neutral_on_the_left_of_list_append W (list_map V W f v2s)).
+    rewrite -> (nil_is_neutral_on_the_left_of_list_append V v2s).
+    reflexivity.
+  - rewrite -> (fold_unfold_list_map_cons V W f v1 v1s').
+    rewrite -> (fold_unfold_list_append_cons W (f v1) (list_map V W f v1s') (list_map V W f v2s)).
+    rewrite -> IHv1s'.
+    rewrite -> (fold_unfold_list_append_cons V v1 v1s' v2s).
+    rewrite -> (fold_unfold_list_map_cons V W f v1 (list_append V v1s' v2s)).
+    reflexivity.
+Qed.
 
 (*
    h. Do list_map and list_reverse commute with each other and if so how?
 *)
+Theorem list_map_and_list_reverse_commute_with_each_other :
+  forall (V W : Type)
+    (f : V -> W)
+    (vs : list V),
+    list_reverse W (list_map V W f vs) = list_map V W f (list_reverse V vs).
+Proof.
+  intros V W f vs.
+  induction vs as [ | v vs' IHvs' ].
+  - rewrite -> (fold_unfold_list_map_nil V W f).
+    rewrite -> (fold_unfold_list_reverse_nil W).
+    rewrite -> (fold_unfold_list_reverse_nil V).
+    rewrite -> (fold_unfold_list_map_nil V W f).
+    reflexivity.
+  - rewrite -> (fold_unfold_list_map_cons V W f v vs').
+    rewrite -> (fold_unfold_list_reverse_cons W (f v) (list_map V W f vs')).
+    rewrite -> (fold_unfold_list_reverse_cons V v vs').
+    rewrite -> IHvs'.
+    Search list_reverse.
+    rewrite <- (list_map_and_list_append_commute_with_each_other V W f (list_reverse V vs') (v :: nil)).
+    rewrite -> (fold_unfold_list_map_cons V W f v nil).
+    rewrite -> (fold_unfold_list_map_nil V W f).
+    reflexivity.
+Qed.
 
 (*
    i. Do list_map and list_reverse_alt commute with each other and if so how?
 *)
-
+Theorem list_map_and_list_reverse_alt_commute_with_each_other :
+  forall (V W : Type)
+    (f : V -> W)
+    (vs : list V),
+    list_reverse_alt W (list_map V W f vs) = list_map V W f (list_reverse_alt V vs).
+Proof.
+  intros V W f vs.
+  unfold list_reverse_alt.
+  induction vs as [ | v vs' IHvs' ].
+  - rewrite -> (fold_unfold_list_map_nil V W f).
+    rewrite -> (fold_unfold_list_reverse_acc_nil W nil).
+    rewrite -> (fold_unfold_list_reverse_acc_nil V nil).
+    rewrite -> (fold_unfold_list_map_nil V W f).
+    reflexivity.
+  - rewrite -> (fold_unfold_list_map_cons V W f v vs').
+    rewrite -> (fold_unfold_list_reverse_acc_cons W (f v) (list_map V W f vs')).
+    rewrite -> (fold_unfold_list_reverse_acc_cons V v vs' nil).
+    rewrite -> (about_list_reverse_acc V vs' (v :: nil)).
+    rewrite <- (list_map_and_list_append_commute_with_each_other V W f (list_reverse_acc V vs' nil) (v::nil)).
+    rewrite -> (fold_unfold_list_map_cons V W f v nil).
+    rewrite -> (fold_unfold_list_map_nil V W f).
+    rewrite <- IHvs'.
+    rewrite <- (about_list_reverse_acc W (list_map V W f vs') (f v :: nil)).
+    reflexivity.
+  Qed.
 (*
    j. Define a unit-test function for the map function
       and verify that your implementation satisfies it.