+set "baseuri" "cic:/matita/tests/".
+
inductive nat : Set \def
O : nat
| S : nat \to nat.
apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
intro. reflexivity.
simplify. intros.
- (* manca discriminate H3 *)
-qed.
\ No newline at end of file
+ discriminate H3.
+qed.