1. rewrite_* and rewrite_back_* merged into one function

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

diff --git a/helm/matita/tests/inversion.ma b/helm/matita/tests/inversion.ma
index 888ec5abd130ae290ec3d09555a4859c0f8fbde2..f5ad10c7fc727fb33377c9150cad16926030786b 100644 (file)
--- a/helm/matita/tests/inversion.ma
+++ b/helm/matita/tests/inversion.ma
@@ -20,7 +20,7 @@ theorem test_inversion: \forall n. le n O \to n=O.
   generalize Hcut.
   apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
   (* first goal (left open) *)
-  intro. rewrite right H1.
+  intro. rewrite < H1.
   clear Hcut.
   (* second goal (closed) *)
   goal 14.
@@ -38,7 +38,7 @@ theorem test_inversion2: \forall n. le n O \to n=O.
  generalize (refl_equal nat O).
  apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
  (* first goal (left open) *)
- intro. rewrite right H1.
+ intro. rewrite < H1.
  (* second goal (closed) *)
  goal 13.
  simplify. intros.