From ec8e1d9d245950f185f6d4ff1b5e1b8755e7202c Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 7 Aug 2018 18:06:10 +0200
Subject: Tweaks

---
 scratch.thy | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'scratch.thy')

diff --git a/scratch.thy b/scratch.thy
index 55e7023..e06fb7e 100644
--- a/scratch.thy
+++ b/scratch.thy
@@ -3,6 +3,12 @@ theory scratch
 
 begin
 
+lemma
+  assumes "\<Sum>x:A. B(x): U(i)" "(a,b): \<Sum>x:A. B(x)"
+  shows "a : A"
+proof (rule Sum_form_conds)
+  
+
 abbreviation pred where "pred \<equiv> \<^bold>\<lambda>n:\<nat>. ind\<^sub>\<nat>(\<lambda>n c. n, 0, n)"
 
 schematic_goal "?a: (pred`0) =\<^sub>\<nat> 0"
-- 
cgit v1.2.3