X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Ftests%2Fng_auto.ma;h=6ba8d3da4d129214b2e477e0c22d722ec8a4acc1;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=b2a4206678b0fa639fee9c3843c38e7fa35f0cb6;hpb=60d2eb6a56200d4ddd7bae8ce6eabe464258926d;p=helm.git

diff --git a/helm/software/matita/tests/ng_auto.ma b/helm/software/matita/tests/ng_auto.ma
index b2a420667..6ba8d3da4 100644
--- a/helm/software/matita/tests/ng_auto.ma
+++ b/helm/software/matita/tests/ng_auto.ma
@@ -41,5 +41,31 @@ naxiom is_nat_0 : is_nat zero.
 naxiom is_nat_S : ∀x.is_nat x → is_nat (succ x).
 
 nlemma bar : ∀P:T → CProp[0].P (succ zero) → (λx.And (is_nat x) (P x)) ?.
-##[ #P; #H; nwhd; ##] nauto.  
-nqed.  
\ No newline at end of file
+##[ #P; #H; nwhd; napply And_intro; ##] nauto.  
+nqed.
+
+naxiom A : CProp[0].
+naxiom pA : A.
+
+nlemma baz : ∀P,Q:CProp[0].(A → P) → (And A P → Q) → Q.
+nauto depth=3;
+nqed.
+
+nlemma traz:
+  ∀T:Type[0].
+  ∀And: CProp[0] → CProp[0] → CProp[0] → CProp[0].
+  ∀And_elim : ∀a,b,c.a → b → c → And a b c. 
+  ∀C: T → T → T → CProp[0].
+  ∀B: T → T → CProp[0].
+  ∀A: T → CProp[0].
+  ∀a,b,c:T.
+  ∀p2:A b.
+  ∀p1:A a.
+  ∀p3:B a b. 
+  ∀p3:B b b. 
+  ∀p4:B b a.  
+  ∀p3:B a a. 
+  ∀p5:C a a a.
+  (λx,y,z:T.And (A x) (B x y) (C x y z)) ???.
+##[ #T; #And; #And_intro; #A; #B;  #C; #a;  #b; #p1; #p2; #p3; #p4; #p5;
+    #p6; #p7; nauto;
\ No newline at end of file