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: 0.4.95@7852~1635
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=49f8a041ca862b3fb93c277737c2e7aa02bc4b4e;p=helm.git

simplify used in place of change
---

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.