From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 22 Feb 2006 21:50:00 +0000 (+0000)
Subject: simplify used in place of change
X-Git-Tag: make_still_working~7537
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=69ea26e2bc9cb25e3a3dfa37b7fa0d20d2697b0b;p=helm.git

simplify used in place of change
---

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.