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