From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 30 May 2011 19:18:51 +0000 (+0000)
Subject: auto does not work here :(
X-Git-Tag: make_still_working~2477
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fb7085b34f02f297c527f00d40c1fc52d0a584cc;p=helm.git

auto does not work here :(
---

diff --git a/matita/matita/lib/bacato.ma b/matita/matita/lib/bacato.ma
new file mode 100644
index 000000000..41211e69d
--- /dev/null
+++ b/matita/matita/lib/bacato.ma
@@ -0,0 +1,21 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department of the University of Bologna, Italy.
+    ||I||
+    ||T||
+    ||A||  This file is distributed under the terms of the
+    \   /  GNU General Public License Version 2
+     \ /
+      V_______________________________________________________________ *)
+
+include "basics/pts.ma".
+
+inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0→A1→Prop) : Prop ≝
+   | ex3_2_intro: ∀x0,x1. (P0 x0 x1)→(P1 x0 x1)→(P2 x0 x1)→(ex3_2 ? ? ? ? ?).
+
+lemma bacato: ∀A0,A1:Type[0]. ∀P0,P1,P2:A0→A1→Prop. ∀x0,x1.
+              P0 x0 x1 → P1 x0 x1 → P2 x0 x1 →
+              ex3_2 … (λx0,x1. P0 x0 x1) (λx0,x1. P1 x0 x1) (λx0,x1. P2 x0 x1).
+#A0 #A1 #P0 #P1 #P2 #x0 #x1 #H0 #H1 #H2
+@ex3_2_intro //