1. rewrite_* and rewrite_back_* merged into one function

[helm.git] / helm / matita / tests / fguidi.ma

diff --git a/helm/matita/tests/fguidi.ma b/helm/matita/tests/fguidi.ma
index 11396b8bdc8160327373a3c5f55037092028b575..c0662e78f9986fc3b6d59124efb9272f44aca417 100644 (file)
--- a/helm/matita/tests/fguidi.ma
+++ b/helm/matita/tests/fguidi.ma
@@ -102,5 +102,5 @@ qed.
 theorem le_gen_S_S_2: \forall m,n. (le (S m) (S n)) \to (le m n).
 intros.
 lapply le_gen_S_x_2 to H using H0. elim H0. elim H1. 
-lapply eq_gen_S_S to H2 using H4. rewrite left H4. assumption.
+lapply eq_gen_S_S to H2 using H4. rewrite > H4. assumption.
 qed.