...

[helm.git] / helm / software / matita / tests / ng_auto.ma

diff --git a/helm/software/matita/tests/ng_auto.ma b/helm/software/matita/tests/ng_auto.ma
index b2a4206678b0fa639fee9c3843c38e7fa35f0cb6..2438c547037d2c6f73eb402daf64857c00dbb4ab 100644 (file)
--- a/helm/software/matita/tests/ng_auto.ma
+++ b/helm/software/matita/tests/ng_auto.ma
@@ -41,5 +41,12 @@ 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.  
+##[ #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=4;
 nqed.  
\ No newline at end of file