...

[helm.git] / helm / software / matita / contribs / ng_TPTP / COL058-2.ma

diff --git a/helm/software/matita/contribs/ng_TPTP/COL058-2.ma b/helm/software/matita/contribs/ng_TPTP/COL058-2.ma
index be4dc09f2cc458743075dbe2a65975dae74ec413..02072cf40b66d3576e680f9dcc1a36b2dd3e390e 100644 (file)
--- a/helm/software/matita/contribs/ng_TPTP/COL058-2.ma
+++ b/helm/software/matita/contribs/ng_TPTP/COL058-2.ma
@@ -4,7 +4,7 @@ include "logic/equality.ma".
 
 (* -------------------------------------------------------------------------- *)
 
-(*  File     : COL058-2 : TPTP v3.2.0. Released v1.0.0. *)
+(*  File     : COL058-2 : 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 lark (response (response lark (response lark lark)) (response lark (response lark lark)))) (response lark (response lark lark))) (response (response lark (response (response lark (response lark lark)) (response lark (response lark lark)))) (response lark (response lark lark)))) (response (response lark (response (response lark (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 lark (response (response lark (response lark lark)) (response lark (response lark lark)))) (response lark (response lark lark))) (response (response lark (response (response lark (response lark lark)) (response lark (response lark lark)))) (response lark (response lark lark)))) (response (response lark (response (response lark (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.
 
 (* -------------------------------------------------------------------------- *)