From e7448ca77e1e7ae38ca10d3e029bc0e2fb6b537e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 2 Jun 2015 10:52:07 -0700
Subject: [PATCH] feat(library/init/quot): add exists_rep theorem for quotients

---
 library/init/quot.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/library/init/quot.lean b/library/init/quot.lean
index 355e8acb25..c4aa686403 100644
--- a/library/init/quot.lean
+++ b/library/init/quot.lean
@@ -36,6 +36,9 @@ namespace quot
   protected theorem induction_on {A : Type} [s : setoid A] {B : quot s → Prop} (q : quot s) (H : ∀ a, B ⟦a⟧) : B q :=
   ind H q
 
+  theorem exists_rep {A : Type} [s : setoid A] (q : quot s) : ∃ a : A, ⟦a⟧ = q :=
+  quot.induction_on q (λ a, exists.intro a rfl)
+
   section
   variable {A : Type}
   variable [s : setoid A]