X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Ftests%2Fhard_refine.ma;h=94766ab0b06ba67c81c31ac3d65c1a1dfb8aeb81;hb=ad45ff0a9bc4ddbfe0691ce1edbfa8784b37aa8e;hp=b528414df502b68b3d423c4dbfa501996a744c1d;hpb=dd759c366bc713e36e8405ff6b9534fdff0885e9;p=helm.git

diff --git a/matita/tests/hard_refine.ma b/matita/tests/hard_refine.ma
index b528414df..94766ab0b 100644
--- a/matita/tests/hard_refine.ma
+++ b/matita/tests/hard_refine.ma
@@ -1,5 +1,5 @@
 set "baseuri" "cic:/matita/TPTP/BOO024-1".
-include "legacy/coq.ma".
+include "../legacy/coq.ma".
 alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
 (* Inclusion of: BOO024-1.p *)
 (* -------------------------------------------------------------------------- *)
@@ -52,16 +52,16 @@ letin k3 \def (eq_ind_r A (add (multiply ? (inverse ?)) (multiply b n1)) (\lambd
 focus 633. clearbody k3.
 exact
 (eq_ind A b (\lambda x:A.(eq A x b)) (refl_equal A b) (add (multiply a b) b) (eq_ind A (multiply b n1) (\lambda x:A.(eq A x (add (multiply a b) b))) (eq_ind_r A (add a n1) (\lambda x:A.(eq A (multiply b x) (add (multiply a b) b))) (eq_ind_r A (multiply n1 b) (\lambda x:A.(eq A (multiply b (add a n1)) (add (multiply a b) x))) (H5 b a n1) b (eq_ind A (multiply b n1) (\lambda x:A.(eq A b (multiply n1 x))) (eq_ind A (multiply b n1) (\lambda x:A.(eq A x (multiply n1 (multiply b n1)))) (eq_ind_r A (add b b) (\lambda x:A.(eq A (multiply b n1) (multiply n1 x))) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply b x) (multiply n1 (add b b)))) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply b (add n1 n1)) (multiply x (add b b)))) (eq_ind_r A (add (multiply b (add n1 n1)) (multiply b (add n1 n1))) (\lambda x:A.(eq A (multiply b (add n1 n1)) x)) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A (multiply b (add n1 n1)) (add (multiply b (add n1 n1)) x))) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A x (add (multiply b (add n1 n1)) (add (multiply n1 b) (multiply n1 b))))) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A (add (multiply n1 b) (multiply n1 b)) (add x (add (multiply n1 b) (multiply n1 b))))) (eq_ind A (multiply (add (multiply n1 b) (multiply n1 b)) n1) (\lambda x:A.(eq A x (add (add (multiply n1 b) (multiply n1 b)) (add (multiply n1 b) (multiply n1 b))))) (H7 (multiply n1 b)) (add (multiply n1 b) (multiply n1 b)) (H8 (multiply n1 b))) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply (add n1 n1) (add b b)) (H5 (add n1 n1) b b)) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))) (multiply b n1) (eq_ind_r A (multiply n1 (add b b)) (\lambda x:A.(eq A x (add b b))) (eq_ind A (multiply (add b b) n1) (\lambda x:A.(eq A (multiply n1 (add b b)) x)) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply n1 (add b b)) (multiply (add b b) x))) (eq_ind_r A (add (multiply n1 (add b b)) (multiply n1 (add b b))) (\lambda x:A.(eq A (multiply n1 (add b b)) x)) (eq_ind_r A (add (multiply b n1) (multiply b n1)) (\lambda x:A.(eq A (multiply n1 (add b b)) (add (multiply n1 (add b b)) x))) (eq_ind_r A (add (multiply b n1) (multiply b n1)) (\lambda x:A.(eq A x (add (multiply n1 (add b b)) (add (multiply b n1) (multiply b n1))))) (eq_ind_r A (add (multiply b n1) (multiply b n1)) (\lambda x:A.(eq A (add (multiply b n1) (multiply b n1)) (add x (add (multiply b n1) (multiply b n1))))) (eq_ind A (multiply (add (multiply b n1) (multiply b n1)) n1) (\lambda x:A.(eq A x (add (add (multiply b n1) (multiply b n1)) (add (multiply b n1) (multiply b n1))))) (H7 (multiply b n1)) (add (multiply b n1) (multiply b n1)) (H8 (multiply b n1))) (multiply n1 (add b b)) (H5 n1 b b)) (multiply n1 (add b b)) (H5 n1 b b)) (multiply n1 (add b b)) (H5 n1 b b)) (multiply (add b b) (add n1 n1)) (H5 (add b b) n1 n1)) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))) (add b b) (H8 b)) (multiply b n1) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply b x) (multiply n1 (add b b)))) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply b (add n1 n1)) (multiply x (add b b)))) (eq_ind_r A (add (multiply b (add n1 n1)) (multiply b (add n1 n1))) (\lambda x:A.(eq A (multiply b (add n1 n1)) x)) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A (multiply b (add n1 n1)) (add (multiply b (add n1 n1)) x))) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A x (add (multiply b (add n1 n1)) (add (multiply n1 b) (multiply n1 b))))) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A (add (multiply n1 b) (multiply n1 b)) (add x (add (multiply n1 b) (multiply n1 b))))) (eq_ind A (multiply (add (multiply n1 b) (multiply n1 b)) n1) (\lambda x:A.(eq A x (add (add (multiply n1 b) (multiply n1 b)) (add (multiply n1 b) (multiply n1 b))))) (H7 (multiply n1 b)) (add (multiply n1 b) (multiply n1 b)) (H8 (multiply n1 b))) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply (add n1 n1) (add b b)) (H5 (add n1 n1) b b)) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))))) b ?) b ?)) n1 ?) b ?)).
-auto.
-auto.
-auto.
-auto.
+auto new.
+auto new.
+auto new.
+auto new.
 unfocus.
-auto.
+auto new.
 unfocus.
-auto.
+auto new.
 unfocus.
-auto.
+auto new.
 unfocus.
-auto.
+auto new.
 qed.