From 69ea26e2bc9cb25e3a3dfa37b7fa0d20d2697b0b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 22 Feb 2006 21:50:00 +0000 Subject: [PATCH] simplify used in place of change --- helm/software/matita/library/Q/q.ma | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/helm/software/matita/library/Q/q.ma b/helm/software/matita/library/Q/q.ma index 340154979..af0161c2a 100644 --- a/helm/software/matita/library/Q/q.ma +++ b/helm/software/matita/library/Q/q.ma @@ -199,9 +199,8 @@ intros.apply (fraction_elim2 intros.simplify.unfold Not.intro.apply (not_eq_pp_cons m x f1).apply sym_eq. assumption. intros.simplify.unfold Not.intro.apply (not_eq_nn_cons m x f1).apply sym_eq. assumption. intros. - change in match (eqfb (cons x f1) (cons y g1)) - with (andb (eqZb x y) (eqfb f1 g1)). - apply eqZb_elim. + simplify. + apply eqZb_elim. intro.generalize in match H.elim (eqfb f1 g1). simplify.apply eq_f2.assumption. apply H2. -- 2.39.2