From 5799dca87fe5c1b5a3cc1f4869109fe75d055ecd Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 17 Jul 2009 20:18:04 +0000
Subject: [PATCH] ...

---
 helm/software/matita/nlibrary/logic/connectives.ma | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/helm/software/matita/nlibrary/logic/connectives.ma b/helm/software/matita/nlibrary/logic/connectives.ma
index 6eb2375dc..25fb2ce93 100644
--- a/helm/software/matita/nlibrary/logic/connectives.ma
+++ b/helm/software/matita/nlibrary/logic/connectives.ma
@@ -18,9 +18,6 @@ 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.
-- 
2.39.2