X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_TPTP%2FCOL058-3.ma;h=4a51f4ff503e829e81c8b82dec0ddc5b3a6c7710;hb=HEAD;hp=dff033e64ef7137c9460e8ed7bdbd715a5f45816;hpb=11e495dda047bcdfa4267c06cad2d074fcffe3e3;p=helm.git

diff --git a/helm/software/matita/contribs/ng_TPTP/COL058-3.ma b/helm/software/matita/contribs/ng_TPTP/COL058-3.ma
index dff033e64..4a51f4ff5 100644
--- a/helm/software/matita/contribs/ng_TPTP/COL058-3.ma
+++ b/helm/software/matita/contribs/ng_TPTP/COL058-3.ma
@@ -4,7 +4,7 @@ include "logic/equality.ma".
 
 (* -------------------------------------------------------------------------- *)
 
-(*  File     : COL058-3 : TPTP v3.2.0. Released v1.0.0. *)
+(*  File     : COL058-3 : TPTP v3.7.0. Released v1.0.0. *)
 
 (*  Domain   : Combinatory Logic *)
 
@@ -56,18 +56,19 @@ include "logic/equality.ma".
 
 (* ---- Hypothesis: This bird is egocentric  *)
 ntheorem prove_the_bird_exists:
- ∀Univ:Type.∀X1:Univ.∀X2:Univ.
+ (∀Univ:Type.∀X1:Univ.∀X2:Univ.
 ∀lark:Univ.
 ∀response:∀_:Univ.∀_:Univ.Univ.
-∀H0:∀X1:Univ.∀X2:Univ.eq Univ (response (response lark X1) X2) (response X1 (response X2 X2)).eq Univ (response (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark))) (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark)))) (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark)))
+∀H0:∀X1:Univ.∀X2:Univ.eq Univ (response (response lark X1) X2) (response X1 (response X2 X2)).eq Univ (response (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark))) (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark)))) (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark))))
 .
-#Univ.
-#X1.
-#X2.
-#lark.
-#response.
-#H0.
-nauto by H0;
+#Univ ##.
+#X1 ##.
+#X2 ##.
+#lark ##.
+#response ##.
+#H0 ##.
+nauto by H0 ##;
+ntry (nassumption) ##;
 nqed.
 
 (* -------------------------------------------------------------------------- *)