X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Ftests%2Fng_include.ma;h=2582da4b418f95d649915105f6589e594aa17a60;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=4584afddcd5eb3f17fd66ada30724c850a7d2911;hpb=5c8de084e314e41f3dc2f605f6242283e930b803;p=helm.git

diff --git a/helm/software/matita/tests/ng_include.ma b/helm/software/matita/tests/ng_include.ma
index 4584afddc..2582da4b4 100644
--- a/helm/software/matita/tests/ng_include.ma
+++ b/helm/software/matita/tests/ng_include.ma
@@ -24,4 +24,8 @@ axiom P: nat → Prop.
 
 unification hint 0 (∀n. P (0 + n) = P n) .
 
-ntheorem foo: ∀n. ∀H:(P (? + n) → Prop). ∀p:P n. H p.
\ No newline at end of file
+ntheorem foo: ∀n. ∀H:(P (? + n) → Prop). ∀p:P n. H p → True.
+ #n; #H; #p; #_; napply I;
+nqed. 
+
+naxiom nnn: nat.
\ No newline at end of file