diff --git a/cs3234/labs/week-05_eqn-and-remember.v b/cs3234/labs/week-05_eqn-and-remember.v
new file mode 100644
index 0000000..fc34dd4
--- /dev/null
+++ b/cs3234/labs/week-05_eqn-and-remember.v
@@ -0,0 +1,35 @@
+(* week-05_eqn-and-remember.v *)
+(* LPP 2024 - CS3234 2023-2024, Sem2 *)
+(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
+(* Version of 16 Feb 2024 *)
+
+(* ********** *)
+
+Lemma O_or_S :
+  forall n : nat,
+    n = 0 \/ exists n' : nat, n = S n'.
+Proof.
+  intro n.
+  case n as [ | n'] eqn:H_n.
+  - left.
+    reflexivity.
+  - right.
+    exists n'.
+    reflexivity.
+Qed.
+
+(* ********** *)
+
+Lemma add_1_r :
+  forall n : nat,
+    n + 1 = S n.
+Proof.
+  intro n.
+  remember (n + 1) as n_plus_1 eqn:H_n_plus_1.
+  remember (S n) as Sn eqn:H_Sn.
+  remember (n_plus_1 = Sn) as prove_me eqn:goal.
+Abort.
+
+(* ********** *)
+
+(* end of week-05_eqn-and-remember.v *)
diff --git a/cs3234/labs/week-05_induction-and-induction-proofs-a-recapitulation.v b/cs3234/labs/week-05_induction-and-induction-proofs-a-recapitulation.v
new file mode 100644
index 0000000..8d74f24
--- /dev/null
+++ b/cs3234/labs/week-05_induction-and-induction-proofs-a-recapitulation.v
@@ -0,0 +1,644 @@
+(* week-05_induction-and-induction-proofs-a-recapitulation.v *)
+(* LPP 2024 - CS3234 2023-2024, Sem2 *)
+(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
+(* Version of 16 Feb 2024 *)
+
+(* ********** *)
+
+(* Paraphernalia: *)
+
+Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.
+
+Require Import Arith Bool.
+
+(* ********** *)
+
+Inductive bool' : Type :=
+  true' : bool'
+| false' : bool'.
+
+(*
+bool' is defined
+bool'_rect is defined
+bool'_ind is defined
+bool'_rec is defined
+*)
+
+Check bool'_ind.
+(* : forall P : bool' -> Prop, P true' -> P false' -> forall b : bool', P b *)
+
+Proposition bool'_identity :
+  forall b : bool',
+    b = b.
+Proof.
+  intro b.
+  reflexivity.
+
+  Restart.
+
+  intro b.
+  case b as [ | ] eqn:H_b.
+  - reflexivity.
+  - reflexivity.
+
+  Restart.
+
+  intros [ | ].
+  - reflexivity.
+  - reflexivity.
+Qed.
+
+(* ********** *)
+
+Inductive nat' : Type :=
+  O'
+| S' : nat' -> nat'.
+
+(*
+nat' is defined
+nat'_rect is defined
+nat'_ind is defined
+nat'_rec is defined
+*)
+
+Check nat'_ind.
+(* : forall P : nat' -> Prop, P O' -> (forall n : nat', P n -> P (S' n)) -> forall n : nat', P n *)
+
+Proposition nat'_identity :
+  forall n : nat',
+    n = n.
+Proof.
+  intro n.
+  reflexivity.
+
+  Restart.
+
+  intro n.
+  case n as [ | n'] eqn:H_n.
+  - reflexivity.
+  - reflexivity.
+
+  Restart.
+
+  intros [ | n'].
+  - reflexivity.
+  - reflexivity.
+
+  Restart.
+
+  intro n.
+  induction n as [ | n' IHn'].
+  - 
+(* The goal is the base case, where "P x" is "x = x", for any x:
+
+  ============================
+  O' = O'
+*)
+    reflexivity.
+  - 
+(*
+  n' : nat
+  IHn' : n' = n'
+  ============================
+  S' n' = S' n'
+*)
+    revert n' IHn'.
+(* The goal is the induction step, where "P x" is "x = x", for any x:
+
+  ============================
+  forall n' : nat', n' = n' -> S' n' = S' n'
+*)
+    intros n' IHn'.
+    reflexivity.
+Qed.
+
+Check nat_ind.
+(* : forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n *)
+
+Proposition nat_identity :
+  forall n : nat,
+    n = n.
+Proof.
+  intro n.
+  induction n as [ | n' IHn'].
+  - 
+(* The goal is the base case, where "P x" is "x = x", for any x:
+
+  ============================
+  0 = 0
+*)
+    reflexivity.
+  - 
+(*
+  n' : nat
+  IHn' : n' = n'
+  ============================
+  S n' = S n'
+*)
+    revert n' IHn'.
+(* The goal is the induction step, where "P x" is "x = x", for any x:
+
+  ============================
+  forall n' : nat, n' = n' -> S n' = S n'
+*)
+    intros n' IHn'.
+    reflexivity.
+Qed.
+
+(* ********** *)
+
+Inductive binary_tree_wpl (V : Type) : Type :=
+  Leaf_wpl : V -> binary_tree_wpl V
+| Node_wpl : binary_tree_wpl V -> binary_tree_wpl V -> binary_tree_wpl V.
+
+(*
+binary_tree_wpl is defined
+binary_tree_wpl_rect is defined
+binary_tree_wpl_ind is defined
+binary_tree_wpl_rec is defined
+*)
+
+Check binary_tree_wpl_ind.
+(* : forall (V : Type)
+            (P : binary_tree_wpl V -> Prop),
+       (forall v : V, P (Leaf_wpl V v)) ->
+       (forall t1 : binary_tree_wpl V, P t1 -> forall t2 : binary_tree_wpl V, P t2 -> P (Node_wpl V t1 t2)) ->
+       forall t : binary_tree_wpl V,
+         P t
+*)
+
+Proposition binary_tree_wpl_identity :
+  forall (V : Type)
+         (t : binary_tree_wpl V),
+    t = t.
+Proof.
+  intros V t.
+  reflexivity.
+
+  Restart.
+
+  intros V t.
+  case t as [v | t1 t2] eqn:H_t.
+  - reflexivity.
+  - reflexivity.
+
+  Restart.
+
+  intros V [v | t1 t2].
+  - reflexivity.
+  - reflexivity.
+
+  Restart.
+
+  induction t as [v | t1 IHt1 t2 IHt2].
+  - revert v.
+(* The goal is the base case, where "P x" is "x = x", for any x:
+
+  V : Type
+  ============================
+  forall v : V, Leaf_wpl V v = Leaf_wpl V v
+*)
+    intro v.
+    reflexivity.
+  - revert t1 IHt1 t2 IHt2.
+(* The goal is the induction step, where "P x" is "x = x", for any x:
+
+  V : Type
+  ============================
+  forall t1 : binary_tree_wpl V, t1 = t1 -> forall t2 : binary_tree_wpl V, t2 = t2 -> Node_wpl V t1 t2 = Node_wpl V t1 t2
+*)
+    intros t1 IHt1 t2 IHt2.
+    reflexivity.
+Qed.
+
+(* ********** *)
+
+Inductive binary_tree_wpn (V : Type) : Type :=
+  Leaf_wpn : binary_tree_wpn V
+| Node_wpn : binary_tree_wpn V -> V -> binary_tree_wpn V -> binary_tree_wpn V.
+
+(*
+binary_tree_wpn is defined
+binary_tree_wpn_rect is defined
+binary_tree_wpn_ind is defined
+binary_tree_wpn_rec is defined
+*)
+
+Check binary_tree_wpn_ind.
+(* : forall (V : Type)
+            (P : binary_tree_wpn V -> Prop),
+       P (Leaf_wpn V) ->
+       (forall t1 : binary_tree_wpn V,
+          P t1 ->
+          forall (v : V)
+                 (t2 : binary_tree_wpn V_,
+            P t2 ->
+            P (Node_wpn V t1 v t2)) ->
+       forall t : binary_tree_wpn V,
+         P t
+*)
+
+Proposition binary_tree_wpn_identity :
+  forall (V : Type)
+         (t : binary_tree_wpn V),
+    t = t.
+Proof.
+  intros V t.
+  reflexivity.
+
+  Restart.
+
+  intros V t.
+  case t as [ | t1 v t2] eqn:H_t.
+  - reflexivity.
+  - reflexivity.
+
+  Restart.
+
+  intros V [ | t1 v t2].
+  - reflexivity.
+  - reflexivity.
+
+  Restart.
+
+  intros V t.
+  induction t as [ | t1 IHt1 v t2 IHt2].
+  - 
+(* The goal is the base case, where "P x" is "x = x", for any x:
+
+  V : Type
+  ============================
+  Leaf_wpn V = Leaf_wpn V
+*)
+    reflexivity.
+  - revert t1 IHt1 v t2 IHt2.
+(* The goal is the induction step, where "P x" is "x = x", for any x:
+
+  V : Type
+  ============================
+  forall t1 : binary_tree_wpn V, t1 = t1 -> forall (v : V) (t2 : binary_tree_wpn V), t2 = t2 -> Node_wpn V t1 v t2 = Node_wpn V t1 v t2
+*)
+    intros t1 IHt1 v t2 IHt2.
+    reflexivity.
+Qed.
+
+(* ********** *)
+
+Inductive tree3 (V : Type) : Type :=
+  Node0 : V -> tree3 V
+| Node1 : tree3 V -> tree3 V
+| Node2 : tree3 V -> tree3 V -> tree3 V
+| Node3 : tree3 V -> tree3 V -> tree3 V -> tree3 V.
+
+Proposition tree3_identity :
+  forall (V : Type)
+         (t : tree3 V),
+    t = t.
+Proof.
+  intros V t.
+  reflexivity.
+
+  Restart.
+
+  intros V t.
+  case t as [v | t1 | t1 t2 | t1 t2 t3] eqn:H_t.
+  - reflexivity.
+  - reflexivity.
+  - reflexivity.
+  - reflexivity.
+
+  Restart.
+
+  intros V [v | t1 | t1 t2 | t1 t2 t3].
+  - reflexivity.
+  - reflexivity.
+  - reflexivity.
+  - reflexivity.
+
+  Restart.
+
+  intros V t.
+  induction t as [v | t1 IHt1 | t1 IHt1 t2 IHt2 | t1 IHt1 t2 IHt2 t3 IHt3].
+  - reflexivity.
+  - reflexivity.
+  - reflexivity.
+  - reflexivity.
+Qed.
+
+(* ********** *)
+
+Inductive list' (V : Type) : Type :=
+  nil' : list' V
+| cons' : V -> list' V -> list' V.
+
+(*
+list' is defined
+list'_rect is defined
+list'_ind is defined
+list'_rec is defined
+*)
+
+Check list'_ind.
+(* : forall (V : Type)
+            (P : list' V -> Prop),
+       P (nil' V) ->
+       (forall (v : V)
+               (vs' : list' V),
+          P vs' ->
+          P (cons' V v vs')) ->
+       forall vs : list' V,
+         P vs
+*)
+
+Proposition list'_identity :
+  forall (V : Type)
+         (vs : list' V),
+    vs = vs.
+Proof.
+  intros V vs.
+  induction vs as [ | v vs' IHvs'].
+  - 
+(* The goal is the base case, where "P x" is "x = x", for any x:
+
+  V : Type
+  ============================
+  nil' V = nil' V
+*)
+    reflexivity.
+  - revert v vs' IHvs'.
+(* The goal is the induction step, where "P x" is "x = x", for any x:
+
+  forall (v : V) (vs' : list' V), vs' = vs' -> cons' V v vs' = cons' V v vs'
+*)
+    intros v vs' IHvs'.
+    reflexivity.
+Qed.
+
+Check list_ind.
+(* : forall (V : Type)
+            (P : list V -> Prop),
+       P nil ->
+       (forall (v : V)
+               (vs' : list V),
+          P vs' ->
+          P (v :: vs)%list) ->
+       forall vs : list V,
+         P vs
+*)
+
+Proposition list_identity :
+  forall (V : Type)
+         (vs : list V),
+    vs = vs.
+Proof.
+  intros V vs.
+  reflexivity.
+
+  Restart.
+
+  intros V vs.
+  case vs as [ | v vs'] eqn:H_vs.
+  - reflexivity.
+  - reflexivity.
+
+  Restart.
+
+  intros V [ | v vs'].
+  - reflexivity.
+  - reflexivity.
+
+  Restart.
+  intros V vs.
+  induction vs as [ | v vs' IHvs'].
+  - 
+(* The goal is the base case, where "P x" is "x = x", for any x:
+
+  V : Type
+  ============================
+  nil = nil
+*)
+    reflexivity.
+  - revert v vs' IHvs'.
+(* The goal is the induction step, where "P x" is "x = x", for any x:
+
+  V : Type
+  ============================
+  forall (v : V) (vs' : list V), vs' = vs' -> (v :: vs')%list = (v :: vs')%list
+*)
+    intros v vs' IHvs'.
+    reflexivity.
+Qed.
+
+(* ********** *)
+
+(* Exercise 11 *)
+
+Inductive tsil' (V : Type) : Type :=
+ lin' : tsil' V
+| snoc' : tsil' V -> V -> tsil' V.
+
+Fixpoint list'_to_tsil' (V : Type) (vs : list' V) : tsil' V :=
+  match vs with
+  | nil' _ =>
+    lin' V
+  | cons' _ v vs' =>
+    snoc' V (list'_to_tsil' V vs') v
+  end.
+
+Lemma fold_unfold_list'_to_tsil'_nil' :
+  forall (V : Type),
+    list'_to_tsil' V (nil' V) =
+    lin' V.
+Proof.
+  fold_unfold_tactic list'_to_tsil'.
+Qed.
+
+Lemma fold_unfold_list'_to_tsil'_cons' :
+  forall (V : Type)
+         (v : V)
+         (vs' : list' V),
+    list'_to_tsil' V (cons' V v vs') =
+    snoc' V (list'_to_tsil' V vs') v.
+Proof.
+  fold_unfold_tactic list'_to_tsil'.
+Qed.
+
+Fixpoint tsil'_to_list' (V : Type) (sv : tsil' V) : list' V :=
+  match sv with
+  | lin' _ =>
+    nil' V
+  | snoc' _ sv' v =>
+    cons' V v (tsil'_to_list' V sv')
+  end.
+
+Lemma fold_unfold_tsil'_to_list'_lin' :
+  forall (V : Type),
+    tsil'_to_list' V (lin' V) =
+    nil' V.
+Proof.
+  fold_unfold_tactic tsil'_to_list'.
+Qed.
+
+Lemma fold_unfold_tsil'_to_list'_snoc' :
+  forall (V : Type)
+         (sv' : tsil' V)
+         (v : V),
+    tsil'_to_list' V (snoc' V sv' v) =
+    cons' V v (tsil'_to_list' V sv').
+Proof.
+  fold_unfold_tactic tsil'_to_list'.
+Qed.
+
+Theorem tsil'_to_list'_is_a_left_inverse_of_list'_to_tsil' :
+  forall (V : Type)
+         (vs : list' V),
+    tsil'_to_list' V (list'_to_tsil' V vs) = vs.
+Proof.
+  intros V vs.
+  induction vs as [ | v vs' IHvs'].
+  - rewrite -> (fold_unfold_list'_to_tsil'_nil' V).
+    exact (fold_unfold_tsil'_to_list'_lin' V).
+  - rewrite -> (fold_unfold_list'_to_tsil'_cons' V v vs').
+    rewrite -> (fold_unfold_tsil'_to_list'_snoc' V (list'_to_tsil' V vs') v).
+    rewrite -> IHvs'.
+    reflexivity.
+Qed.
+
+Theorem list'_to_tsil'_is_a_left_inverse_of_tsil'_to_list' :
+  forall (V : Type)
+         (sv : tsil' V),
+    list'_to_tsil' V (tsil'_to_list' V sv) = sv.
+Proof.
+  intros V sv.
+  induction sv as [ | sv' IHsv' v].
+  - rewrite -> (fold_unfold_tsil'_to_list'_lin' V).
+    exact (fold_unfold_list'_to_tsil'_nil' V).
+  - rewrite -> (fold_unfold_tsil'_to_list'_snoc' V sv' v).
+    rewrite -> (fold_unfold_list'_to_tsil'_cons' V v (tsil'_to_list' V sv')).
+    rewrite -> IHsv'.
+    reflexivity.
+Qed.
+
+(* ********** *)
+
+Theorem identity :
+  forall (V : Type)
+         (v : V),
+    v = v.
+Proof.
+  intros V v.
+  reflexivity.
+Qed.
+
+Corollary list_identity_revisited :
+  forall (V : Type)
+         (vs : list V),
+    vs = vs.
+Proof.
+  intro V.
+  exact (identity (list V)).
+Qed.
+
+(* ********** *)
+
+Definition bool_to_bool' (b : bool) : bool' :=
+  match b with
+  | true =>
+    true'
+  | false =>
+    false'
+  end.
+
+Definition bool'_to_bool (b : bool') : bool :=
+  match b with
+  | true' =>
+    true
+  | false' =>
+    false
+  end.
+
+Proposition bool'_to_bool_is_a_left_inverse_of_bool_to_bool' :
+  forall b : bool,
+    bool'_to_bool (bool_to_bool' b) = b.
+Proof.
+  intro b.
+  case b.
+  - rewrite→ (bool_to_bool' true).
+  intros [ | ].
+  - reflexivity.
+  intros [ | ]; reflexivity.
+Qed.
+
+Proposition bool_to_bool'_is_a_left_inverse_of_bool'_to_bool :
+  forall b' : bool',
+    bool_to_bool' (bool'_to_bool b') = b'.
+Proof.
+  intros [ | ]; reflexivity.
+Qed.
+
+(* ********** *)
+
+Inductive byte_code_instruction : Type :=
+  PUSH : nat -> byte_code_instruction
+| ADD : byte_code_instruction
+| SUB : byte_code_instruction.
+
+Inductive target_program : Type :=
+  Target_program : list byte_code_instruction -> target_program.
+
+Proposition target_program_identity :
+  forall sp : target_program,
+    sp = sp.
+Proof.
+  intro sp.
+(*
+  sp : target_program
+  ============================
+  sp = sp
+*)
+  reflexivity.
+
+  Restart.
+
+  intros [bcis].
+(*
+  bcis : list byte_code_instruction
+  ============================
+  Target_program bcis = Target_program bcis
+*)
+  reflexivity.
+
+  Restart.
+
+  intros [[ | bci bcis']].
+(*
+  ============================
+  Target_program nil = Target_program nil
+
+subgoal 2 (ID 36) is:
+ Target_program (bci :: bcis') = Target_program (bci :: bcis')
+*)
+  - reflexivity.
+  - reflexivity.
+Qed.
+
+(* ********** *)
+
+Inductive empty : Type.
+
+Proposition empty_identity :
+  forall e : empty,
+    e = e.
+Proof.
+  intro e.
+  reflexivity.
+
+  Restart.
+
+  intros [].
+  reflexivity.
+Qed.
+
+(* ********** *)
+
+(* end of week-05_induction-and-induction-proofs-a-recapitulation.v *)
diff --git a/cs3234/labs/week-05_reasoning-about-lambda-dropped-functions.v b/cs3234/labs/week-05_reasoning-about-lambda-dropped-functions.v
new file mode 100644
index 0000000..37efd0f
--- /dev/null
+++ b/cs3234/labs/week-05_reasoning-about-lambda-dropped-functions.v
@@ -0,0 +1,223 @@
+(* week-05_reasoning-about-lambda-dropped-functions.v *)
+(* LPP 2024 - CS3235 2023-2024, Sem2 *)
+(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
+(* Version of 16 Feb 2024 *)
+
+(* ********** *)
+
+Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.
+
+Require Import Arith Bool List.
+
+(* ********** *)
+
+Definition add_acc (n m : nat) : nat :=
+  let fix loop n a :=
+    match n with
+      O =>
+      a
+    | S n' =>
+      loop n' (S a)
+    end
+  in loop n m.
+
+(* ***** *)
+
+Lemma O_is_right_neutral_for_add_acc :
+  forall n : nat,
+    add_acc n 0 = n.
+Proof.
+  unfold add_acc.
+  remember (fix loop (n0 a : nat) {struct n0} : nat := match n0 with
+                                              | 0 => a
+                                              | S n' => loop n' (S a)
+                                              end)
+    as loop eqn:H_loop.
+  assert (fold_unfold_loop_O :
+            forall a : nat,
+              loop 0 a = a).
+  { intro a.
+    rewrite -> H_loop.
+    reflexivity. }
+  assert (fold_unfold_loop_S :
+            forall n' a : nat,
+              loop (S n') a = loop n' (S a)).
+  { intros n' a.
+    rewrite -> H_loop.
+    reflexivity. }
+  assert (about_loop :
+            forall n a : nat,
+              loop n a = loop n 0 + a).
+  { intro n'.
+    induction n' as [ | n'' IHn'']; intro a.
+    - rewrite -> (fold_unfold_loop_O a).
+      rewrite -> (fold_unfold_loop_O 0).
+      exact (Nat.add_0_l a).
+    - rewrite -> (fold_unfold_loop_S n'' a).
+      rewrite -> (fold_unfold_loop_S n'' 0).
+      rewrite (IHn'' (S a)).
+      rewrite (IHn'' (S 0)).
+      Check Nat.add_assoc.
+      rewrite <- Nat.add_assoc.
+      Check Nat.add_1_l.
+      rewrite -> (Nat.add_1_l a).
+      reflexivity. }
+  intro n.
+  induction n as [ | n' IHn'].
+  - rewrite -> (fold_unfold_loop_O 0).
+    reflexivity.
+  - rewrite -> (fold_unfold_loop_S n' 0).
+    rewrite -> (about_loop n' 1).
+    rewrite -> IHn'.
+    exact (Nat.add_1_r n').
+Qed.
+
+(* ***** *)
+
+Lemma add_acc_is_associative :
+  forall n1 n2 n3 : nat,
+    add_acc n1 (add_acc n2 n3) = add_acc (add_acc n1 n2) n3.
+Proof.
+  unfold add_acc.
+  remember (fix loop (n0 a : nat) {struct n0} : nat := match n0 with
+                                              | 0 => a
+                                              | S n' => loop n' (S a)
+                                              end)
+    as loop eqn:H_loop.
+  assert (fold_unfold_loop_O :
+            forall a : nat,
+              loop 0 a = a).
+  { intro a.
+    rewrite -> H_loop.
+    reflexivity. }
+  assert (fold_unfold_loop_S :
+            forall n' a : nat,
+              loop (S n') a = loop n' (S a)).
+  { intros n' a.
+    rewrite -> H_loop.
+    reflexivity. }
+  assert (about_loop :
+            forall n a : nat,
+              loop n a = loop n 0 + a).
+  { intro n'.
+    induction n' as [ | n'' IHn'']; intro a.
+    - rewrite -> (fold_unfold_loop_O a).
+      rewrite -> (fold_unfold_loop_O 0).
+      exact (Nat.add_0_l a).
+    - rewrite -> (fold_unfold_loop_S n'' a).
+      rewrite -> (fold_unfold_loop_S n'' 0).
+      rewrite (IHn'' (S a)).
+      rewrite (IHn'' (S 0)).
+      Check Nat.add_assoc.
+      rewrite <- Nat.add_assoc.
+      Check Nat.add_1_l.
+      rewrite -> (Nat.add_1_l a).
+      reflexivity. }
+  intro n1.
+  induction n1 as [ | n1' IHn1'].
+  - intros n2 n3.
+    rewrite -> (fold_unfold_loop_O (loop n2 n3)).
+    rewrite -> (fold_unfold_loop_O n2).
+    reflexivity.
+  - intros n2 n3.
+    rewrite -> (fold_unfold_loop_S n1' (loop n2 n3)).
+    rewrite -> (fold_unfold_loop_S n1' n2).
+    rewrite <- (IHn1' (S n2) n3).
+    assert (helpful :
+              forall x y : nat,
+                S (loop x y) = loop (S x) y).
+    { intro x.
+      induction x as [ | x' IHx'].
+      - intro y.
+        rewrite -> (fold_unfold_loop_O y).
+        rewrite -> (fold_unfold_loop_S 0 y).
+        rewrite -> (fold_unfold_loop_O (S y)).
+        reflexivity.
+      - intro y.
+        rewrite -> (fold_unfold_loop_S x' y).
+        rewrite -> (fold_unfold_loop_S (S x') y).
+        exact (IHx' (S y)). }
+    rewrite -> (helpful n2 n3).
+    reflexivity.
+Qed.
+
+(* ********** *)
+
+Definition power (x n : nat) : nat :=
+  let fix loop i a :=
+    match i with
+      O =>
+      a
+    | S i' =>
+      loop i' (x * a)
+    end
+  in loop n 1.
+
+Proposition about_exponentiating_with_a_sum :
+  forall x n1 n2 : nat,
+    power x (n1 + n2) = power x n1 * power x n2.
+Proof.
+  unfold power.
+  intro x.
+  remember (fix loop (i a : nat) {struct i} : nat := match i with
+                                                     | 0 => a
+                                                     | S i' => loop i' (x * a)
+                                                     end)
+    as loop eqn:H_loop.
+  assert (fold_unfold_loop_O :
+            forall a : nat,
+              loop 0 a = a).
+  { intro a.
+    rewrite -> H_loop.
+    reflexivity. }
+  assert (fold_unfold_loop_S :
+            forall i' a : nat,
+              loop (S i') a = loop i' (x * a)).
+  { intros n' a.
+    rewrite -> H_loop.
+    reflexivity. }
+  assert (eureka :
+            forall n a : nat,
+              loop n a = loop n 1 * a).
+  { intro n.
+    induction n as [ | n' IHn'].
+    - intro a.
+      rewrite -> (fold_unfold_loop_O a).
+      rewrite -> (fold_unfold_loop_O 1).
+      symmetry.
+      exact (Nat.mul_1_l a).
+    - intro a.
+      rewrite -> (fold_unfold_loop_S n' a).
+      rewrite -> (fold_unfold_loop_S n' 1).
+      rewrite -> (Nat.mul_1_r x).
+      rewrite -> (IHn' (x * a)).
+      rewrite -> (IHn' x).
+      Check (Nat.mul_assoc (loop n' 1) x a).
+      exact (Nat.mul_assoc (loop n' 1) x a). }
+  intro n1.
+  induction n1 as [ | n1' IHn1'].
+  - intro n2.
+    rewrite -> (Nat.add_0_l n2).
+    rewrite -> (fold_unfold_loop_O 1).
+    symmetry.
+    exact (Nat.mul_1_l (loop n2 1)).
+  - intro n2.
+    Check plus_Sn_m.
+    rewrite -> (plus_Sn_m n1' n2).
+    rewrite -> (fold_unfold_loop_S (n1' + n2) 1).
+    rewrite -> (Nat.mul_1_r x).
+    rewrite -> (fold_unfold_loop_S n1' 1).
+    rewrite -> (Nat.mul_1_r x).
+    rewrite -> (eureka (n1' + n2) x).
+    rewrite -> (eureka n1' x).
+    rewrite -> (IHn1' n2).
+    Check Nat.mul_assoc.
+    rewrite -> (Nat.mul_comm (loop n1' 1 * loop n2 1)).
+    rewrite -> (Nat.mul_comm (loop n1' 1) x).
+    Check Nat.mul_assoc.
+    exact (Nat.mul_assoc x (loop n1' 1) (loop n2 1)).
+Qed.
+
+(* ********** *)
+
+(* end of week-05_reasoning-about-lambda-dropped-functions.v *)