From 7a89ec1e72f61179767c6488177c6d12e69388c5 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sun, 12 Aug 2018 13:04:16 +0200
Subject: Commit before testing polymorphic equality eliminator

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

(limited to 'scratch.thy')

diff --git a/scratch.thy b/scratch.thy
index e06fb7e..3141120 100644
--- a/scratch.thy
+++ b/scratch.thy
@@ -3,6 +3,12 @@ theory scratch
 
 begin
 
+
+lemma "U(O): U(O)"
+proof (rule inhabited_implies_type)
+  show "\<nat>: U(O)" ..
+qed
+
 lemma
   assumes "\<Sum>x:A. B(x): U(i)" "(a,b): \<Sum>x:A. B(x)"
   shows "a : A"
-- 
cgit v1.2.3