diff --git a/ModelChecking.v b/ModelChecking.v
index 5c1f099..23ee33d 100644
--- a/ModelChecking.v
+++ b/ModelChecking.v
@@ -3,6 +3,8 @@
   * Author: Adam Chlipala
   * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *)
 
+Set Warnings "-notation-overridden". (* <-- needed while we play with defining one
+                                      * of the book's notations ourselves locally *)
 Require Import Frap TransitionSystems.
 
 Set Implicit Arguments.
diff --git a/ModelChecking_template.v b/ModelChecking_template.v
index c062866..1bb3dc5 100644
--- a/ModelChecking_template.v
+++ b/ModelChecking_template.v
@@ -3,6 +3,8 @@
   * Author: Adam Chlipala
   * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *)
 
+Set Warnings "-notation-overridden". (* <-- needed while we play with defining one
+                                      * of the book's notations ourselves locally *)
 Require Import Frap TransitionSystems.
 
 Set Implicit Arguments.
@@ -175,28 +177,64 @@ Qed.
 Theorem factorial_ok_2 :
   invariantFor (factorial_sys 2) (fact_correct 2).
 Proof.
-Admitted.
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+  simplify.
+  eapply invariant_weaken.
 
+  apply multiStepClosure_ok.
+  simplify.
+  rewrite fact_init_is.
 
+  eapply MscStep.
+  apply oneStepClosure_split.
+  simplify.
+  invert H.
+  simplify.
+  apply singleton_in.
+  apply oneStepClosure_empty.
+  simplify.
 
+  eapply MscStep.
+  apply oneStepClosure_split.
+  simplify.
+  invert H.
+  simplify.
+  apply singleton_in.
+  apply oneStepClosure_split.
+  simplify.
+  invert H.
+  simplify.
+  apply singleton_in.
+  apply oneStepClosure_empty.
+  simplify.
 
+  eapply MscStep.
+  apply oneStepClosure_split.
+  simplify.
+  invert H.
+  simplify.
+  apply singleton_in.
+  apply oneStepClosure_split.
+  simplify.
+  invert H.
+  simplify.
+  apply singleton_in.
+  apply oneStepClosure_split.
+  simplify.
+  invert H.
+  simplify.
+  apply singleton_in.
+  apply oneStepClosure_empty.
+  simplify.
 
+  apply MscDone.
+  apply prove_oneStepClosure; simplify.
+  assumption.
+  propositional; subst; invert H0; simplify; propositional.
 
+  simplify.
+  unfold fact_correct.
+  propositional; subst; trivial.
+Qed.
 
 (* BEGIN CODE THAT WILL NOT BE EXPLAINED IN DETAIL! *)
 
@@ -404,25 +442,10 @@ Proof.
   assumption.
 Qed.
 
-Theorem add2_ok :
+(*Theorem add2_ok :
   invariantFor add2_sys add2_correct.
 Proof.
-Admitted.
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+Admitted.*)
 
 Inductive add2_bthread :=
 | BRead
@@ -488,7 +511,7 @@ Qed.
 Hint Rewrite add2_init_is.
 
 (* Now, let's verify the original system. *)
-(*Theorem add2_ok :
+Theorem add2_ok :
   invariantFor add2_sys add2_correct.
 Proof.
   (* First step: strengthen the invariant.  We leave an underscore for the
@@ -597,7 +620,7 @@ Proof.
 
   invert H1.
   propositional.
-Qed.*)
+Qed.
 
 
 (** * Another abstraction example *)
@@ -1373,35 +1396,17 @@ Qed.
 Theorem twoadd2_ok :
   invariantFor (parallel twoadd_sys twoadd_sys) (twoadd_correct (private := _)).
 Proof.
-Admitted.
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+  eapply invariant_weaken.
+  eapply invariant_simulates.
+  apply withInterference_abstracts.
+  apply withInterference_parallel.
+  apply twoadd_ok.
+  apply twoadd_ok.
+  
+  unfold twoadd_correct.
+  invert 1.
+  assumption.
+Qed.
 
 (* In fact, this modularity technique is so powerful that we now get correctness
  * for any number of threads, "for free"!  Here's a tactic definition, which we
diff --git a/TransitionSystems.v b/TransitionSystems.v
index eb50cb6..8fee239 100644
--- a/TransitionSystems.v
+++ b/TransitionSystems.v
@@ -85,6 +85,8 @@ Proof.
 Qed.
 
 (* Transitive-reflexive closure is so common that it deserves a shorthand notation! *)
+Set Warnings "-notation-overridden". (* <-- needed while we play with defining one
+                                      * of the book's notations ourselves locally *)
 Notation "R ^*" := (trc R) (at level 0).
 
 (* Now let's use it to execute the factorial program. *)
diff --git a/TransitionSystems_template.v b/TransitionSystems_template.v
index ba426e5..2661e28 100644
--- a/TransitionSystems_template.v
+++ b/TransitionSystems_template.v
@@ -50,6 +50,8 @@ Inductive trc {A} (R : A -> A -> Prop) : A -> A -> Prop :=
   -> trc R x z.
 
 (* Transitive-reflexive closure is so common that it deserves a shorthand notation! *)
+Set Warnings "-notation-overridden". (* <-- needed while we play with defining one
+                                      * of the book's notations ourselves locally *)
 Notation "R ^*" := (trc R) (at level 0).
 
 (* Now let's use it to execute the factorial program. *)