diff --git a/Tactics.v b/Tactics.v
index 4718d30..3a20d0b 100644
--- a/Tactics.v
+++ b/Tactics.v
@@ -77,7 +77,26 @@ Theorem silly_ex : forall p,
   even p = true ->
   odd (S p) = true.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros p HevenS Hodd Heven.
+  apply Hodd.
+  apply HevenS.
+  apply Heven.
+Qed.
+
+Theorem silly_ex' : forall p,
+  (forall n, even n = true -> even (S n) = false) ->
+  (forall n, even n = false -> odd n = true) ->
+  even p = true ->
+  odd (S p) = true.
+Proof.
+  intros p HevenS Hodd Heven.
+  rewrite -> Hodd.
+  reflexivity.
+  rewrite -> HevenS.
+  reflexivity.
+  rewrite -> Heven.
+  reflexivity.
+Qed.
 (** [] *)
 
 (** To use the [apply] tactic, the (conclusion of the) fact
@@ -108,11 +127,17 @@ Proof.
     that theorem as part of your (relatively short) solution to this
     exercise. You do not need [induction]. *)
 
+Search (rev ?l).
+
 Theorem rev_exercise1 : forall (l l' : list nat),
   l = rev l' ->
   l' = rev l.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros l l' H.
+  rewrite H.
+  symmetry.
+  apply rev_involutive.
+Qed.
 (** [] *)
 
 (** **** Exercise: 1 star, standard, optional (apply_rewrite)
@@ -195,7 +220,11 @@ Example trans_eq_exercise : forall (n m o p : nat),
      (n + p) = m ->
      (n + p) = (minustwo o).
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros n m o p eq1 eq2.
+  transitivity m.
+  apply eq2.
+  apply eq1.
+Qed.
 (** [] *)
 
 (* ################################################################# *)
@@ -286,7 +315,14 @@ Example injection_ex3 : forall (X : Type) (x y z : X) (l j : list X),
   j = z :: l ->
   x = y.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros X x y z l j H1 H2.
+  injection H1 as H3 H4.
+  rewrite H3.
+  rewrite <- H4 in H2.
+  injection H2 as H5.
+  symmetry.
+  apply H5.
+Qed.
 (** [] *)
 
 (** So much for injectivity of constructors.  What about disjointness? *)
@@ -335,7 +371,9 @@ Example discriminate_ex3 :
     x :: y :: l = [] ->
     x = z.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros X x y z l j H.
+  discriminate H.
+Qed.
 (** [] *)
 
 (** For a more useful example, we can use [discriminate] to make a
@@ -469,13 +507,20 @@ Proof.
 
 (** **** Exercise: 3 stars, standard (nth_error_always_none) *)
 
+Search nth_error.
+
 (** Use [specialize] to prove the the following lemma, following the
     model of [specialize_example] above. Do not use [induction]. *)
 Lemma nth_error_always_none: forall (l : list nat),
   (forall i, nth_error l i = None) ->
   l = [].
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros l H.
+  specialize H with (i := 0).
+  destruct l.
+  - reflexivity.
+  - discriminate.
+Qed.
 (** [] *)
 
 (** Using [specialize] before [apply] gives us yet another way to
@@ -654,7 +699,20 @@ Proof.
 Theorem eqb_true : forall n m,
   n =? m = true -> n = m.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros n.
+  induction n as [| n' IHn].
+  - intros m H.
+    destruct m as [| m'] eqn:E.
+    + reflexivity.
+    + discriminate.
+  - intros m H.
+    destruct m as [| m'] eqn:E.
+    + discriminate.
+    + f_equal.
+      apply IHn.
+      simpl in H.
+      apply H.
+Qed.
 (** [] *)
 
 (** **** Exercise: 2 stars, advanced, optional (eqb_true_informal)
@@ -663,6 +721,34 @@ Proof.
     hypothesis explicitly and being as explicit as possible about
     quantifiers, everywhere. *)
 
+(* Theorem: for all n m : nat, n =? m = true -> n = m.
+
+  Proof: by induction on n.
+
+  First, consider the base case where n = 0.
+
+  Let's consider the case where m = 0. Then we can substitute (n =? m)
+  into (0 =? 0), which is always true.
+
+  Next, lets consider the case where m = S m' for some nat m'. Then the premise
+  become (0 =? S m'), which is a contradiction.
+
+  Now we consider the inductive case where n = S n' for some natural number  n'.
+  We have the following induction hypothesis:
+
+    forall m, (n =? m) = true -> n = m.
+
+  And we need to show that S n' = m.
+
+  Clearly, m can not be 0, as this would be a contradiction. Lets consider the case
+  where m = S m' for some natural number m'. We can now infer that
+
+    S n' = S m' -> n' = m'
+
+  Using the induction hypothesis, we know that this is the case if (n' =? m') is true,
+  which is immediate from the premise of the theorem. Qed.
+*)
+
 (* FILL IN HERE *)
 
 (* Do not modify the following line: *)
@@ -677,7 +763,22 @@ Theorem plus_n_n_injective : forall n m,
   n + n = m + m ->
   n = m.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros n.
+  induction n.
+  - intros m H.
+    destruct m.
+    + reflexivity.
+    + discriminate.
+  - intros m H.
+    destruct m.
+    + discriminate.
+    + f_equal.
+      simpl in H.
+      rewrite <- plus_n_Sm in H.
+      rewrite <- plus_n_Sm in H.
+      injection H.
+      apply IHn.
+Qed.
 (** [] *)
 
 (** The strategy of doing fewer [intros] before an [induction] to
@@ -827,7 +928,20 @@ Theorem nth_error_after_last: forall (n : nat) (X : Type) (l : list X),
   length l = n ->
   nth_error l n = None.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros n X l.
+  generalize dependent n.
+  induction l.
+  - intros n H.
+    reflexivity.
+  - intros n H.
+    simpl in H.
+    destruct n as [| n'] eqn:Heq.
+    + discriminate.
+    + simpl.
+      specialize IHl with (n := n').
+      injection H.
+      apply IHl.
+Qed.
 (** [] *)
 
 (* ################################################################# *)
@@ -1015,7 +1129,28 @@ Theorem combine_split : forall X Y (l : list (X * Y)) l1 l2,
   split l = (l1, l2) ->
   combine l1 l2 = l.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros X Y l l1 l2 Hsplit.
+  generalize dependent l2.
+  generalize dependent l1.
+  induction l.
+  - intros l1 l2 Hsplit.
+    simpl in Hsplit.
+    injection Hsplit.
+    intros Hl2 Hl1.
+    rewrite <- Hl2, <- Hl1.
+    reflexivity.
+  - intros l1 l2 Hsplit.
+    destruct x as [x1 x2].
+    simpl in Hsplit.
+    destruct (split l) as [l1' l2'].
+    injection Hsplit.
+    intros Hl2 Hl1.
+    rewrite <- Hl2, <- Hl1.
+    simpl.
+    rewrite IHl.
+    + reflexivity.
+    + reflexivity.
+Qed.
 (** [] *)
 
 (** The [eqn:] part of the [destruct] tactic is optional; although
@@ -1089,7 +1224,23 @@ Theorem bool_fn_applied_thrice :
   forall (f : bool -> bool) (b : bool),
   f (f (f b)) = f b.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros f b.
+  destruct (f b) eqn:Hfb.
+  - destruct b.
+    + rewrite Hfb.
+      rewrite Hfb.
+      reflexivity.
+    + destruct (f true) eqn:Hft.
+      * apply Hft.
+      * apply Hfb.
+  - destruct b.
+    + destruct (f false) eqn:Hff.
+      * apply Hfb.
+      * apply Hff.
+    + rewrite Hfb.
+      rewrite Hfb.
+      reflexivity.
+Qed.
 (** [] *)
 
 (* ################################################################# *)
@@ -1176,7 +1327,17 @@ Proof.
 Theorem eqb_sym : forall (n m : nat),
   (n =? m) = (m =? n).
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros n.
+  induction n as [| n' IHn].
+  - intros m.
+    destruct m.
+    + reflexivity.
+    + reflexivity.
+  - intros m.
+    destruct m.
+    + reflexivity.
+    + apply IHn.
+Qed.
 (** [] *)
 
 (** **** Exercise: 3 stars, advanced, optional (eqb_sym_informal)
@@ -1184,12 +1345,36 @@ Proof.
     Give an informal proof of this lemma that corresponds to your
     formal proof above:
 
-   Theorem: For any [nat]s [n] [m], [(n =? m) = (m =? n)].
+    Theorem: For any [nat]s [n] [m], [(n =? m) = (m =? n)].
 
-   Proof: *)
-   (* FILL IN HERE
+    Proof: by induction on n.
 
-    [] *)
+    First consider the base case where n = 0.
+
+    If m = 0, then
+
+      (n ?= m) = (0 ?= 0) = true = (m ?= n).
+
+    If m = S m' for some natural number m', then
+
+      (n ? m) = (0 ?= S m') = false = (S m' ?= true)
+
+    Now consider the inductive case where n = S n' for some natural number n'.
+    We have the following induction hypothesis:
+
+      forall m, (n' ?= m) = (m ?= n').
+
+    Let's consider the case where m = 0. Then
+
+      (n ?= m) = (S n' ?= 0) = false = (0 ?= S n').
+
+    Now consider the case where m = S m' for some natural number m'.
+    We now need to show that:
+
+      (S n' =? S m) = (S m =? S n')
+
+    Which is immediate from the induction hypothesis. Qed.
+   *)
 
 (** **** Exercise: 3 stars, standard, optional (eqb_trans) *)
 Theorem eqb_trans : forall n m p,
@@ -1197,7 +1382,12 @@ Theorem eqb_trans : forall n m p,
   m =? p = true ->
   n =? p = true.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros n m p Hnm Hmp.
+  apply eqb_true in Hnm.
+  apply eqb_true in Hmp.
+  subst.
+  apply eqb_refl.
+Qed.
 (** [] *)
 
 (** **** Exercise: 3 stars, advanced (split_combine)
@@ -1211,14 +1401,38 @@ Proof.
     Your property will need to account for the behavior of [combine]
     in its base cases, which possibly drop some list elements. *)
 
-Definition split_combine_statement : Prop
-  (* ("[: Prop]" means that we are giving a name to a
-     logical proposition here.) *)
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+Definition split_combine_statement : Prop :=
+  forall (X Y : Type) (l : list (X * Y)) (l1 : list X) (l2 : list Y),
+  length l1 = length l2 ->
+  combine l1 l2 = l ->
+  split l = (l1, l2).
 
 Theorem split_combine : split_combine_statement.
 Proof.
-(* FILL IN HERE *) Admitted.
+  unfold split_combine_statement.
+  intros X Y l.
+  induction l as [| [x y] t IH].
+  - intros l1 l2 Hlen Hcombine.
+    destruct l1 as [| x1 t1] eqn:Hl1.
+    + destruct l2 as [| y1 t2] eqn:Hl2.
+      * simpl. reflexivity.
+      * discriminate.
+    + destruct l2 as [| y1 t2] eqn:Hl2.
+      * discriminate.
+      * discriminate.
+  - intros l1 l2 Hlen Hcombine.
+    destruct l1 as [| x1 t1] eqn:Hl1.
+    + discriminate.
+    + destruct l2 as [| y1 t2] eqn:Hl2.
+      * discriminate.
+      * injection Hlen as Hlen'.
+        injection Hcombine as Hcombine'.
+        specialize (IH t1 t2 Hlen' H0).
+        subst.
+        simpl.
+        rewrite IH.
+        reflexivity.
+Qed.
 
 (* Do not modify the following line: *)
 Definition manual_grade_for_split_combine : option (nat*string) := None.
@@ -1230,7 +1444,24 @@ Theorem filter_exercise : forall (X : Type) (test : X -> bool)
   filter test l = x :: lf ->
   test x = true.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros X test x l lf H.
+  generalize dependent x.
+  induction l as [| x' xs IHf].
+  - intros x H.
+    simpl in H.
+    discriminate H.
+  - intros x H.
+    destruct (test x') eqn:Htst.
+    + unfold filter in H.
+      rewrite Htst in H.
+      injection H as Hx Htail.
+      rewrite Hx in Htst.
+      apply Htst.
+    + apply IHf.
+      unfold filter in H.
+      rewrite Htst in H.
+      apply H.
+Qed.
 (** [] *)
 
 (** **** Exercise: 4 stars, advanced, especially useful (forall_exists_challenge)
@@ -1259,43 +1490,63 @@ Proof.
     [existsb'] and [existsb] have the same behavior.
 *)
 
-Fixpoint forallb {X : Type} (test : X -> bool) (l : list X) : bool
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+Fixpoint forallb {X : Type} (test : X -> bool) (l : list X) : bool :=
+  match l with
+  | nil => true
+  | x :: xs => test x && forallb test xs
+  end.
 
 Example test_forallb_1 : forallb odd [1;3;5;7;9] = true.
-Proof. (* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example test_forallb_2 : forallb negb [false;false] = true.
-Proof. (* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example test_forallb_3 : forallb even [0;2;4;5] = false.
-Proof. (* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example test_forallb_4 : forallb (eqb 5) [] = true.
-Proof. (* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
-Fixpoint existsb {X : Type} (test : X -> bool) (l : list X) : bool
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+Fixpoint existsb {X : Type} (test : X -> bool) (l : list X) : bool :=
+  match l with
+  | nil => false
+  | x :: xs => test x || existsb test xs
+  end.
 
 Example test_existsb_1 : existsb (eqb 5) [0;2;3;6] = false.
-Proof. (* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example test_existsb_2 : existsb (andb true) [true;true;false] = true.
-Proof. (* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example test_existsb_3 : existsb odd [1;0;0;0;0;3] = true.
-Proof. (* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example test_existsb_4 : existsb even [] = false.
-Proof. (* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
-Definition existsb' {X : Type} (test : X -> bool) (l : list X) : bool
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+(* NOTE: A || B || ... is equivalent to ~(~A && ~B && ...) *)
+Definition existsb' {X : Type} (test : X -> bool) (l : list X) : bool :=
+  negb (forallb (fun x => negb (test x)) l).
 
 Theorem existsb_existsb' : forall (X : Type) (test : X -> bool) (l : list X),
   existsb test l = existsb' test l.
-Proof. (* FILL IN HERE *) Admitted.
-
+Proof.
+  intros X test l.
+  induction l as [| b bs IHt].
+  - reflexivity.
+  - simpl.
+    unfold existsb'.
+    destruct (test b) eqn:Htst.
+    + simpl.
+      rewrite Htst.
+      reflexivity.
+    + simpl.
+      rewrite Htst.
+      simpl.
+      apply IHt.
+Qed.
 (** [] *)
 
 (* 2026-01-07 13:17 *)