Commit 77128029 authored by Samuel Ben Hamou's avatar Samuel Ben Hamou
Browse files

Correction d'un bug de Peano.v.

parent cfcefac4
......@@ -8,7 +8,7 @@
# #
###############################################################################
COQMF_VFILES = AsciiOrder.v StringOrder.v StringUtils.v Utils.v Defs.v Nam.v Mix.v NameProofs.v Subst.v Meta.v Equiv.v Equiv2.v AltSubst.v Countable.v Theories.v PreModels.v Models.v Peano.v
COQMF_VFILES = AsciiOrder.v StringOrder.v StringUtils.v Utils.v Defs.v Nam.v Mix.v NameProofs.v Subst.v Meta.v Equiv.v Equiv2.v AltSubst.v Countable.v Theories.v PreModels.v Models.v Peano.v ZF.v
COQMF_MLIFILES =
COQMF_MLFILES =
COQMF_ML4FILES =
......
......@@ -406,7 +406,7 @@ Proof.
unfold PeanoTheory. simpl.
unfold PeanoAx.IsAx.
intros [IN|(B & -> & CK & CL)].
- compute in IN. calc; subst; cbn; intros; subst; omega.
- compute in IN. intuition; subst; cbn; intros; subst; omega.
- intros genv.
unfold PeanoAx.induction_schema.
apply interp_nforall.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment