diff options
Diffstat (limited to 'scratch.thy')
| -rw-r--r-- | scratch.thy | 6 |
1 files changed, 6 insertions, 0 deletions
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" |