+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+universe constraint Type[0] < Type[1].
+universe constraint Type[1] < Type[2].
+
+naxiom T : Type[0].
+naxiom P : T → T → CProp[0].
+naxiom Q : T → CProp[0].
+naxiom f : T → T → T.
+
+naxiom f_com : ∀x,y. P (f x y) (f y x).
+naxiom f_Q : ∀x,y. P x y → Q (f x y).
+
+nlemma foo : ∀x,y. Q x → Q (f (f x y) (f y x)).
+#x; #y; #H;
+ncut (Q x);
+##[##2: #_; nauto;
+##| nassumption;
+##]
+nqed.
+
+naxiom And : CProp[0] → CProp[0] → CProp[0].
+naxiom And_intro : ∀A,B.A → B → And A B.
+
+naxiom zero : T.
+naxiom succ : T → T.
+naxiom is_nat : T → CProp[0].
+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