From 49f8a041ca862b3fb93c277737c2e7aa02bc4b4e 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 --- matita/library/Q/q.ma | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/matita/library/Q/q.ma b/matita/library/Q/q.ma index 340154979..af0161c2a 100644 --- a/matita/library/Q/q.ma +++ b/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