X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Flogic%2Fdestruct_bb.ma;h=c64b651180076612c3c3fe27b6b699ac51c50018;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=308f8bebeb91ed3b554cca708bb4e6fbd0eb1124;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git

diff --git a/helm/software/matita/nlibrary/logic/destruct_bb.ma b/helm/software/matita/nlibrary/logic/destruct_bb.ma
index 308f8bebe..c64b65118 100644
--- a/helm/software/matita/nlibrary/logic/destruct_bb.ma
+++ b/helm/software/matita/nlibrary/logic/destruct_bb.ma
@@ -14,13 +14,6 @@
 
 include "logic/equality.ma".
 
-ninductive unit: Type[0] ≝ k: unit.
-
-ninductive bool: unit → Type[0] ≝ true : bool k | false : bool k.
-
-nlemma foo: true = false → False. #H; ndestruct;
-nqed.
-
 (* nlemma prova : ∀T:Type[0].∀a,b:T.∀e:a = b.
                ∀P:∀x,y:T.x=y→Prop.P a a (refl T a) → P a b e.
 #T;#a;#b;#e;#P;#H;