From a17430d258e886b5164fca3d65ee7da7c40e6a36 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 Jul 2009 18:20:47 +0000 Subject: [PATCH] ... --- helm/software/matita/nlibrary/algebra/magmas.ma | 2 +- helm/software/matita/nlibrary/logic/connectives.ma | 5 ++++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma index 742a5ddb0..0d4d7d6b1 100644 --- a/helm/software/matita/nlibrary/algebra/magmas.ma +++ b/helm/software/matita/nlibrary/algebra/magmas.ma @@ -71,5 +71,5 @@ ndefinition mm_image: | #x; #y; *; #x0; #Hx0; *; #y0; #Hy0; nwhd; napply (ex_intro ????) [ napply (op ? x0 y0) - | nelim daemon ]] + | nelim daemon ]##] nqed. \ No newline at end of file diff --git a/helm/software/matita/nlibrary/logic/connectives.ma b/helm/software/matita/nlibrary/logic/connectives.ma index 02002dc83..6eb2375dc 100644 --- a/helm/software/matita/nlibrary/logic/connectives.ma +++ b/helm/software/matita/nlibrary/logic/connectives.ma @@ -18,6 +18,9 @@ ninductive True: CProp ≝ I : True. ninductive False: CProp ≝. +(* elimination principle *) +ndefinition False_rect ≝ λP: False → Type.λp: False. + match p in False return λp. P p with []. ndefinition Not: CProp → CProp ≝ λA. A → False. @@ -38,4 +41,4 @@ interpretation "logical or" 'or x y = (Or x y). ninductive Ex (A:Type) (P:A → CProp) : CProp ≝ ex_intro: ∀x:A. P x → Ex A P. -interpretation "exists" 'exists x = (Ex ? x). \ No newline at end of file +interpretation "exists" 'exists x = (Ex ? x). -- 2.39.2