From fb7085b34f02f297c527f00d40c1fc52d0a584cc Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 30 May 2011 19:18:51 +0000
Subject: [PATCH] auto does not work here :(

---
 matita/matita/lib/bacato.ma | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 matita/matita/lib/bacato.ma

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 //
-- 
2.39.2