diff options
| author | Josh Chen | 2018-08-12 13:04:16 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-08-12 13:04:16 +0200 |
| commit | 7a89ec1e72f61179767c6488177c6d12e69388c5 (patch) | |
| tree | a305bd9d92d6a51dec49b4c741dc77323ff3ab0c /scratch.thy | |
| parent | 25225e0c637a43319fef6889dabc222df05bfd3c (diff) | |
Commit before testing polymorphic equality eliminator
Diffstat (limited to '')
| -rw-r--r-- | scratch.thy | 6 |
1 files changed, 6 insertions, 0 deletions
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" |