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

diff --git a/helm/software/matita/nlibrary/logic/destruct_bb.ma b/helm/software/matita/nlibrary/logic/destruct_bb.ma
index 269cfc765..308f8bebe 100644
--- a/helm/software/matita/nlibrary/logic/destruct_bb.ma
+++ b/helm/software/matita/nlibrary/logic/destruct_bb.ma
@@ -19,6 +19,7 @@ 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.