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