diff --git a/src/Logic.lagda b/src/Logic.lagda
index 8444e83a..b58512d2 100644
--- a/src/Logic.lagda
+++ b/src/Logic.lagda
@@ -161,8 +161,7 @@ akin to associativity, commutativity, and distributivity.
 ## Conjunction is product
 
 Given two propositions `A` and `B`, the conjunction `A × B` holds
-if both `A` holds and `B` holds.
-We formalise this idea by
+if both `A` holds and `B` holds.  We formalise this idea by
 declaring a suitable inductive type.
 \begin{code}
 data _×_ : Set → Set → Set where
diff --git a/src/extra/Gentzen.lagda b/src/extra/Gentzen.lagda
index b16a1ed8..da8b6d99 100644
--- a/src/extra/Gentzen.lagda
+++ b/src/extra/Gentzen.lagda
@@ -21,7 +21,8 @@ about to write your doctoral dissertation!
 ## Natural Deduction
 
 Here are the inference rules for Natural Deduction annotated with Agda terms.
-    
+
+
     M : A    N : B
     ---------------- ×-I
     (M , N) : A × B
diff --git a/src/extra/Mutual2.agda b/src/extra/Mutual2.agda
new file mode 100644
index 00000000..55904d60
--- /dev/null
+++ b/src/extra/Mutual2.agda
@@ -0,0 +1,46 @@
+open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
+open import Data.Product using (∃; _,_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)
+
++-identity : ∀ (m : ℕ) → m + zero ≡ m
++-identity zero = refl
++-identity (suc m) rewrite +-identity m = refl
+
++-suc : ∀ (m n : ℕ) → n + suc m ≡ suc (n + m)
++-suc m zero = refl
++-suc m (suc n) rewrite +-suc m n = refl
+
++-comm : ∀ (m n : ℕ) → m + n ≡ n + m
++-comm zero n rewrite +-identity n = refl
++-comm (suc m) n rewrite +-suc m n | +-comm m n = refl
+
+data even : ℕ → Set
+data odd : ℕ → Set
+
+data even where
+  zero : even zero
+  suc : ∀ {n : ℕ} → odd n → even (suc n)
+data odd where
+  suc : ∀ {n : ℕ} → even n → odd (suc n)
+
++-lemma : ∀ (m : ℕ) → suc (suc (m + (m + 0))) ≡ suc m + suc (m + 0)
++-lemma m rewrite +-identity m | +-suc m m = refl
+
+is-even : ∀ (n : ℕ) → even n → ∃(λ (m : ℕ) → n ≡ 2 * m)
+is-odd : ∀ (n : ℕ) → odd n → ∃(λ (m : ℕ) → n ≡ 1 + 2 * m)
+
+is-even zero zero =  zero , refl
+is-even (suc n) (suc oddn) with is-odd n oddn
+... | m , n≡1+2*m rewrite n≡1+2*m | +-lemma m = suc m , refl
+
+is-odd (suc n) (suc evenn) with is-even n evenn
+... | m , n≡2*m rewrite n≡2*m = m , refl
+
++-lemma′ : ∀ (m : ℕ) → suc (suc (m + (m + 0))) ≡ suc m + suc (m + 0)
++-lemma′ m rewrite +-suc (m + 0) m = refl
+
+is-even′ : ∀ (n : ℕ) → even n → ∃(λ (m : ℕ) → n ≡ 2 * m)
+is-even′ zero zero =  zero , refl
+is-even′ (suc n) (suc oddn) with is-odd n oddn
+... | m , n≡1+2*m rewrite n≡1+2*m | +-identity m | +-suc m m = suc m , {!!}
+