From 4eee26eaee55b8e2cb6731c0499d520daf91d38c Mon Sep 17 00:00:00 2001
From: Sean Leather <sean.leather@gmail.com>
Date: Mon, 21 Mar 2016 12:07:22 +0200
Subject: [PATCH] feat(library/data/sigma): add imp_sigma

---
 library/data/sigma.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/library/data/sigma.lean b/library/data/sigma.lean
index 2a287c6c7..78d064be8 100644
--- a/library/data/sigma.lean
+++ b/library/data/sigma.lean
@@ -16,6 +16,9 @@ namespace sigma
   definition unpack {C : (Σa, B a) → Type} {u : Σa, B a} (H : C ⟨u.1 , u.2⟩) : C u :=
   destruct u (λx y H, H) H
 
+  theorem imp_sigma {C : A → Type} (H : ∀a, (B a → C a)) (p : Σa, B a) : Σa, C a :=
+  destruct p (λa Hp, mk a (H a Hp))
+
   theorem dpair_heq {a : A} {a' : A'} {b : B a} {b' : B' a'}
       (HB : B == B') (Ha : a == a') (Hb : b == b') : ⟨a, b⟩ == ⟨a', b'⟩ :=
   hcongr_arg4 @mk (type_eq_of_heq Ha) HB Ha Hb