From d43194ae7fed02d5454e329c3b1de3e5c667068b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 6 Jul 2005 11:27:45 +0000 Subject: [PATCH] fix please --- helm/matita/tests/fguidi.ma | 15 ++++----------- 1 file changed, 4 insertions(+), 11 deletions(-) diff --git a/helm/matita/tests/fguidi.ma b/helm/matita/tests/fguidi.ma index 141e29776..274cda027 100644 --- a/helm/matita/tests/fguidi.ma +++ b/helm/matita/tests/fguidi.ma @@ -92,14 +92,7 @@ intros. auto. qed. (* theorem le_trans: \forall x,y. (le x y) \to \forall z. (le y z) \to (le x z). -intros 1. -elim x. auto. -fwd H1 [H0]. -elim H0 names [pippo; pappo]. - -decompose H0 - - -elim H0. clear H0. elim H1. clear H1. - -*) +intros 1. elim x. +clear H. auto. +clear H. fwd H1 [H]. decompose H. +*) \ No newline at end of file -- 2.39.2