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 340154979777529f94387cd1c630c6234cf21ab5..af0161c2ac1f885a9c22edb80d672018cc09d875 100644 (file)
--- 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.