diff --git a/Basics.v b/Basics.v
index 7fcd1ef..704888f 100644
--- a/Basics.v
+++ b/Basics.v
@@ -489,23 +489,21 @@ Module LateDays.
   Qed.
 End LateDays.
 
-Module Bin.
-  Inductive bin : Type :=
-  | Z
-  | B0 (n : bin)
-  | B1 (n : bin).
+Inductive bin : Type :=
+| Z
+| B0 (n : bin)
+| B1 (n : bin).
 
-  Fixpoint incr (m : bin) : bin :=
-    match m with
-    | Z => B0 Z
-    | B0 b => B1 b
-    | B1 b => B0 (incr b)
-    end.
+Fixpoint incr (m : bin) : bin :=
+  match m with
+  | Z => B0 Z
+  | B0 b => B1 b
+  | B1 b => B0 (incr b)
+  end.
 
-  Fixpoint bin_to_nat (m : bin) : nat :=
-    match m with
-    | Z => O
-    | B0 b => 2 * bin_to_nat b
-    | B1 b => 1 + 2 * bin_to_nat b
-    end.
-End Bin.
+Fixpoint bin_to_nat (m : bin) : nat :=
+  match m with
+  | Z => O
+  | B0 b => 2 * bin_to_nat b
+  | B1 b => 1 + 2 * bin_to_nat b
+  end.
diff --git a/Induction.v b/Induction.v
index b48faf2..e8fb66d 100644
--- a/Induction.v
+++ b/Induction.v
@@ -3,8 +3,7 @@ From LF Require Export Basics.
 Theorem add_0_r : forall n : nat,
     n + 0 = n.
 Proof.
-  intros n.
-  induction n as [| n' IHn'].
+  induction n as [ | n' IHn'].
   - reflexivity.
   - simpl.
     rewrite IHn'.
@@ -14,7 +13,6 @@ Qed.
 Theorem minus_n_n : forall n,
     n - n = 0.
 Proof.
-  intros.
   induction n as [ | n' IHn'].
   - reflexivity.
   - simpl.
@@ -174,7 +172,7 @@ Proof.
   reflexivity.
 Qed.
   
-Theorem distributivity : forall (n m k : nat),
+Theorem mult_plus_distr_l : forall (n m k : nat),
     n * (m + k) = n * m + n * k.
 Proof.
   induction n as [ | n' IHn'].
@@ -206,7 +204,7 @@ Proof.
     assert (H: S n' = n' + 1).
     { rewrite add_comm. reflexivity. }
     rewrite H.
-    rewrite distributivity.
+    rewrite mult_plus_distr_l.
     rewrite n_one_n.
     rewrite IHn'.
     rewrite add_comm.
@@ -240,3 +238,241 @@ Theorem zero_neqb_S : forall n : nat,
 Proof.
   reflexivity.
 Qed.
+
+Theorem andb_false_r : forall b : bool,
+    andb b false = false.
+Proof.
+  intros.
+  rewrite andb_commutative.
+  reflexivity.
+Qed.
+
+Theorem S_neqb_0 : forall n : nat,
+    (S n) =? 0 = false.
+Proof.
+  reflexivity.
+Qed.
+
+Theorem mult_1_l : forall n : nat, 1 * n = n.
+Proof.
+  intros n.
+  simpl.
+  rewrite add_0_r.
+  reflexivity.
+Qed.
+
+Theorem all3_spec : forall b c : bool,
+    b && c || (negb b || negb c) = true.
+Proof.
+  intros [] [].
+  - reflexivity.
+  - reflexivity.
+  - reflexivity.
+  - reflexivity.
+Qed.
+
+Theorem mult_plus_distr_r : forall n m p : nat,
+    (n + m) * p = (n * p) + (m * p).
+Proof.
+  induction p as [ | p' IHp'].
+  - rewrite n_zero_zero.
+    rewrite n_zero_zero.
+    rewrite n_zero_zero.
+    reflexivity.
+  - rewrite mul_comm.
+    simpl.
+    rewrite mul_comm.
+    rewrite IHp'.
+    assert (H: forall n', n' * S p' = S p' * n').
+    { intros. rewrite mul_comm. reflexivity. }
+    rewrite H.
+    rewrite H.
+    simpl.
+    rewrite shuffle_4.
+    assert (H': forall n', p' * n' = n' * p').
+    { intros. rewrite mul_comm. reflexivity. }
+    rewrite H'.
+    rewrite H'.
+    reflexivity.
+Qed.
+
+Theorem mult_assoc : forall n m p : nat,
+    n * (m * p) = (n * m) * p.
+Proof.
+  induction n as [ | n' IHn'].
+  - reflexivity.
+  - intros.
+    simpl.
+    rewrite mult_plus_distr_r.
+    rewrite IHn'.
+    reflexivity.
+Qed.
+
+Theorem add_shuffle3' : forall n m p : nat,
+    n + (m + p) = m + (n + p).
+Proof.
+  intros.
+  rewrite add_assoc.
+  rewrite add_assoc.
+  replace (n + m) with (m + n).
+  - reflexivity.
+  - rewrite add_comm.
+    reflexivity.
+Qed.
+
+Inductive bin : Type :=
+| Z
+| B0 (n : bin)
+| B1 (n : bin).
+
+Fixpoint incr (m : bin) : bin :=
+  match m with
+  | Z => B1 Z
+  | B0 b => B1 b
+  | B1 b => B0 (incr b)
+  end.
+
+Fixpoint bin_to_nat (m : bin) : nat :=
+  match m with
+  | Z => O
+  | B0 b => 2 * bin_to_nat b
+  | B1 b => 1 + 2 * bin_to_nat b
+  end.
+
+Theorem sn_np1 : forall n : nat,
+    S n = n + 1.
+Proof.
+  intros.
+  rewrite add_comm.
+  reflexivity.
+Qed.
+
+Theorem add_both_r : forall n m k : nat,
+    n = m -> n + k = m + k.
+Proof.
+  intros n m k H.
+  rewrite H.
+  reflexivity.
+Qed.
+
+Theorem add_cancel_r : forall n m k : nat,
+    n + k = m + k -> n = m.
+Proof.
+  induction k as [ | k' IHk'].
+  - rewrite add_0_r.
+    rewrite add_0_r.
+    intro H.
+    rewrite H.
+    reflexivity.
+  - simpl.
+    rewrite <- plus_n_Sm.
+    rewrite <- plus_n_Sm.
+    intro H.
+    inversion H.
+    apply IHk'.
+    rewrite H1.
+    reflexivity.
+Qed.    
+  
+Theorem bin_to_nat_pres_incr : forall b : bin,
+    bin_to_nat (incr b) = S (bin_to_nat b).
+Proof.
+  induction b as [ | b0 | b1 IHb].
+  - reflexivity.
+  - reflexivity.
+  - simpl.
+    rewrite add_0_r.
+    rewrite IHb.
+    rewrite add_0_r.
+    rewrite sn_np1.
+    assert (H: S (S (bin_to_nat b1 + bin_to_nat b1)) = S (bin_to_nat b1 + bin_to_nat b1) + 1).
+    { rewrite sn_np1. reflexivity. }
+    rewrite H.
+    assert (H1 : S (bin_to_nat b1 + bin_to_nat b1) + 1 = bin_to_nat b1 + bin_to_nat b1 + 1 + 1).
+    { rewrite sn_np1. reflexivity. }
+    rewrite H1.
+    rewrite shuffle_4.
+    rewrite add_assoc.
+    reflexivity.
+Qed.
+
+Fixpoint nat_to_bin (n : nat) : bin :=
+  match n with
+  | O => Z
+  | S n' => incr (nat_to_bin n')
+  end.
+
+Theorem nat_bin_nat : forall n : nat,
+    bin_to_nat (nat_to_bin n) = n.
+Proof.
+  induction n as [ | n' IHn'].
+  - reflexivity.
+  - simpl.
+    rewrite bin_to_nat_pres_incr.
+    rewrite IHn'.
+    reflexivity.
+Qed.
+
+Lemma double_incr : forall n : nat,
+    double (S n) = S (S (double n)).
+Proof.
+  intros [ | n' ].
+  - reflexivity.
+  - simpl.
+    reflexivity.
+Qed.
+
+Definition double_bin (b : bin) : bin :=
+  match b with
+  | Z => Z
+  | b' => B0 b'
+  end.
+
+Lemma double_incr_bin : forall b,
+    double_bin (incr b) = incr (incr (double_bin b)).
+Proof.
+  intros [ | b0 | b1 ] ; reflexivity.
+Qed.
+
+Fixpoint normalize (b : bin) : bin :=
+  match b with
+  | B0 Z => Z
+  | Z => Z
+  | B0 b' => double_bin (normalize b')                         
+  | B1 b' => B1 (normalize b')
+  end.
+
+Theorem double_natural : forall n : nat,
+    nat_to_bin (double n) = double_bin (nat_to_bin n).
+Proof.
+  induction n as [ | n' IHn'].
+  - reflexivity.
+  - simpl.
+    rewrite double_incr_bin.
+    rewrite IHn'.
+    reflexivity.
+Qed.
+
+Lemma incr_double_B1 : forall b,
+    incr (double_bin b) = B1 b.
+Proof.
+  induction b as [ | b0 IHb0 | b1 IHb1] ; reflexivity.
+Qed.
+
+Theorem bin_nat_bin : forall b, nat_to_bin (bin_to_nat b) = normalize b.
+  induction b as [ | b0 IHb0 | b1 IHb1].
+  - reflexivity.
+  - simpl.
+    rewrite add_0_r.
+    rewrite <- double_plus.
+    rewrite double_natural.
+    rewrite IHb0.
+    destruct b0 as [ | b0' | b1'] ; reflexivity.
+  - simpl.
+    rewrite add_0_r.
+    rewrite <- double_plus.
+    rewrite double_natural.
+    rewrite IHb1.
+    rewrite incr_double_B1.
+    reflexivity.
+Qed.
diff --git a/Makefile b/Makefile
index 851734c..7dce943 100644
--- a/Makefile
+++ b/Makefile
@@ -45,7 +45,7 @@ HASNATDYNLINK     := $(COQMF_HASNATDYNLINK)
 OCAMLWARN         := $(COQMF_WARN)
 
 Makefile.conf: _CoqProject
-	coq_makefile -f _CoqProject Basics.v -o Makefile
+	coq_makefile -f _CoqProject Basics.v Induction.v Structured.v -o Makefile
 
 # This file can be created by the user to hook into double colon rules or
 # add any other Makefile code he may need
diff --git a/Makefile.conf b/Makefile.conf
index 9015f05..a49f604 100644
--- a/Makefile.conf
+++ b/Makefile.conf
@@ -1,5 +1,5 @@
 # This configuration file was generated by running:
-# coq_makefile -f _CoqProject Basics.v -o Makefile
+# coq_makefile -f _CoqProject Basics.v Induction.v Structured.v -o Makefile
 
 COQBIN?=
 ifneq (,$(COQBIN))
@@ -14,7 +14,7 @@ COQMKFILE ?= "$(COQBIN)coq_makefile"
 #                                                                             #
 ###############################################################################
 
-COQMF_CMDLINE_VFILES := Basics.v
+COQMF_CMDLINE_VFILES := Basics.v Induction.v Structured.v
 COQMF_SOURCES := $(shell $(COQMKFILE) -sources-of -f _CoqProject $(COQMF_CMDLINE_VFILES))
 COQMF_VFILES := $(filter %.v, $(COQMF_SOURCES))
 COQMF_MLIFILES := $(filter %.mli, $(COQMF_SOURCES))
diff --git a/Structured.v b/Structured.v
new file mode 100644
index 0000000..d82f095
--- /dev/null
+++ b/Structured.v
@@ -0,0 +1,443 @@
+From LF Require Export Induction.
+Module NatList.
+
+  Inductive natprod : Type :=
+  | pair (n1 n2 : nat).
+
+  Definition fst (p : natprod) : nat :=
+    match p with
+    | pair x y => x
+    end.
+
+  Definition snd (p : natprod) : nat :=
+    match p with
+    | pair x y => y
+    end.
+
+  Notation "( x , y )" := (pair x y).
+
+  Definition swap_pair (p : natprod) : natprod :=
+    match p with
+    | (x, y) => (y, x)
+    end.
+
+  Theorem surjective_pairing : forall (n m : nat),
+      (n, m) = (fst (n, m), snd (n, m)).
+  Proof.
+    reflexivity.
+  Qed.
+
+  Theorem snd_fst_is_swap : forall (p : natprod),
+      (snd p, fst p) = swap_pair p.
+  Proof.
+    intros [n m].
+    reflexivity.
+  Qed.
+
+  Theorem fst_swap_is_snd : forall (p : natprod),
+      fst (swap_pair p) = snd p.
+  Proof.
+    intros [n m].
+    reflexivity.
+  Qed.
+
+  Inductive natlist : Type :=
+  | nil
+  | cons (n : nat) (l : natlist).
+
+  Notation "x :: l" := (cons x l)
+                         (at level 60, right associativity).
+  Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
+
+  Fixpoint repeat (n count : nat) : natlist :=
+    match count with
+    | 0 => nil
+    | S count' => n :: (repeat n count')
+    end.
+
+  Fixpoint length (l : natlist) : nat :=
+    match l with
+    | nil => 0
+    | _ :: t => S (length t)
+    end.
+
+  Fixpoint app (l1 l2 : natlist) : natlist :=
+    match l1 with
+    | nil => l2
+    | h :: t => h :: (app t l2)
+    end.
+
+  Notation "x ++ y" := (app x y)
+                         (right associativity, at level 60).
+
+  Definition hd (default : nat) (l : natlist) : nat :=
+    match l with
+    | nil => default
+    | h :: t => h
+    end.
+
+  Definition tl (l: natlist) : natlist :=
+    match l with
+    | nil => nil
+    | h :: t => t
+    end.
+
+  Fixpoint nonzeros (l : natlist) : natlist :=
+    match l with
+    | nil => nil
+    | 0 :: t => nonzeros t
+    | h :: t => h :: nonzeros t
+    end.
+
+  Fixpoint odd (n : nat): bool :=
+    match n with
+    | O => false
+    | S n' => negb (odd n')
+    end.
+
+  Fixpoint oddmembers (l : natlist) : natlist :=
+    match l with
+    | nil => nil
+    | h :: t => if odd (h)
+                then h :: oddmembers t
+                else oddmembers t
+    end.
+
+  Definition countoddmembers (l: natlist) : nat :=
+    length (oddmembers l).
+
+  Fixpoint alternate (l1 l2 : natlist) : natlist :=
+    match l1, l2 with
+    | nil, nil => nil
+    | nil, l2' => l2'
+    | l1', nil => l1'
+    | h1 :: t1, h2 :: t2 => h1 :: h2 :: alternate t1 t2
+    end.
+
+  Definition bag := natlist.
+
+  Fixpoint count (v : nat) (s : bag) : nat :=
+    match s with
+    | nil => 0
+    | h :: t => if eqb v h
+                then S (count v t)
+                else count v t
+    end.
+
+  Definition sum : bag -> bag -> bag := app.
+
+  Definition add : nat -> bag -> bag := cons.
+
+  Fixpoint member (v : nat) (s : bag) : bool :=
+    match s with
+    | nil => false
+    | h :: t => if eqb v h
+                then true
+                else member v t
+    end.
+
+  Fixpoint remove_one (v : nat) (s : bag) : bag :=
+    match s with
+    | nil => nil
+    | h :: t => if eqb v h
+                then t
+                else h :: remove_one v t
+    end.
+
+  Fixpoint remove_all (v : nat) (s : bag) : bag :=
+    match s with
+    | nil => nil
+    | h :: t => if eqb v h
+                then remove_all v t
+                else h :: remove_all v t
+    end.
+
+  Fixpoint included (s1 : bag) (s2 : bag) : bool :=
+    match s1 with
+    | nil => true
+    | h :: t => if member h s2
+                then included t s2
+                else false
+    end.
+
+  Theorem add_inc_count : forall (n : nat) (b : bag),
+      count n (add n b) = S (count n b).
+  Proof.
+    intros n [ |[]] ; simpl ; rewrite eqb_refl ; reflexivity.
+  Qed.
+
+  Theorem nil_app : forall l : natlist,
+      nil ++ l = l.
+  Proof. reflexivity. Qed.
+
+  Definition pred n : nat :=
+    match n with
+    | 0 => 0
+    | S n' => n'
+    end.
+
+  Theorem tl_length_pred : forall l : natlist,
+      pred (length l) = length (tl l).
+  Proof.
+    intros [|] ; reflexivity.
+  Qed.
+
+  Theorem app_assoc : forall l1 l2 l3 : natlist,
+      (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
+  Proof.
+    intros l1 l2 l3.
+    induction l1 as [ | n l1' IHl1'].
+    - reflexivity.
+    - simpl.
+      rewrite IHl1'.
+      reflexivity.
+  Qed.
+
+  Fixpoint rev (l: natlist) : natlist :=
+    match l with
+    | nil => nil
+    | h :: t => rev t ++ [h]
+    end.
+
+  Theorem app_length : forall l1 l2 : natlist,
+      length (l1 ++ l2) = (length l1) + (length l2).
+  Proof.
+    intros l1 l2.
+    induction l1 as [ | n l1' IHl1'].
+    - reflexivity.
+    - simpl.
+      rewrite IHl1'.
+      reflexivity.
+  Qed.
+
+  Theorem rev_length : forall l : natlist,
+      length (rev l) = length l.
+  Proof.
+    induction l as [ | n l' IHl'].
+    - reflexivity.
+    - simpl.
+      rewrite app_length.
+      simpl.
+      rewrite IHl'.
+      rewrite <- plus_n_Sm.
+      rewrite add_0_r.
+      reflexivity.
+  Qed.
+
+  Theorem app_nil_r : forall l : natlist,
+      l ++ nil = l.
+  Proof.
+    induction l as [ | n l' IHl'].
+    - reflexivity.
+    - simpl.
+      rewrite IHl'.
+      reflexivity.
+  Qed.
+
+  Theorem rev_app_distr: forall l1 l2 : natlist,
+      rev (l1 ++ l2) = (rev l2) ++ (rev l1).
+  Proof.
+    intros l1 l2.
+    induction l1 as [ | n l1' IHl1'].
+    - simpl.
+      rewrite app_nil_r.
+      reflexivity.
+    - simpl.
+      rewrite IHl1'.
+      rewrite app_assoc.
+      reflexivity.
+  Qed.
+
+  Theorem rev_involutive : forall l : natlist,
+      rev (rev l) = l.
+  Proof.
+    induction l as [ | n l' IHl'].
+    - reflexivity.
+    - simpl.
+      rewrite rev_app_distr.
+      simpl.
+      rewrite IHl'.
+      reflexivity.
+  Qed.
+
+  Theorem app_assoc4 : forall l1 l2 l3 l4 : natlist,
+      l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
+  Proof.
+    intros.
+    repeat rewrite app_assoc.
+    reflexivity.
+  Qed.
+
+  Theorem nonzeros_app : forall l1 l2 : natlist,
+      nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
+  Proof.
+    intros l1 l2.
+    induction l1 as [ | h t IHl1'].
+    - reflexivity.
+    - destruct h as [ | ] ; simpl; rewrite IHl1'; reflexivity.
+  Qed.
+
+  Fixpoint eqblist (l1 l2 : natlist) : bool :=
+    match l1, l2 with
+    | nil, nil => true
+    | nil, _ => false
+    | _, nil => false
+    | h1 :: t1, h2 :: t2 => if eqb h1 h2
+                            then eqblist t1 t2
+                            else false
+    end.
+
+  Theorem eqblist_refl : forall l : natlist,
+      eqblist l l = true.
+  Proof.
+    induction l as [ | h t IHt].
+    - reflexivity.
+    - simpl.
+      rewrite eqb_refl.
+      rewrite IHt.
+      reflexivity.
+  Qed.
+
+  Theorem count_member_nonzero : forall (s : bag),
+      1 <=? (count 1 (1 :: s)) = true.
+
+  Proof.
+    reflexivity.
+  Qed.
+
+  Theorem leb_n_Sn : forall n,
+      n <=? (S n) = true.
+  Proof.
+    induction n as [ | n' IHn'].
+    - reflexivity.
+    - simpl.
+      rewrite IHn'.
+      reflexivity.
+  Qed.
+
+  Theorem remove_does_not_increase_count : forall (s : bag),
+      (count 0 (remove_one 0 s)) <=? (count 0 s) = true.
+  Proof.
+    induction s as [ | [ |h] t IHt].
+    - reflexivity.
+    - simpl.
+      rewrite leb_n_Sn.
+      reflexivity.
+    - simpl.
+      rewrite IHt.
+      reflexivity.
+  Qed.
+
+  Theorem bag_count_sum : forall (b1 b2 : bag),
+      count 0 (sum b1 b2) = count 0 b1 + count 0 b2.
+  Proof.
+    intros b1 b2.
+    induction b1 as [ | h t IHt].
+    - reflexivity.
+    - destruct h as [ |n] ; simpl ; rewrite IHt ; reflexivity.
+  Qed.
+
+  Theorem involution_injective : forall (f : nat -> nat),
+      (forall n : nat, n = f (f n)) ->
+      (forall n1 n2 : nat, f n1 = f n2 -> n1 = n2).
+  Proof.
+    intros f H n1 n2 H1.
+    rewrite H.
+    rewrite <- H1.
+    rewrite <- H.
+    reflexivity.
+  Qed.
+
+  Theorem rev_injective : forall (l1 l2 : natlist),
+      rev l1 = rev l2 -> l1 = l2.
+  Proof.
+    intros l1 l2 H.
+    rewrite <- rev_involutive.
+    rewrite <- H.
+    rewrite rev_involutive.
+    reflexivity.
+  Qed.
+
+  Inductive natoption : Type :=
+  | Some (n : nat)
+  | None.
+
+  Fixpoint nth_error (l : natlist) (n : nat) : natoption :=
+    match l with
+    | nil => None
+    | a :: l' => match n with
+                 | 0 => Some a
+                 | S n' => nth_error l' n'
+                 end
+    end.
+
+  Definition option_elim (d : nat) (o : natoption) : nat :=
+    match o with
+    | Some n' => n'
+    | None => d
+    end.
+
+  Definition hd_error (l : natlist) : natoption :=
+    match l with
+    | nil => None
+    | h :: _ => Some h
+    end.
+
+  Theorem option_elim_hd : forall (l : natlist) (default: nat),
+      hd default l = option_elim default (hd_error l).
+  Proof.
+    intros [ | h tl] d ; reflexivity.
+  Qed.
+End NatList.
+
+Module PartialMap.
+  Export NatList.
+  
+  Inductive id : Type :=
+  | Id (n : nat).
+
+  Definition eqb_id (x1 x2 : id) :=
+    match x1, x2 with
+    | Id n1, Id n2 => n1 =? n2
+    end.
+
+  Theorem eqb_id_refl : forall x, eqb_id x x = true.
+  Proof.
+    intros [x].
+    simpl.
+    rewrite eqb_refl.
+    reflexivity.
+  Qed.
+
+  Inductive partial_map : Type :=
+  | empty
+  | record (i : id) (v : nat) (m : partial_map).
+
+  Definition update (d : partial_map)
+    (x : id) (value : nat)
+    : partial_map :=
+    record x value d.
+
+  Fixpoint find (x : id) (d : partial_map) : natoption :=
+    match d with
+    | empty => None
+    | record y v d' => if eqb_id x y
+                       then Some v
+                       else find x d'
+    end.
+
+  Theorem update_eq :
+    forall (d : partial_map) (x : id) (v : nat),
+      find x (update d x v) = Some v.
+  Proof.
+    intros [ | [] ] [] ; simpl ; rewrite eqb_refl ; reflexivity.
+  Qed.
+
+  Theorem update_neq :
+    forall (d : partial_map) (x y : id) (o : nat),
+      eqb_id x y = false -> find x (update d y o) = find x d.
+  Proof.
+    intros [ | [] ] [] [] o H ; simpl ; simpl in H ; rewrite H ; reflexivity.
+  Qed.
+
+End PartialMap.