↑ Up

cocATP---0.2.0.THM-Prf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : cocATP---0.2.0
% Problem  : SEU894^5 : TPTP v6.1.0. Released v4.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p

% Computer : n094.star.cs.uiowa.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz
% Memory   : 32286.75MB
% OS       : Linux 2.6.32-431.20.3.el6.x86_64
% CPULimit : 300s
% DateTime : Thu Jul 17 13:33:21 EDT 2014

% Result   : Theorem 26.66s
% Output   : Proof 26.66s
% Verified : 
% SZS Type : None (Parsing solution fails)
% Syntax   : Number of formulae    : 0

% Comments : 
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % Problem  : SEU894^5 : TPTP v6.1.0. Released v4.0.0.
% % Command  : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p
% % Computer : n094.star.cs.uiowa.edu
% % Model    : x86_64 x86_64
% % CPU      : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% % Memory   : 32286.75MB
% % OS       : Linux 2.6.32-431.20.3.el6.x86_64
% % CPULimit : 300
% % DateTime : Thu Jul 17 11:41:11 CDT 2014
% % CPUTime  : 26.66 
% Python 2.7.5
% Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/']
% FOF formula (forall (F:(fofType->fofType)), ((ex (fofType->fofType)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))))))) of role conjecture named cTHM15_0_pme
% Conjecture to prove = (forall (F:(fofType->fofType)), ((ex (fofType->fofType)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))))))):Prop
% Parameter fofType_DUMMY:fofType.
% We need to prove ['(forall (F:(fofType->fofType)), ((ex (fofType->fofType)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))))']
% Parameter fofType:Type.
% Trying to prove (forall (F:(fofType->fofType)), ((ex (fofType->fofType)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))))
% Found eq_ref00:=(eq_ref0 (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))):(((eq ((fofType->fofType)->Prop)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))))))
% Found (eq_ref0 (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))) as proof of (((eq ((fofType->fofType)->Prop)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))) b)
% Found ((eq_ref ((fofType->fofType)->Prop)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))) as proof of (((eq ((fofType->fofType)->Prop)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))) b)
% Found ((eq_ref ((fofType->fofType)->Prop)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))) as proof of (((eq ((fofType->fofType)->Prop)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))) b)
% Found ((eq_ref ((fofType->fofType)->Prop)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))) as proof of (((eq ((fofType->fofType)->Prop)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))) b)
% Found eta_expansion_dep000:=(eta_expansion_dep00 (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (G x1)) x1)))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))):(((eq ((fofType->fofType)->Prop)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (G x1)) x1)))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))) (fun (x:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P x)))) ((ex fofType) ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (x x1)) x1)))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))))))
% Found (eta_expansion_dep00 (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (G x1)) x1)))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))) as proof of (((eq ((fofType->fofType)->Prop)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (G x1)) x1)))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))) b)
% Found ((eta_expansion_dep0 (fun (x1:(fofType->fofType))=> Prop)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (G x1)) x1)))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))) as proof of (((eq ((fofType->fofType)->Prop)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (G x1)) x1)))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))) b)
% Found (((eta_expansion_dep (fofType->fofType)) (fun (x1:(fofType->fofType))=> Prop)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (G x1)) x1)))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))) as proof of (((eq ((fofType->fofType)->Prop)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (G x1)) x1)))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))) b)
% Found (((eta_expansion_dep (fofType->fofType)) (fun (x1:(fofType->fofType))=> Prop)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (G x1)) x1)))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))) as proof of (((eq ((fofType->fofType)->Prop)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (G x1)) x1)))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))) b)
% Found (((eta_expansion_dep (fofType->fofType)) (fun (x1:(fofType->fofType))=> Prop)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (G x1)) x1)))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))) as proof of (((eq ((fofType->fofType)->Prop)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (G x1)) x1)))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))) b)
% Found eta_expansion0000:=(eta_expansion000 (ex fofType)):(((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))->((ex fofType) (fun (x0:fofType)=> ((and (((eq fofType) (x x0)) x0)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x0) Y)))))))
% Found (eta_expansion000 (ex fofType)) as proof of (P (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))
% Found ((eta_expansion00 (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))) (ex fofType)) as proof of (P (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))
% Found (((eta_expansion0 Prop) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))) (ex fofType)) as proof of (P (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))
% Found ((((eta_expansion fofType) Prop) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))) (ex fofType)) as proof of (P (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))
% Found ((((eta_expansion fofType) Prop) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))) (ex fofType)) as proof of (P (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))
% Found eta_expansion0000:=(eta_expansion000 (ex fofType)):(((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))->((ex fofType) (fun (x0:fofType)=> ((and (((eq fofType) (x x0)) x0)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x0) Y)))))))
% Found (eta_expansion000 (ex fofType)) as proof of (P (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))
% Found ((eta_expansion00 (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))) (ex fofType)) as proof of (P (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))
% Found (((eta_expansion0 Prop) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))) (ex fofType)) as proof of (P (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))
% Found ((((eta_expansion fofType) Prop) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))) (ex fofType)) as proof of (P (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))
% Found ((((eta_expansion fofType) Prop) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))) (ex fofType)) as proof of (P (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))
% Found eta_expansion0000:=(eta_expansion000 (ex fofType)):(((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))->((ex fofType) (fun (x0:fofType)=> ((and (((eq fofType) (x x0)) x0)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x0) Y)))))))
% Found (eta_expansion000 (ex fofType)) as proof of (P (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))
% Found ((eta_expansion00 (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))) (ex fofType)) as proof of (P (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))
% Found (((eta_expansion0 Prop) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))) (ex fofType)) as proof of (P (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))
% Found ((((eta_expansion fofType) Prop) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))) (ex fofType)) as proof of (P (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))
% Found ((((eta_expansion fofType) Prop) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))) (ex fofType)) as proof of (P (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))
% Found eta_expansion0000:=(eta_expansion000 (ex fofType)):(((ex fofType) ((unique fofType) (fun (x10:fofType)=> (((eq fofType) (x x10)) x10))))->((ex fofType) (fun (x0:fofType)=> (((unique fofType) (fun (x10:fofType)=> (((eq fofType) (x x10)) x10))) x0))))
% Found (eta_expansion000 (ex fofType)) as proof of (P ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (x x1)) x1))))
% Found ((eta_expansion00 ((unique fofType) (fun (x10:fofType)=> (((eq fofType) (x x10)) x10)))) (ex fofType)) as proof of (P ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (x x1)) x1))))
% Found (((eta_expansion0 Prop) ((unique fofType) (fun (x10:fofType)=> (((eq fofType) (x x10)) x10)))) (ex fofType)) as proof of (P ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (x x1)) x1))))
% Found ((((eta_expansion fofType) Prop) ((unique fofType) (fun (x10:fofType)=> (((eq fofType) (x x10)) x10)))) (ex fofType)) as proof of (P ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (x x1)) x1))))
% Found ((((eta_expansion fofType) Prop) ((unique fofType) (fun (x10:fofType)=> (((eq fofType) (x x10)) x10)))) (ex fofType)) as proof of (P ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (x x1)) x1))))
% Found eta_expansion0000:=(eta_expansion000 (ex fofType)):(((ex fofType) ((unique fofType) (fun (x10:fofType)=> (((eq fofType) (x x10)) x10))))->((ex fofType) (fun (x0:fofType)=> (((unique fofType) (fun (x10:fofType)=> (((eq fofType) (x x10)) x10))) x0))))
% Found (eta_expansion000 (ex fofType)) as proof of (P ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (x x1)) x1))))
% Found ((eta_expansion00 ((unique fofType) (fun (x10:fofType)=> (((eq fofType) (x x10)) x10)))) (ex fofType)) as proof of (P ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (x x1)) x1))))
% Found (((eta_expansion0 Prop) ((unique fofType) (fun (x10:fofType)=> (((eq fofType) (x x10)) x10)))) (ex fofType)) as proof of (P ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (x x1)) x1))))
% Found ((((eta_expansion fofType) Prop) ((unique fofType) (fun (x10:fofType)=> (((eq fofType) (x x10)) x10)))) (ex fofType)) as proof of (P ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (x x1)) x1))))
% Found ((((eta_expansion fofType) Prop) ((unique fofType) (fun (x10:fofType)=> (((eq fofType) (x x10)) x10)))) (ex fofType)) as proof of (P ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (x x1)) x1))))
% Found eta_expansion0000:=(eta_expansion000 (ex fofType)):(((ex fofType) ((unique fofType) (fun (x10:fofType)=> (((eq fofType) (x x10)) x10))))->((ex fofType) (fun (x0:fofType)=> (((unique fofType) (fun (x10:fofType)=> (((eq fofType) (x x10)) x10))) x0))))
% Found (eta_expansion000 (ex fofType)) as proof of (P ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (x x1)) x1))))
% Found ((eta_expansion00 ((unique fofType) (fun (x10:fofType)=> (((eq fofType) (x x10)) x10)))) (ex fofType)) as proof of (P ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (x x1)) x1))))
% Found (((eta_expansion0 Prop) ((unique fofType) (fun (x10:fofType)=> (((eq fofType) (x x10)) x10)))) (ex fofType)) as proof of (P ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (x x1)) x1))))
% Found ((((eta_expansion fofType) Prop) ((unique fofType) (fun (x10:fofType)=> (((eq fofType) (x x10)) x10)))) (ex fofType)) as proof of (P ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (x x1)) x1))))
% Found ((((eta_expansion fofType) Prop) ((unique fofType) (fun (x10:fofType)=> (((eq fofType) (x x10)) x10)))) (ex fofType)) as proof of (P ((unique fofType) (fun (x1:fofType)=> (((eq fofType) (x x1)) x1))))
% Found x03:(((eq fofType) (x x02)) x02)
% Instantiate: x2:=x02:fofType;x:=F:(fofType->fofType)
% Found x03 as proof of (((eq fofType) (F x2)) x2)
% Found (ex_intro100 x03) as proof of ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))
% Found ((ex_intro10 x02) x03) as proof of ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))
% Found (((ex_intro1 (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03) as proof of ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))
% Found ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03) as proof of ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))
% Found (fun (x04:(forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03)) as proof of ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))
% Found (fun (x03:(((eq fofType) (x x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03)) as proof of ((forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))))
% Found (fun (x03:(((eq fofType) (x x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03)) as proof of ((((eq fofType) (x x02)) x02)->((forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))
% Found (and_rect10 (fun (x03:(((eq fofType) (x x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03))) as proof of ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))
% Found ((and_rect1 ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x03:(((eq fofType) (x x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03))) as proof of ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))
% Found (((fun (P:Type) (x2:((((eq fofType) (x x02)) x02)->((forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))->P)))=> (((((and_rect (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))) P) x2) x1)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x03:(((eq fofType) (x x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03))) as proof of ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))
% Found (fun (x1:((and (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))))=> (((fun (P:Type) (x2:((((eq fofType) (x x02)) x02)->((forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))->P)))=> (((((and_rect (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))) P) x2) x1)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x03:(((eq fofType) (x x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03)))) as proof of ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))
% Found (fun (x02:fofType) (x1:((and (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))))=> (((fun (P:Type) (x2:((((eq fofType) (x x02)) x02)->((forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))->P)))=> (((((and_rect (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))) P) x2) x1)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x03:(((eq fofType) (x x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03)))) as proof of (((and (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))))
% Found (fun (x02:fofType) (x1:((and (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))))=> (((fun (P:Type) (x2:((((eq fofType) (x x02)) x02)->((forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))->P)))=> (((((and_rect (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))) P) x2) x1)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x03:(((eq fofType) (x x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03)))) as proof of (forall (x0:fofType), (((and (((eq fofType) (x x0)) x0)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x0) Y))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))
% Found (ex_ind00 (fun (x02:fofType) (x1:((and (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))))=> (((fun (P:Type) (x2:((((eq fofType) (x x02)) x02)->((forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))->P)))=> (((((and_rect (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))) P) x2) x1)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x03:(((eq fofType) (x x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03))))) as proof of ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))
% Found ((ex_ind0 ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x02:fofType) (x1:((and (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))))=> (((fun (P:Type) (x2:((((eq fofType) (x x02)) x02)->((forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))->P)))=> (((((and_rect (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))) P) x2) x1)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x03:(((eq fofType) (x x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03))))) as proof of ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))
% Found (((fun (P:Prop) (x1:(forall (x0:fofType), (((and (((eq fofType) (x x0)) x0)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x0) Y))))->P)))=> (((((ex_ind fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))) P) x1) x01)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x02:fofType) (x1:((and (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))))=> (((fun (P:Type) (x2:((((eq fofType) (x x02)) x02)->((forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))->P)))=> (((((and_rect (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))) P) x2) x1)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x03:(((eq fofType) (x x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03))))) as proof of ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))
% Found (fun (x01:((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))))=> (((fun (P:Prop) (x1:(forall (x0:fofType), (((and (((eq fofType) (x x0)) x0)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x0) Y))))->P)))=> (((((ex_ind fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))) P) x1) x01)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x02:fofType) (x1:((and (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))))=> (((fun (P:Type) (x2:((((eq fofType) (x x02)) x02)->((forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))->P)))=> (((((and_rect (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))) P) x2) x1)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x03:(((eq fofType) (x x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03)))))) as proof of ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))
% Found (fun (x00:(forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P x)))) (x01:((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))))=> (((fun (P:Prop) (x1:(forall (x0:fofType), (((and (((eq fofType) (x x0)) x0)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x0) Y))))->P)))=> (((((ex_ind fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))) P) x1) x01)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x02:fofType) (x1:((and (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))))=> (((fun (P:Type) (x2:((((eq fofType) (x x02)) x02)->((forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))->P)))=> (((((and_rect (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))) P) x2) x1)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x03:(((eq fofType) (x x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03)))))) as proof of (((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))))
% Found (fun (x00:(forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P x)))) (x01:((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))))=> (((fun (P:Prop) (x1:(forall (x0:fofType), (((and (((eq fofType) (x x0)) x0)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x0) Y))))->P)))=> (((((ex_ind fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))) P) x1) x01)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x02:fofType) (x1:((and (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))))=> (((fun (P:Type) (x2:((((eq fofType) (x x02)) x02)->((forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))->P)))=> (((((and_rect (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))) P) x2) x1)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x03:(((eq fofType) (x x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03)))))) as proof of ((forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P x)))->(((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))
% Found (and_rect00 (fun (x00:(forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P x)))) (x01:((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))))=> (((fun (P:Prop) (x1:(forall (x0:fofType), (((and (((eq fofType) (x x0)) x0)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x0) Y))))->P)))=> (((((ex_ind fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))) P) x1) x01)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x02:fofType) (x1:((and (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))))=> (((fun (P:Type) (x2:((((eq fofType) (x x02)) x02)->((forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))->P)))=> (((((and_rect (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))) P) x2) x1)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x03:(((eq fofType) (x x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03))))))) as proof of ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))
% Found ((and_rect0 ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x00:(forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P x)))) (x01:((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))))=> (((fun (P:Prop) (x1:(forall (x0:fofType), (((and (((eq fofType) (x x0)) x0)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x0) Y))))->P)))=> (((((ex_ind fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))) P) x1) x01)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x02:fofType) (x1:((and (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))))=> (((fun (P:Type) (x2:((((eq fofType) (x x02)) x02)->((forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))->P)))=> (((((and_rect (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))) P) x2) x1)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x03:(((eq fofType) (x x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03))))))) as proof of ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))
% Found (((fun (P:Type) (x1:((forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P x)))->(((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))->P)))=> (((((and_rect (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P x)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))) P) x1) x0)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x00:(forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P x)))) (x01:((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))))=> (((fun (P:Prop) (x1:(forall (x00:fofType), (((and (((eq fofType) (x x00)) x00)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x00) Y))))->P)))=> (((((ex_ind fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))) P) x1) x01)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x02:fofType) (x1:((and (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))))=> (((fun (P:Type) (x2:((((eq fofType) (x x02)) x02)->((forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))->P)))=> (((((and_rect (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))) P) x2) x1)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x03:(((eq fofType) (x x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03))))))) as proof of ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))
% Found (fun (x0:((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P x)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))))=> (((fun (P:Type) (x1:((forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P x)))->(((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))->P)))=> (((((and_rect (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P x)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))) P) x1) x0)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x00:(forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P x)))) (x01:((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))))=> (((fun (P:Prop) (x1:(forall (x00:fofType), (((and (((eq fofType) (x x00)) x00)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x00) Y))))->P)))=> (((((ex_ind fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))) P) x1) x01)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x02:fofType) (x1:((and (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))))=> (((fun (P:Type) (x2:((((eq fofType) (x x02)) x02)->((forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))->P)))=> (((((and_rect (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))) P) x2) x1)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x03:(((eq fofType) (x x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03)))))))) as proof of ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))
% Found (fun (x0:((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P x)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))))=> (((fun (P:Type) (x1:((forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P x)))->(((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))->P)))=> (((((and_rect (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P x)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))) P) x1) x0)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x00:(forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P x)))) (x01:((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))))=> (((fun (P:Prop) (x1:(forall (x00:fofType), (((and (((eq fofType) (x x00)) x00)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x00) Y))))->P)))=> (((((ex_ind fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))) P) x1) x01)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x02:fofType) (x1:((and (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))))=> (((fun (P:Type) (x2:((((eq fofType) (x x02)) x02)->((forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))->P)))=> (((((and_rect (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))) P) x2) x1)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x03:(((eq fofType) (x x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03)))))))) as proof of (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P x)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))))
% Found (ex_intro000 (fun (x0:((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P x)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))))=> (((fun (P:Type) (x1:((forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P x)))->(((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))->P)))=> (((((and_rect (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P x)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y))))))) P) x1) x0)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x00:(forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P x)))) (x01:((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))))=> (((fun (P:Prop) (x1:(forall (x00:fofType), (((and (((eq fofType) (x x00)) x00)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x00) Y))))->P)))=> (((((ex_ind fofType) (fun (X:fofType)=> ((and (((eq fofType) (x X)) X)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) X) Y)))))) P) x1) x01)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x02:fofType) (x1:((and (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))))=> (((fun (P:Type) (x2:((((eq fofType) (x x02)) x02)->((forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))->P)))=> (((((and_rect (((eq fofType) (x x02)) x02)) (forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y)))) P) x2) x1)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x03:(((eq fofType) (x x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (x Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03))))))))) as proof of ((ex (fofType->fofType)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))))))
% Found ((ex_intro00 F) (fun (x0:((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y))))))))=> (((fun (P:Type) (x1:((forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))->(((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y))))))->P)))=> (((((and_rect (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y))))))) P) x1) x0)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x00:(forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))) (x01:((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y)))))))=> (((fun (P:Prop) (x1:(forall (x00:fofType), (((and (((eq fofType) (F x00)) x00)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x00) Y))))->P)))=> (((((ex_ind fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y)))))) P) x1) x01)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x02:fofType) (x1:((and (((eq fofType) (F x02)) x02)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y)))))=> (((fun (P:Type) (x2:((((eq fofType) (F x02)) x02)->((forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y)))->P)))=> (((((and_rect (((eq fofType) (F x02)) x02)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y)))) P) x2) x1)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x03:(((eq fofType) (F x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03))))))))) as proof of ((ex (fofType->fofType)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))))))
% Found (((ex_intro0 (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))) F) (fun (x0:((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y))))))))=> (((fun (P:Type) (x1:((forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))->(((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y))))))->P)))=> (((((and_rect (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y))))))) P) x1) x0)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x00:(forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))) (x01:((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y)))))))=> (((fun (P:Prop) (x1:(forall (x00:fofType), (((and (((eq fofType) (F x00)) x00)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x00) Y))))->P)))=> (((((ex_ind fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y)))))) P) x1) x01)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x02:fofType) (x1:((and (((eq fofType) (F x02)) x02)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y)))))=> (((fun (P:Type) (x2:((((eq fofType) (F x02)) x02)->((forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y)))->P)))=> (((((and_rect (((eq fofType) (F x02)) x02)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y)))) P) x2) x1)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x03:(((eq fofType) (F x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03))))))))) as proof of ((ex (fofType->fofType)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))))))
% Found ((((ex_intro (fofType->fofType)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))) F) (fun (x0:((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y))))))))=> (((fun (P:Type) (x1:((forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))->(((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y))))))->P)))=> (((((and_rect (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y))))))) P) x1) x0)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x00:(forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))) (x01:((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y)))))))=> (((fun (P:Prop) (x1:(forall (x00:fofType), (((and (((eq fofType) (F x00)) x00)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x00) Y))))->P)))=> (((((ex_ind fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y)))))) P) x1) x01)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x02:fofType) (x1:((and (((eq fofType) (F x02)) x02)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y)))))=> (((fun (P:Type) (x2:((((eq fofType) (F x02)) x02)->((forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y)))->P)))=> (((((and_rect (((eq fofType) (F x02)) x02)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y)))) P) x2) x1)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x03:(((eq fofType) (F x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03))))))))) as proof of ((ex (fofType->fofType)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))))))
% Found (fun (F:(fofType->fofType))=> ((((ex_intro (fofType->fofType)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))) F) (fun (x0:((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y))))))))=> (((fun (P:Type) (x1:((forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))->(((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y))))))->P)))=> (((((and_rect (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y))))))) P) x1) x0)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x00:(forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))) (x01:((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y)))))))=> (((fun (P:Prop) (x1:(forall (x00:fofType), (((and (((eq fofType) (F x00)) x00)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x00) Y))))->P)))=> (((((ex_ind fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y)))))) P) x1) x01)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x02:fofType) (x1:((and (((eq fofType) (F x02)) x02)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y)))))=> (((fun (P:Type) (x2:((((eq fofType) (F x02)) x02)->((forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y)))->P)))=> (((((and_rect (((eq fofType) (F x02)) x02)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y)))) P) x2) x1)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x03:(((eq fofType) (F x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03)))))))))) as proof of ((ex (fofType->fofType)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))))))
% Found (fun (F:(fofType->fofType))=> ((((ex_intro (fofType->fofType)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))) F) (fun (x0:((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y))))))))=> (((fun (P:Type) (x1:((forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))->(((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y))))))->P)))=> (((((and_rect (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y))))))) P) x1) x0)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x00:(forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))) (x01:((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y)))))))=> (((fun (P:Prop) (x1:(forall (x00:fofType), (((and (((eq fofType) (F x00)) x00)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x00) Y))))->P)))=> (((((ex_ind fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y)))))) P) x1) x01)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x02:fofType) (x1:((and (((eq fofType) (F x02)) x02)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y)))))=> (((fun (P:Type) (x2:((((eq fofType) (F x02)) x02)->((forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y)))->P)))=> (((((and_rect (((eq fofType) (F x02)) x02)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y)))) P) x2) x1)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x03:(((eq fofType) (F x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03)))))))))) as proof of (forall (F:(fofType->fofType)), ((ex (fofType->fofType)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))))
% Got proof (fun (F:(fofType->fofType))=> ((((ex_intro (fofType->fofType)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))) F) (fun (x0:((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y))))))))=> (((fun (P:Type) (x1:((forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))->(((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y))))))->P)))=> (((((and_rect (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y))))))) P) x1) x0)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x00:(forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))) (x01:((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y)))))))=> (((fun (P:Prop) (x1:(forall (x00:fofType), (((and (((eq fofType) (F x00)) x00)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x00) Y))))->P)))=> (((((ex_ind fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y)))))) P) x1) x01)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x02:fofType) (x1:((and (((eq fofType) (F x02)) x02)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y)))))=> (((fun (P:Type) (x2:((((eq fofType) (F x02)) x02)->((forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y)))->P)))=> (((((and_rect (((eq fofType) (F x02)) x02)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y)))) P) x2) x1)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x03:(((eq fofType) (F x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03))))))))))
% Time elapsed = 26.157515s
% node=2699 cost=1478.000000 depth=30
% ::::::::::::::::::::::
% % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% (fun (F:(fofType->fofType))=> ((((ex_intro (fofType->fofType)) (fun (G:(fofType->fofType))=> (((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P G)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (G X)) X)) (forall (Y:fofType), ((((eq fofType) (G Y)) Y)->(((eq fofType) X) Y)))))))->((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))))) F) (fun (x0:((and (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y))))))))=> (((fun (P:Type) (x1:((forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))->(((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y))))))->P)))=> (((((and_rect (forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))) ((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y))))))) P) x1) x0)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x00:(forall (P:((fofType->fofType)->Prop)), (((and (P F)) (forall (H:(fofType->fofType)), ((P H)->(P (fun (T:fofType)=> (F (H T)))))))->(P F)))) (x01:((ex fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y)))))))=> (((fun (P:Prop) (x1:(forall (x00:fofType), (((and (((eq fofType) (F x00)) x00)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x00) Y))))->P)))=> (((((ex_ind fofType) (fun (X:fofType)=> ((and (((eq fofType) (F X)) X)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) X) Y)))))) P) x1) x01)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x02:fofType) (x1:((and (((eq fofType) (F x02)) x02)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y)))))=> (((fun (P:Type) (x2:((((eq fofType) (F x02)) x02)->((forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y)))->P)))=> (((((and_rect (((eq fofType) (F x02)) x02)) (forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y)))) P) x2) x1)) ((ex fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y)))) (fun (x03:(((eq fofType) (F x02)) x02)) (x04:(forall (Y:fofType), ((((eq fofType) (F Y)) Y)->(((eq fofType) x02) Y))))=> ((((ex_intro fofType) (fun (Y:fofType)=> (((eq fofType) (F Y)) Y))) x02) x03))))))))))
% % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% EOF
%------------------------------------------------------------------------------