From 67dcf461383d4811fe2a2fb60d384804067dbc71 Mon Sep 17 00:00:00 2001
From: Cosimo Oliboni <??>
Date: Thu, 21 Jan 2010 11:49:45 +0000
Subject: [PATCH]

---
 .../contribs/ng_assembly/common/theory.ma     | 25 ++++++++++++++-----
 1 file changed, 19 insertions(+), 6 deletions(-)

diff --git a/helm/software/matita/contribs/ng_assembly/common/theory.ma b/helm/software/matita/contribs/ng_assembly/common/theory.ma
index 3223b1d45..f96351775 100644
--- a/helm/software/matita/contribs/ng_assembly/common/theory.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/theory.ma
@@ -40,6 +40,7 @@ ndefinition Not: Prop → Prop ≝
 
 interpretation "logical not" 'not x = (Not x).
 
+(*
 nlemma absurd : ∀A,C:Prop.A → ¬A → C.
  #A; #C; #H;
  nnormalize;
@@ -177,8 +178,6 @@ ninductive Or2 (A,B:Prop) : Prop ≝
 
 interpretation "logical or" 'or x y = (Or2 x y).
 
-ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
-
 nlemma or2_elim
  : ∀P1,P2,Q:Prop.Or2 P1 P2 → ∀f1:P1 → Q.∀f2:P2 → Q.Q.
  #P1; #P2; #Q; #H; #f1; #f2;
@@ -439,21 +438,22 @@ interpretation "exists" 'exists x = (ex ? x).
 
 ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝
  ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
-
-ndefinition iff ≝
-λA,B.(A → B) ∧ (B → A).
+*)
 
 (* higher_order_defs/relations *)
 
 ndefinition relation : Type → Type ≝
 λA:Type.A → A → Prop. 
 
+(*
 ndefinition reflexive : ∀A:Type.∀R:relation A.Prop ≝
 λA.λR.∀x:A.R x x.
+*)
 
 ndefinition symmetric : ∀A:Type.∀R:relation A.Prop ≝
 λA.λR.∀x,y:A.R x y → R y x.
 
+(*
 ndefinition transitive : ∀A:Type.∀R:relation A.Prop ≝
 λA.λR.∀x,y,z:A.R x y → R y z → R x z.
 
@@ -468,6 +468,7 @@ ndefinition tight_apart : ∀A:Type.∀eq,ap:relation A.Prop ≝
 
 ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
 λA.λR.∀x,y:A.R x y → ¬ (R y x).
+*)
 
 (* logic/equality.ma *)
 
@@ -478,6 +479,7 @@ interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 
 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
 
+(*
 nlemma eq_f : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.x = y → (f x) = (f y).
  #T1; #T2; #x; #y; #f; #H;
  nrewrite < H;
@@ -496,6 +498,7 @@ nlemma neqf_to_neq : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.((f x) ≠ (f y)) 
  nnormalize; #H; #H1;
  napply (H (eq_f … H1)).
 nqed.
+*)
 
 nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
  #A;
@@ -511,7 +514,8 @@ nlemma eq_ind_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
  napply H.
 nqed.
 
-nlemma symmetric_neq : ∀T.∀x,y:T.x ≠ y → y ≠ x.
+(*
+nlemma symmetric_neq : ∀T:Type.∀x,y:T.x ≠ y → y ≠ x.
  #T; #x; #y;
  nnormalize;
  #H; #H1;
@@ -527,3 +531,12 @@ ndefinition symmetricT: ∀A,T:Type.∀R:relationT A T.Prop ≝
 
 ndefinition associative : ∀A:Type.∀R:relationT A A.Prop ≝
 λA.λR.∀x,y,z:A.R (R x y) z = R x (R y z).
+*)
+
+ninductive bool : Type ≝
+ true : bool |
+ false : bool.
+
+nlemma pippo : (true = false) → (false = true).
+ #H; ndestruct.
+nqed.
-- 
2.39.2