X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FTPTP%2FHEQ%2FCAT018-4.ma;h=4eb08df91f6cb8a8b3a018c10182592579deb869;hb=34e2c8f59dd7924e15a7746644182d12ad09fed3;hp=3c772d9231152a4f5a07e570a50d3f12d090d892;hpb=2af96fc83e36af5270b1181864855791ed38fbb8;p=helm.git

diff --git a/helm/software/matita/contribs/TPTP/HEQ/CAT018-4.ma b/helm/software/matita/contribs/TPTP/HEQ/CAT018-4.ma
index 3c772d923..4eb08df91 100644
--- a/helm/software/matita/contribs/TPTP/HEQ/CAT018-4.ma
+++ b/helm/software/matita/contribs/TPTP/HEQ/CAT018-4.ma
@@ -111,7 +111,7 @@ include "logic/equality.ma".
 
 (* -------------------------------------------------------------------------- *)
 theorem prove_a_bc_exists:
- ∀Univ:Set.∀X:Univ.∀Y:Univ.∀Z:Univ.∀a:Univ.∀b:Univ.∀c:Univ.∀codomain:∀_:Univ.Univ.∀compose:∀_:Univ.∀_:Univ.Univ.∀domain:∀_:Univ.Univ.∀equivalent:∀_:Univ.∀_:Univ.Prop.∀there_exists:∀_:Univ.Prop.∀H0:there_exists (compose b c).∀H1:there_exists (compose a b).∀H2:∀X:Univ.eq Univ (compose (codomain X) X) X.∀H3:∀X:Univ.eq Univ (compose X (domain X)) X.∀H4:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (compose X (compose Y Z)) (compose (compose X Y) Z).∀H5:∀X:Univ.∀Y:Univ.∀_:there_exists (domain X).∀_:there_exists (compose X Y).eq Univ (domain X) (codomain Y).∀H6:∀X:Univ.∀Y:Univ.∀_:there_exists (compose X Y).eq Univ (domain X) (codomain Y).∀H7:∀X:Univ.∀Y:Univ.∀_:there_exists (compose X Y).there_exists (domain X).∀H8:∀X:Univ.∀_:there_exists (codomain X).there_exists X.∀H9:∀X:Univ.∀_:there_exists (domain X).there_exists X.∀H10:∀X:Univ.∀Y:Univ.∀_:there_exists X.∀_:equivalent X Y.eq Univ X Y.∀H11:∀X:Univ.∀Y:Univ.∀_:equivalent X Y.eq Univ X Y.∀H12:∀X:Univ.∀Y:Univ.∀_:equivalent X Y.there_exists X.there_exists (compose a (compose b c))
+ ∀Univ:Set.∀X:Univ.∀Y:Univ.∀Z:Univ.∀a:Univ.∀b:Univ.∀c:Univ.∀codomain:∀_:Univ.Univ.∀compose:∀_:Univ.∀_:Univ.Univ.∀domain:∀_:Univ.Univ.∀equivalent:∀_:Univ.∀_:Univ.Prop.∀there_exists:∀_:Univ.Prop.∀H0:there_exists (compose b c).∀H1:there_exists (compose a b).∀H2:∀X:Univ.eq Univ (compose (codomain X) X) X.∀H3:∀X:Univ.eq Univ (compose X (domain X)) X.∀H4:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (compose X (compose Y Z)) (compose (compose X Y) Z).∀H5:∀X:Univ.∀Y:Univ.∀_:eq Univ (domain X) (codomain Y).∀_:there_exists (domain X).there_exists (compose X Y).∀H6:∀X:Univ.∀Y:Univ.∀_:there_exists (compose X Y).eq Univ (domain X) (codomain Y).∀H7:∀X:Univ.∀Y:Univ.∀_:there_exists (compose X Y).there_exists (domain X).∀H8:∀X:Univ.∀_:there_exists (codomain X).there_exists X.∀H9:∀X:Univ.∀_:there_exists (domain X).there_exists X.∀H10:∀X:Univ.∀Y:Univ.∀_:eq Univ X Y.∀_:there_exists X.equivalent X Y.∀H11:∀X:Univ.∀Y:Univ.∀_:equivalent X Y.eq Univ X Y.∀H12:∀X:Univ.∀Y:Univ.∀_:equivalent X Y.there_exists X.there_exists (compose a (compose b c))
 .
 intros.
 autobatch depth=5 width=5 size=20 timeout=10;