(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/bad_induction".
+
include "nat/nat.ma".
theorem absurd: ∀n. n = O.
intros.
letin P ≝ (λx:nat. n = O).
- apply (bad_ind P n); simplify; intros; autobatch.
+ apply (bad_ind P n); simplify; intros; unfold; autobatch.
qed.
\ No newline at end of file