From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 8 Jul 2009 18:20:47 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~3726
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=a17430d258e886b5164fca3d65ee7da7c40e6a36

...
---

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).