From ced742083ade162d3ae7c5e3fa78efa291cd3c44 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 1 Apr 2015 13:04:41 -0700
Subject: [PATCH] =?UTF-8?q?feat(library/init/quot):=20add=20helper=20funct?=
 =?UTF-8?q?ion=20quot.rec=5Fon=5Fsubsingleton=E2=82=82?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 library/init/quot.lean | 20 ++++++++++++++++++--
 1 file changed, 18 insertions(+), 2 deletions(-)

diff --git a/library/init/quot.lean b/library/init/quot.lean
index a5aba27ce..4a1e465a7 100644
--- a/library/init/quot.lean
+++ b/library/init/quot.lean
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 Quotient types
 -/
 prelude
-import init.sigma init.setoid
+import init.sigma init.setoid init.logic
 open sigma.ops setoid
 
 constant quot.{l}   : Π {A : Type.{l}}, setoid A → Type.{l}
@@ -91,7 +91,23 @@ namespace quot
   protected theorem ind₂ {C : quot s₁ → quot s₂ → Prop} (H : ∀ a b, C ⟦a⟧ ⟦b⟧) (q₁ : quot s₁) (q₂ : quot s₂) : C q₁ q₂ :=
   quot.ind (λ a₁, quot.ind (λ a₂, H a₁ a₂) q₂) q₁
 
-  protected theorem induction_on₂ {C : quot s₁ → quot s₂ → Prop} (q₁ : quot s₁) (q₂ : quot s₂) (H : ∀ a b, C ⟦a⟧ ⟦b⟧) : C q₁ q₂ :=
+  protected theorem induction_on₂
+     {C : quot s₁ → quot s₂ → Prop} (q₁ : quot s₁) (q₂ : quot s₂) (H : ∀ a b, C ⟦a⟧ ⟦b⟧) : C q₁ q₂ :=
   quot.ind (λ a₁, quot.ind (λ a₂, H a₁ a₂) q₂) q₁
+
+  end
+
+  section
+  variables {A B : Type}
+  variables [s₁ : setoid A] [s₂ : setoid B]
+  include s₁ s₂
+  variable {C : quot s₁ → quot s₂ → Type}
+
+  protected definition rec_on_subsingleton₂ [reducible]
+     {C : quot s₁ → quot s₂ → Type₁} [H : ∀ a b, subsingleton (C ⟦a⟧ ⟦b⟧)]
+     (q₁ : quot s₁) (q₂ : quot s₂) (f : Π a b, C ⟦a⟧ ⟦b⟧) : C q₁ q₂:=
+  @quot.rec_on_subsingleton _ _ _
+    (λ a, quot.ind _ _)
+    q₁ (λ a, quot.rec_on_subsingleton q₂ (λ b, f a b))
   end
 end quot