X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_TPTP%2FCOL058-2.ma;h=4ebcf330ffa47289ede35f5dd0171fc671535172;hb=0639dda9142d1cf047b07e61fb557e8877aba4d8;hp=be4dc09f2cc458743075dbe2a65975dae74ec413;hpb=11e495dda047bcdfa4267c06cad2d074fcffe3e3;p=helm.git

diff --git a/helm/software/matita/contribs/ng_TPTP/COL058-2.ma b/helm/software/matita/contribs/ng_TPTP/COL058-2.ma
index be4dc09f2..4ebcf330f 100644
--- a/helm/software/matita/contribs/ng_TPTP/COL058-2.ma
+++ b/helm/software/matita/contribs/ng_TPTP/COL058-2.ma
@@ -56,18 +56,18 @@ 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 ##;
 nqed.
 
 (* -------------------------------------------------------------------------- *)