From 99a3ae3d6501a29397b8ded59a2227d6488d0d38 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 6 Mar 2003 17:12:55 +0000
Subject: MAJ

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8327 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/faq.tex | 30 +++++++++++++++++++-----------
 1 file changed, 19 insertions(+), 11 deletions(-)

diff --git a/doc/faq.tex b/doc/faq.tex
index bf136327af..b084af498c 100644
--- a/doc/faq.tex
+++ b/doc/faq.tex
@@ -574,6 +574,10 @@ again the missing coercion.
 \question{I have a problem of dependent elimination on
 proofs, how to solve it?}
 
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
 \begin{coq_example*}
 Inductive Def1 : Set
    := c1 : Def1.
@@ -625,6 +629,9 @@ Lemma eq_pack
 
 \answer
 
+\begin{coq_eval}
+Reset eq_pack.
+\end{coq_eval}
 \begin{coq_example*}
 Scheme natProp_elim := Induction for natProp Sort Prop.
 
@@ -635,19 +642,20 @@ Apply pS; Assumption.
 Defined.
 
 Lemma eq_pack
-   : (n:nat)
-     (np:(natProp n))(n':nat)( np':(natProp n'))
-     n=n' -> 
+   : (n,n':nat)
+     n=n' ->
+     (np:(natProp n); np':(natProp n'))
      (pack n np)=(pack n' np').
-Intros n np.
-Elim np using natProp_elim.
-Intros n' np'; Elim np' using natProp_elim; Intros; Auto. 
-Discriminate H0.
-Intros n0 np0 Hrec n' np'; Elim np' using natProp_elim; Intros; Auto. 
-Discriminate H.
-Change (pack_S (pack n0 np0))=(pack_S (pack n1 n2)).
+Intros n n' Heq np np'.
+Generalize Dependent n'.
+NewInduction np using natProp_elim.
+NewInduction np' using natProp_elim; Intros; Auto. 
+Discriminate Heq.
+NewInduction np' using natProp_elim; Intros; Auto. 
+Discriminate Heq.
+Change (pack_S (pack n  np))=(pack_S (pack n0 np')).
 Apply (f_equal package).
-Apply Hrec.
+Apply IHnp.
 Auto.
 Qed.
 \end{coq_example*}
-- 
cgit v1.2.3