From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 15 Nov 2007 15:35:16 +0000 (+0000)
Subject: autobatch => [auto]
X-Git-Tag: 0.4.96@7881~13
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b1653b6c1008bb99ee91dcf4f075711f4cbaffa4;p=helm.git

autobatch => [auto]
---

diff --git a/matita/library/technicalities/setoids.ma b/matita/library/technicalities/setoids.ma
index bb8aacac6..b945931c1 100644
--- a/matita/library/technicalities/setoids.ma
+++ b/matita/library/technicalities/setoids.ma
@@ -209,7 +209,23 @@ definition equality_morphism_of_symmetric_areflexive_transitive_relation:
     unfold transitive in H;
     unfold symmetric in sym;
     intro;
-    autobatch new
+      [ apply (H x2 x1 x3 ? ?);
+          [apply (sym x1 x2 ?).
+           apply (H1).
+          |apply (H x1 x x3 ? ?);
+            [apply (H3).
+            |apply (H2).
+            ]
+          ]
+      | apply (H x1 x3 x ? ?);
+         [apply (H x1 x2 x3 ? ?);
+            [apply (H1).
+            |apply (H3).
+            ]
+         |apply (sym x x3 ?).
+          apply (H2).
+         ]
+      ]
   ].
 qed.
 
@@ -227,7 +243,26 @@ definition equality_morphism_of_symmetric_reflexive_transitive_relation:
     intro;
     unfold transitive in H;
     unfold symmetric in sym;
-    autobatch depth=4.
+    [ apply (H x2 x1 x3 ? ?);
+        [apply (sym x1 x2 ?).
+         apply (H1).
+        |apply (H x1 x x3 ? ?);
+          [apply (H3).
+          |apply (H2).
+          ]
+        ]
+    | apply (H x1 x2 x ? ?);
+      [apply (H1).
+      |apply (H x2 x3 x ? ?);
+        [apply (H3).
+        |apply (sym x x3 ?).
+         apply (H x x3 x3 ? ?);
+          [apply (H2).
+          |apply (refl x3).
+          ]
+        ]
+      ]
+    ]
   ]
 qed.
 
@@ -244,7 +279,13 @@ definition equality_morphism_of_asymmetric_areflexive_transitive_relation:
    intros;
    whd;
    intros;
-   autobatch
+   apply (H x2 x1 x3 ? ?);
+    [apply (H1).
+    |apply (H x1 x x3 ? ?);
+      [apply (H3).
+      |apply (H2).
+      ]
+    ]
  ].
 qed.
 
@@ -261,7 +302,13 @@ definition equality_morphism_of_asymmetric_reflexive_transitive_relation:
    intros;
    whd;
    intro;
-   autobatch
+   apply (H x2 x1 x3 ? ?);
+     [apply (H1).
+     |apply (H x1 x x3 ? ?);
+       [apply (H3).
+       |apply (H2).
+       ]
+     ]
  ].
 qed.
 
@@ -301,6 +348,7 @@ theorem impl_trans: transitive ? impl.
  whd;
  unfold impl;
  intros;
+ apply (H1 ?).apply (H ?).apply (H2).
  autobatch.
 qed.