From 41bf87dd6a35255596638f1b1983a0b2d0d071b8 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 14 Feb 2001 15:57:26 +0000 Subject: Renommage des variables dans les schémas d'induction MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1387 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Wellfounded/Lexicographic_Product.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'theories/Wellfounded/Lexicographic_Product.v') diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index 157265047..a6da918e3 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -29,11 +29,11 @@ Lemma acc_A_B_lexprod : (x:A)(Acc A leA x) ->(y:(B x))(Acc (B x) (leB x) y) ->(Acc (sigS A B) LexProd (existS A B x y)). Proof. - Induction 1. - Induction 4;Intros. + Induction 1; Intros x0 H0 H1 H2 y. + Induction 1;Intros. Apply Acc_intro. Induction y0. - Intros. + Intros x2 y1 H6. Simple Inversion H6;Intros. Cut (leA x2 x0);Intros. Apply H1;Auto with sets. -- cgit v1.2.3