cocATP---0.2.0.THM-Prf.s

%------------------------------------------------------------------------------
% File     : cocATP---0.2.0
% Problem  : SYN057^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 : n115.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:37:47 EDT 2014

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

% Comments : 
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % Problem  : SYN057^5 : TPTP v6.1.0. Released v4.0.0.
% % Command  : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p
% % Computer : n115.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 08:04:26 CDT 2014
% % CPUTime: 203.72 
% Python 2.7.5
% Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/']
% FOF formula (<kernel.Constant object at 0x1dc9878>, <kernel.DependentProduct object at 0x1dc9758>) of role type named cI
% Using role type
% Declaring cI:(fofType->Prop)
% FOF formula (<kernel.Constant object at 0x2201f38>, <kernel.DependentProduct object at 0x1dc96c8>) of role type named cJ
% Using role type
% Declaring cJ:(fofType->Prop)
% FOF formula (<kernel.Constant object at 0x1dc9c68>, <kernel.DependentProduct object at 0x1dc9680>) of role type named cH
% Using role type
% Declaring cH:(fofType->Prop)
% FOF formula (<kernel.Constant object at 0x1dc9cb0>, <kernel.DependentProduct object at 0x1dc9638>) of role type named cG
% Using role type
% Declaring cG:(fofType->Prop)
% FOF formula (<kernel.Constant object at 0x1dc9a28>, <kernel.DependentProduct object at 0x1dc95f0>) of role type named cF
% Using role type
% Declaring cF:(fofType->Prop)
% FOF formula (((and ((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False)))))->(forall (Xx:fofType), ((cJ Xx)->((cI Xx)->False)))) of role conjecture named cPELL27
% Conjecture to prove = (((and ((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False)))))->(forall (Xx:fofType), ((cJ Xx)->((cI Xx)->False)))):Prop
% Parameter fofType_DUMMY:fofType.
% We need to prove ['(((and ((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False)))))->(forall (Xx:fofType), ((cJ Xx)->((cI Xx)->False))))']
% Parameter fofType:Type.
% Parameter cI:(fofType->Prop).
% Parameter cJ:(fofType->Prop).
% Parameter cH:(fofType->Prop).
% Parameter cG:(fofType->Prop).
% Parameter cF:(fofType->Prop).
% Trying to prove (((and ((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False)))))->(forall (Xx:fofType), ((cJ Xx)->((cI Xx)->False))))
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x5:(cI Xx)
% Found x5 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x7:(cI Xx)
% Found x7 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found x5:(cI Xx)
% Found x5 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x9:(cI Xx)
% Found x9 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found x5:(cI Xx)
% Found x5 as proof of (cI Xx)
% Found x7:(cI Xx)
% Found x7 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x5:(cI Xx)
% Found x5 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x11:(cI Xx)
% Found x11 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found x5:(cI Xx)
% Found x5 as proof of (cI Xx)
% Found x7:(cI Xx)
% Found x7 as proof of (cI Xx)
% Found x9:(cI Xx)
% Found x9 as proof of (cI Xx)
% Found x5:(cI Xx)
% Found x5 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found x5:(cI Xx)
% Found x5 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found x5:(cI Xx)
% Found x5 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x100:False
% Found (fun (x11:(cI Xx))=> x100) as proof of False
% Found (fun (x11:(cI Xx))=> x100) as proof of (not (cI Xx))
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found conj0000:=(conj000 x1):((and (cJ Xx)) (cI Xx))
% Found (conj000 x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x50 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found (x70 ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x7:(cI Xx)
% Found x7 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x5:(cI Xx)
% Found x5 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found conj0000:=(conj000 x1):((and (cJ Xx)) (cI Xx))
% Found (conj000 x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x50 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found (x70 ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found x7:(cI Xx)
% Found x7 as proof of (cI Xx)
% Found x5:(cI Xx)
% Found x5 as proof of (cI Xx)
% Found x5:(cI Xx)
% Found x5 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found x5:(cI Xx)
% Found x5 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found x7:(cI Xx)
% Found x7 as proof of (cI Xx)
% Found conj0000:=(conj000 x1):((and (cJ Xx)) (cI Xx))
% Found (conj000 x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x50 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found (x70 ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found conj0000:=(conj000 x7):((and (cJ Xx)) (cI Xx))
% Found (conj000 x7) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x7) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x7) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x40 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7)) as proof of (cF Xx)
% Found ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7)) as proof of (cF Xx)
% Found ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7)) as proof of (cF Xx)
% Found (x60 ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7))) as proof of (cH Xx)
% Found ((x6 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7))) as proof of (cH Xx)
% Found ((x6 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7))) as proof of (cH Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found conj0000:=(conj000 x3):((and (cJ Xx)) (cI Xx))
% Found (conj000 x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x50 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3)) as proof of (cF Xx)
% Found (x70 ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3))) as proof of (cH Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found x5:(cI Xx)
% Found x5 as proof of (cI Xx)
% Found conj0000:=(conj000 x5):((and (cJ Xx)) (cI Xx))
% Found (conj000 x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x40 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5)) as proof of (cF Xx)
% Found ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5)) as proof of (cF Xx)
% Found ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5)) as proof of (cF Xx)
% Found (x70 ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5))) as proof of (cH Xx)
% Found ((x7 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5))) as proof of (cH Xx)
% Found ((x7 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5))) as proof of (cH Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found x7:(cI Xx)
% Found x7 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found conj0000:=(conj000 x1):((and (cJ Xx)) (cI Xx))
% Found (conj000 x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x50 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found (x70 ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found conj0000:=(conj000 x7):((and (cJ Xx)) (cI Xx))
% Found (conj000 x7) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x7) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x7) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x40 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7)) as proof of (cF Xx)
% Found ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7)) as proof of (cF Xx)
% Found ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7)) as proof of (cF Xx)
% Found (x60 ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7))) as proof of (cH Xx)
% Found ((x6 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7))) as proof of (cH Xx)
% Found ((x6 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7))) as proof of (cH Xx)
% Found conj0000:=(conj000 x3):((and (cJ Xx)) (cI Xx))
% Found (conj000 x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x50 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3)) as proof of (cF Xx)
% Found (x70 ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3))) as proof of (cH Xx)
% Found conj0000:=(conj000 x5):((and (cJ Xx)) (cI Xx))
% Found (conj000 x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x40 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5)) as proof of (cF Xx)
% Found ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5)) as proof of (cF Xx)
% Found ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5)) as proof of (cF Xx)
% Found (x70 ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5))) as proof of (cH Xx)
% Found ((x7 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5))) as proof of (cH Xx)
% Found ((x7 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5))) as proof of (cH Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x5:(cI Xx)
% Found x5 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found conj0000:=(conj000 x1):((and (cJ Xx)) (cI Xx))
% Found (conj000 x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x50 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found (x70 ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found (fun (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))) as proof of (cH Xx)
% Found (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))) as proof of ((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->(cH Xx))
% Found (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))) as proof of (((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->(cH Xx)))
% Found (and_rect20 (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))) as proof of (cH Xx)
% Found ((and_rect2 (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))) as proof of (cH Xx)
% Found (((fun (P:Type) (x6:(((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))->((forall (Xx:fofType), ((cF Xx)->(cH Xx)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))) as proof of (cH Xx)
% Found (((fun (P:Type) (x6:(((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))->((forall (Xx:fofType), ((cF Xx)->(cH Xx)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))) as proof of (cH Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found x5:(cI Xx)
% Found x5 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x7:(cI Xx)
% Found x7 as proof of (cI Xx)
% Found x7:(cI Xx)
% Found x7 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x9:(cI Xx)
% Found x9 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found x5:(cI Xx)
% Found x5 as proof of (cI Xx)
% Found x5:(cI Xx)
% Found x5 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x7:(cI Xx)
% Found x7 as proof of (cI Xx)
% Found conj0000:=(conj000 x1):((and (cJ Xx)) (cI Xx))
% Found (conj000 x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x50 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found (x70 ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found (fun (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))) as proof of (cH Xx)
% Found (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))) as proof of ((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->(cH Xx))
% Found (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))) as proof of (((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->(cH Xx)))
% Found (and_rect20 (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))) as proof of (cH Xx)
% Found ((and_rect2 (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))) as proof of (cH Xx)
% Found (((fun (P:Type) (x6:(((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))->((forall (Xx:fofType), ((cF Xx)->(cH Xx)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))) as proof of (cH Xx)
% Found (((fun (P:Type) (x6:(((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))->((forall (Xx:fofType), ((cF Xx)->(cH Xx)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))) as proof of (cH Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found conj0000:=(conj000 x1):((and (cJ Xx)) (cI Xx))
% Found (conj000 x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x50 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found (x70 ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found x7:(cI Xx)
% Found x7 as proof of (cI Xx)
% Found x7:(cI Xx)
% Found x7 as proof of (cI Xx)
% Found x9:(cI Xx)
% Found x9 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x7:(cI Xx)
% Found x7 as proof of (cI Xx)
% Found conj0000:=(conj000 x1):((and (cJ Xx)) (cI Xx))
% Found (conj000 x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x50 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found (x70 ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found (fun (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))) as proof of (cH Xx)
% Found (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))) as proof of ((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->(cH Xx))
% Found (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))) as proof of (((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->(cH Xx)))
% Found (and_rect20 (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))) as proof of (cH Xx)
% Found ((and_rect2 (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))) as proof of (cH Xx)
% Found (((fun (P:Type) (x6:(((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))->((forall (Xx:fofType), ((cF Xx)->(cH Xx)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))) as proof of (cH Xx)
% Found (((fun (P:Type) (x6:(((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))->((forall (Xx:fofType), ((cF Xx)->(cH Xx)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))) as proof of (cH Xx)
% Found x7:(cI Xx)
% Found x7 as proof of (cI Xx)
% Found x5:(cI Xx)
% Found x5 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found conj0000:=(conj000 x3):((and (cJ Xx)) (cI Xx))
% Found (conj000 x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x50 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3)) as proof of (cF Xx)
% Found (x70 ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3))) as proof of (cH Xx)
% Found (fun (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3)))) as proof of (cH Xx)
% Found (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3)))) as proof of ((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->(cH Xx))
% Found (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3)))) as proof of (((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->(cH Xx)))
% Found (and_rect20 (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3))))) as proof of (cH Xx)
% Found ((and_rect2 (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3))))) as proof of (cH Xx)
% Found (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3))))) as proof of (cH Xx)
% Found (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3))))) as proof of (cH Xx)
% Found x5:(cI Xx)
% Found x5 as proof of (cI Xx)
% Found x7:(cI Xx)
% Found x7 as proof of (cI Xx)
% Found conj0000:=(conj000 x5):((and (cJ Xx)) (cI Xx))
% Found (conj000 x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x40 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5)) as proof of (cF Xx)
% Found ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5)) as proof of (cF Xx)
% Found ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5)) as proof of (cF Xx)
% Found (x70 ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5))) as proof of (cH Xx)
% Found ((x7 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5))) as proof of (cH Xx)
% Found (fun (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5)))) as proof of (cH Xx)
% Found (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5)))) as proof of ((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->(cH Xx))
% Found (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5)))) as proof of (((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->(cH Xx)))
% Found (and_rect20 (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5))))) as proof of (cH Xx)
% Found ((and_rect2 (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5))))) as proof of (cH Xx)
% Found (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x3)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5))))) as proof of (cH Xx)
% Found (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x3)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5))))) as proof of (cH Xx)
% Found x5:(cI Xx)
% Found x5 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x9:(cI Xx)
% Found x9 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found x5:(cI Xx)
% Found x5 as proof of (cI Xx)
% Found conj0000:=(conj000 x1):((and (cJ Xx)) (cI Xx))
% Found (conj000 x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x50 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found (x70 ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found x7:(cI Xx)
% Found x7 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x9:(cI Xx)
% Found x9 as proof of (cI Xx)
% Found conj0000:=(conj000 x1):((and (cJ Xx)) (cI Xx))
% Found (conj000 x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x50 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found (x70 ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found (fun (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))) as proof of (cH Xx)
% Found (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))) as proof of ((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->(cH Xx))
% Found (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))) as proof of (((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->(cH Xx)))
% Found (and_rect20 (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))) as proof of (cH Xx)
% Found ((and_rect2 (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))) as proof of (cH Xx)
% Found (((fun (P:Type) (x6:(((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))->((forall (Xx:fofType), ((cF Xx)->(cH Xx)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))) as proof of (cH Xx)
% Found (((fun (P:Type) (x6:(((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))->((forall (Xx:fofType), ((cF Xx)->(cH Xx)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))) as proof of (cH Xx)
% Found conj0000:=(conj000 x3):((and (cJ Xx)) (cI Xx))
% Found (conj000 x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x50 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3)) as proof of (cF Xx)
% Found (x70 ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3))) as proof of (cH Xx)
% Found (fun (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3)))) as proof of (cH Xx)
% Found (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3)))) as proof of ((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->(cH Xx))
% Found (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3)))) as proof of (((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->(cH Xx)))
% Found (and_rect20 (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3))))) as proof of (cH Xx)
% Found ((and_rect2 (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3))))) as proof of (cH Xx)
% Found (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3))))) as proof of (cH Xx)
% Found (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3))))) as proof of (cH Xx)
% Found conj0000:=(conj000 x5):((and (cJ Xx)) (cI Xx))
% Found (conj000 x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x40 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5)) as proof of (cF Xx)
% Found ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5)) as proof of (cF Xx)
% Found ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5)) as proof of (cF Xx)
% Found (x70 ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5))) as proof of (cH Xx)
% Found ((x7 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5))) as proof of (cH Xx)
% Found (fun (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5)))) as proof of (cH Xx)
% Found (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5)))) as proof of ((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->(cH Xx))
% Found (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5)))) as proof of (((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->(cH Xx)))
% Found (and_rect20 (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5))))) as proof of (cH Xx)
% Found ((and_rect2 (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5))))) as proof of (cH Xx)
% Found (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x3)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5))))) as proof of (cH Xx)
% Found (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x3)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5))))) as proof of (cH Xx)
% Found conj0000:=(conj000 x1):((and (cJ Xx)) (cI Xx))
% Found (conj000 x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x50 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found (x70 ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found conj0000:=(conj000 x3):((and (cJ Xx)) (cI Xx))
% Found (conj000 x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x50 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3)) as proof of (cF Xx)
% Found (x70 ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3))) as proof of (cH Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found conj0000:=(conj000 x9):((and (cJ Xx)) (cI Xx))
% Found (conj000 x9) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x9) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x9) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x9) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x9) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x40 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x9)) as proof of (cF Xx)
% Found ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x9)) as proof of (cF Xx)
% Found ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x9)) as proof of (cF Xx)
% Found (x60 ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x9))) as proof of (cH Xx)
% Found ((x6 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x9))) as proof of (cH Xx)
% Found ((x6 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x9))) as proof of (cH Xx)
% Found conj0000:=(conj000 x5):((and (cJ Xx)) (cI Xx))
% Found (conj000 x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x40 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5)) as proof of (cF Xx)
% Found ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5)) as proof of (cF Xx)
% Found ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5)) as proof of (cF Xx)
% Found (x70 ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5))) as proof of (cH Xx)
% Found ((x7 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5))) as proof of (cH Xx)
% Found ((x7 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5))) as proof of (cH Xx)
% Found x11:((cG x8)->False)
% Instantiate: x12:=x8:fofType
% Found x11 as proof of ((cG x12)->False)
% Found conj0000:=(conj000 x7):((and (cJ Xx)) (cI Xx))
% Found (conj000 x7) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x7) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x7) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x40 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7)) as proof of (cF Xx)
% Found ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7)) as proof of (cF Xx)
% Found ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7)) as proof of (cF Xx)
% Found (x60 ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7))) as proof of (cH Xx)
% Found ((x6 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7))) as proof of (cH Xx)
% Found ((x6 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7))) as proof of (cH Xx)
% Found x11:((cG x8)->False)
% Instantiate: x12:=x8:fofType
% Found x11 as proof of ((cG x12)->False)
% Found x11:((cG x8)->False)
% Instantiate: x12:=x8:fofType
% Found x11 as proof of ((cG x12)->False)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found conj0000:=(conj000 x1):((and (cJ Xx)) (cI Xx))
% Found (conj000 x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x50 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found (x70 ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found (fun (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))) as proof of (cH Xx)
% Found (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))) as proof of ((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->(cH Xx))
% Found (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))) as proof of (((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->(cH Xx)))
% Found (and_rect20 (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))) as proof of (cH Xx)
% Found ((and_rect2 (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))) as proof of (cH Xx)
% Found (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))) as proof of (cH Xx)
% Found (fun (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))))) as proof of (cH Xx)
% Found (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))))) as proof of ((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->(cH Xx))
% Found (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))))) as proof of (((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->(cH Xx)))
% Found (and_rect10 (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))))) as proof of (cH Xx)
% Found ((and_rect1 (cH Xx)) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))))) as proof of (cH Xx)
% Found (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))->((forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx)))) P) x4) x2)) (cH Xx)) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))))) as proof of (cH Xx)
% Found (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))->((forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx)))) P) x4) x2)) (cH Xx)) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))))) as proof of (cH Xx)
% Found x11:((cG x8)->False)
% Instantiate: x12:=x8:fofType
% Found x11 as proof of ((cG x12)->False)
% Found x7:(cI Xx)
% Found x7 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found x5:(cI Xx)
% Found x5 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found conj0000:=(conj000 x1):((and (cJ Xx)) (cI Xx))
% Found (conj000 x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x50 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found (x70 ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found conj0000:=(conj000 x3):((and (cJ Xx)) (cI Xx))
% Found (conj000 x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x50 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3)) as proof of (cF Xx)
% Found (x70 ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x3))) as proof of (cH Xx)
% Found x12:((cG x8)->False)
% Instantiate: x10:=x8:fofType
% Found x12 as proof of ((cG x10)->False)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found x12:((cG x9)->False)
% Instantiate: x6:=x9:fofType
% Found x12 as proof of ((cG x6)->False)
% Found x12:((cG x9)->False)
% Instantiate: x4:=x9:fofType
% Found x12 as proof of ((cG x4)->False)
% Found x12:((cG x9)->False)
% Instantiate: x8:=x9:fofType
% Found x12 as proof of ((cG x8)->False)
% Found conj0000:=(conj000 x9):((and (cJ Xx)) (cI Xx))
% Found (conj000 x9) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x9) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x9) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x9) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x9) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x40 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x9)) as proof of (cF Xx)
% Found ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x9)) as proof of (cF Xx)
% Found ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x9)) as proof of (cF Xx)
% Found (x60 ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x9))) as proof of (cH Xx)
% Found ((x6 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x9))) as proof of (cH Xx)
% Found ((x6 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x9))) as proof of (cH Xx)
% Found x12:((cG x8)->False)
% Instantiate: x10:=x8:fofType
% Found x12 as proof of ((cG x10)->False)
% Found conj0000:=(conj000 x5):((and (cJ Xx)) (cI Xx))
% Found (conj000 x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x40 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5)) as proof of (cF Xx)
% Found ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5)) as proof of (cF Xx)
% Found ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5)) as proof of (cF Xx)
% Found (x70 ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5))) as proof of (cH Xx)
% Found ((x7 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5))) as proof of (cH Xx)
% Found ((x7 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x5))) as proof of (cH Xx)
% Found x12:((cG x9)->False)
% Instantiate: x8:=x9:fofType
% Found x12 as proof of ((cG x8)->False)
% Found x12:((cG x9)->False)
% Instantiate: x6:=x9:fofType
% Found x12 as proof of ((cG x6)->False)
% Found x12:((cG x8)->False)
% Instantiate: x10:=x8:fofType
% Found x12 as proof of ((cG x10)->False)
% Found x12:((cG x9)->False)
% Instantiate: x8:=x9:fofType
% Found x12 as proof of ((cG x8)->False)
% Found conj0000:=(conj000 x7):((and (cJ Xx)) (cI Xx))
% Found (conj000 x7) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x7) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x7) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x40 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7)) as proof of (cF Xx)
% Found ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7)) as proof of (cF Xx)
% Found ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7)) as proof of (cF Xx)
% Found (x60 ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7))) as proof of (cH Xx)
% Found ((x6 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7))) as proof of (cH Xx)
% Found ((x6 Xx) ((x4 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x7))) as proof of (cH Xx)
% Found x7:(cI Xx)
% Found x7 as proof of (cI Xx)
% Found x7:(cI Xx)
% Found x7 as proof of (cI Xx)
% Found x12:((cG x8)->False)
% Instantiate: x10:=x8:fofType
% Found x12 as proof of ((cG x10)->False)
% Found x1:(cI Xx)
% Found x1 as proof of (cI Xx)
% Found x3:(cI Xx)
% Found x3 as proof of (cI Xx)
% Found x5:(cI Xx)
% Found x5 as proof of (cI Xx)
% Found x11:((cG x8)->False)
% Instantiate: x12:=x8:fofType
% Found x11 as proof of ((cG x12)->False)
% Found conj0000:=(conj000 x1):((and (cJ Xx)) (cI Xx))
% Found (conj000 x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found ((conj00 (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> ((conj0 B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1) as proof of ((and (cJ Xx)) (cI Xx))
% Found (x50 (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)) as proof of (cF Xx)
% Found (x70 ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))) as proof of (cH Xx)
% Found (fun (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))) as proof of (cH Xx)
% Found (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))) as proof of ((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->(cH Xx))
% Found (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))) as proof of (((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->(cH Xx)))
% Found (and_rect20 (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))) as proof of (cH Xx)
% Found ((and_rect2 (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))) as proof of (cH Xx)
% Found (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))) as proof of (cH Xx)
% Found (fun (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))))) as proof of (cH Xx)
% Found (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))))) as proof of ((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->(cH Xx))
% Found (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))))) as proof of (((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->(cH Xx)))
% Found (and_rect10 (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))))) as proof of (cH Xx)
% Found ((and_rect1 (cH Xx)) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))))) as proof of (cH Xx)
% Found (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))->((forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx)))) P) x4) x2)) (cH Xx)) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))))) as proof of (cH Xx)
% Found (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))->((forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx)))) P) x4) x2)) (cH Xx)) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))))) as proof of (cH Xx)
% Found x11:((cG x8)->False)
% Instantiate: x12:=x8:fofType
% Found x11 as proof of ((cG x12)->False)
% Found x11:((cG x8)->False)
% Instantiate: x12:=x8:fofType
% Found x11 as proof of ((cG x12)->False)
% Found x11:((cG x8)->False)
% Instantiate: x12:=x8:fofType
% Found x11 as proof of ((cG x12)->False)
% Found x700:=(x70 x10):(cH x12)
% Found (x70 x10) as proof of (cH x12)
% Found ((x7 x12) x10) as proof of (cH x12)
% Found ((x7 x12) x10) as proof of (cH x12)
% Found ((conj00 ((x7 x12) x10)) x11) as proof of ((and (cH x12)) ((cG x12)->False))
% Found (((conj0 ((cG x12)->False)) ((x7 x12) x10)) x11) as proof of ((and (cH x12)) ((cG x12)->False))
% Found ((((conj (cH x12)) ((cG x12)->False)) ((x7 x12) x10)) x11) as proof of ((and (cH x12)) ((cG x12)->False))
% Found ((((conj (cH x12)) ((cG x12)->False)) ((x7 x12) x10)) x11) as proof of ((and (cH x12)) ((cG x12)->False))
% Found (ex_intro000 ((((conj (cH x12)) ((cG x12)->False)) ((x7 x12) x10)) x11)) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))
% Found ((ex_intro00 x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11)) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))
% Found (((ex_intro0 (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11)) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))
% Found ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11)) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))
% Found (fun (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))
% Found (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))) as proof of (((cG x8)->False)->((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))))
% Found (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))) as proof of ((cF x8)->(((cG x8)->False)->((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))))
% Found (and_rect30 (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11)))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))
% Found ((and_rect3 ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11)))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))
% Found (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11)))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))
% Found (fun (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))
% Found (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))))) as proof of (((and (cF x8)) ((cG x8)->False))->((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))))
% Found (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))))) as proof of (forall (x:fofType), (((and (cF x)) ((cG x)->False))->((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))))
% Found (ex_ind00 (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11)))))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))
% Found ((ex_ind0 ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11)))))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))
% Found (((fun (P:Prop) (x8:(forall (x:fofType), (((and (cF x)) ((cG x)->False))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11)))))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))
% Found (fun (x7:(forall (Xx:fofType), ((cF Xx)->(cH Xx))))=> (((fun (P:Prop) (x8:(forall (x:fofType), (((and (cF x)) ((cG x)->False))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))))))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))
% Found (fun (x6:((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (x7:(forall (Xx:fofType), ((cF Xx)->(cH Xx))))=> (((fun (P:Prop) (x8:(forall (x:fofType), (((and (cF x)) ((cG x)->False))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))))))) as proof of ((forall (Xx:fofType), ((cF Xx)->(cH Xx)))->((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))))
% Found (fun (x6:((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (x7:(forall (Xx:fofType), ((cF Xx)->(cH Xx))))=> (((fun (P:Prop) (x8:(forall (x:fofType), (((and (cF x)) ((cG x)->False))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))))))) as proof of (((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))->((forall (Xx:fofType), ((cF Xx)->(cH Xx)))->((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))))
% Found (and_rect20 (fun (x6:((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (x7:(forall (Xx:fofType), ((cF Xx)->(cH Xx))))=> (((fun (P:Prop) (x8:(forall (x:fofType), (((and (cF x)) ((cG x)->False))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11)))))))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))
% Found ((and_rect2 ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x6:((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (x7:(forall (Xx:fofType), ((cF Xx)->(cH Xx))))=> (((fun (P:Prop) (x8:(forall (x:fofType), (((and (cF x)) ((cG x)->False))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11)))))))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))
% Found (((fun (P:Type) (x6:(((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))->((forall (Xx:fofType), ((cF Xx)->(cH Xx)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx)))) P) x6) x4)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x6:((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (x7:(forall (Xx:fofType), ((cF Xx)->(cH Xx))))=> (((fun (P:Prop) (x8:(forall (x:fofType), (((and (cF x)) ((cG x)->False))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11)))))))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))
% Found (fun (x5:(forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))->((forall (Xx:fofType), ((cF Xx)->(cH Xx)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx)))) P) x6) x4)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x6:((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (x7:(forall (Xx:fofType), ((cF Xx)->(cH Xx))))=> (((fun (P:Prop) (x8:(forall (x:fofType), (((and (cF x)) ((cG x)->False))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))))))))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))
% Found (fun (x4:((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (x5:(forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))->((forall (Xx:fofType), ((cF Xx)->(cH Xx)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx)))) P) x6) x4)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x6:((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (x7:(forall (Xx:fofType), ((cF Xx)->(cH Xx))))=> (((fun (P:Prop) (x8:(forall (x:fofType), (((and (cF x)) ((cG x)->False))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))))))))) as proof of ((forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx)))->((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))))
% Found (fun (x4:((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (x5:(forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))->((forall (Xx:fofType), ((cF Xx)->(cH Xx)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx)))) P) x6) x4)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x6:((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (x7:(forall (Xx:fofType), ((cF Xx)->(cH Xx))))=> (((fun (P:Prop) (x8:(forall (x:fofType), (((and (cF x)) ((cG x)->False))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))))))))) as proof of (((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))->((forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx)))->((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))))
% Found (and_rect10 (fun (x4:((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (x5:(forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))->((forall (Xx:fofType), ((cF Xx)->(cH Xx)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx)))) P) x6) x4)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x6:((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (x7:(forall (Xx:fofType), ((cF Xx)->(cH Xx))))=> (((fun (P:Prop) (x8:(forall (x:fofType), (((and (cF x)) ((cG x)->False))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11)))))))))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))
% Found ((and_rect1 ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x4:((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (x5:(forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))->((forall (Xx:fofType), ((cF Xx)->(cH Xx)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx)))) P) x6) x4)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x6:((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (x7:(forall (Xx:fofType), ((cF Xx)->(cH Xx))))=> (((fun (P:Prop) (x8:(forall (x:fofType), (((and (cF x)) ((cG x)->False))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11)))))))))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))
% Found (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))->((forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx)))) P) x4) x2)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x4:((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (x5:(forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))->((forall (Xx:fofType), ((cF Xx)->(cH Xx)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx)))) P) x6) x4)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x6:((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (x7:(forall (Xx:fofType), ((cF Xx)->(cH Xx))))=> (((fun (P:Prop) (x8:(forall (x:fofType), (((and (cF x)) ((cG x)->False))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11)))))))))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))
% Found (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))->((forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx)))) P) x4) x2)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x4:((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (x5:(forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))->((forall (Xx:fofType), ((cF Xx)->(cH Xx)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx)))) P) x6) x4)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x6:((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (x7:(forall (Xx:fofType), ((cF Xx)->(cH Xx))))=> (((fun (P:Prop) (x8:(forall (x:fofType), (((and (cF x)) ((cG x)->False))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11)))))))))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))
% Found (((x30 (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))->((forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx)))) P) x4) x2)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x4:((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (x5:(forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))->((forall (Xx:fofType), ((cF Xx)->(cH Xx)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx)))) P) x6) x4)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x6:((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (x7:(forall (Xx:fofType), ((cF Xx)->(cH Xx))))=> (((fun (P:Prop) (x8:(forall (x:fofType), (((and (cF x)) ((cG x)->False))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))))))))))) x1) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))->((forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx)))) P) x4) x2)) (cH Xx)) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))))))) as proof of False
% Found ((((fun (x4:((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))))=> ((x3 x4) Xx)) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> (((fun (P:Prop) (x8:(forall (x:fofType), (((and (cF x)) ((cG x)->False))->P)))=> (((((ex_ind fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))))))))))) x1) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) (cH Xx)) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))))))) as proof of False
% Found (fun (x3:(((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False)))))=> ((((fun (x4:((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))))=> ((x3 x4) Xx)) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> (((fun (P:Prop) (x8:(forall (x:fofType), (((and (cF x)) ((cG x)->False))->P)))=> (((((ex_ind fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))))))))))) x1) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) (cH Xx)) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))))))) as proof of False
% Found (fun (x2:((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (x3:(((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False)))))=> ((((fun (x4:((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))))=> ((x3 x4) Xx)) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> (((fun (P:Prop) (x8:(forall (x:fofType), (((and (cF x)) ((cG x)->False))->P)))=> (((((ex_ind fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))))))))))) x1) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) (cH Xx)) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))))))) as proof of ((((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False))))->False)
% Found (fun (x2:((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (x3:(((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False)))))=> ((((fun (x4:((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))))=> ((x3 x4) Xx)) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> (((fun (P:Prop) (x8:(forall (x:fofType), (((and (cF x)) ((cG x)->False))->P)))=> (((((ex_ind fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))))))))))) x1) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) (cH Xx)) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))))))) as proof of (((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))->((((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False))))->False))
% Found (and_rect00 (fun (x2:((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (x3:(((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False)))))=> ((((fun (x4:((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))))=> ((x3 x4) Xx)) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> (((fun (P:Prop) (x8:(forall (x:fofType), (((and (cF x)) ((cG x)->False))->P)))=> (((((ex_ind fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))))))))))) x1) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) (cH Xx)) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))))))))) as proof of False
% Found ((and_rect0 False) (fun (x2:((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (x3:(((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False)))))=> ((((fun (x4:((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))))=> ((x3 x4) Xx)) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> (((fun (P:Prop) (x8:(forall (x:fofType), (((and (cF x)) ((cG x)->False))->P)))=> (((((ex_ind fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))))))))))) x1) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) (cH Xx)) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))))))))) as proof of False
% Found (((fun (P:Type) (x2:(((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))->((((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False))))->P)))=> (((((and_rect ((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False))))) P) x2) x)) False) (fun (x2:((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (x3:(((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False)))))=> ((((fun (x4:((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))))=> ((x3 x4) Xx)) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> (((fun (P:Prop) (x8:(forall (x0:fofType), (((and (cF x0)) ((cG x0)->False))->P)))=> (((((ex_ind fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))))))))))) x1) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) (cH Xx)) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))))))))) as proof of False
% Found (fun (x1:(cI Xx))=> (((fun (P:Type) (x2:(((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))->((((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False))))->P)))=> (((((and_rect ((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False))))) P) x2) x)) False) (fun (x2:((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (x3:(((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False)))))=> ((((fun (x4:((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))))=> ((x3 x4) Xx)) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> (((fun (P:Prop) (x8:(forall (x0:fofType), (((and (cF x0)) ((cG x0)->False))->P)))=> (((((ex_ind fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))))))))))) x1) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) (cH Xx)) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))))))))) as proof of False
% Found (fun (x0:(cJ Xx)) (x1:(cI Xx))=> (((fun (P:Type) (x2:(((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))->((((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False))))->P)))=> (((((and_rect ((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False))))) P) x2) x)) False) (fun (x2:((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (x3:(((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False)))))=> ((((fun (x4:((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))))=> ((x3 x4) Xx)) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> (((fun (P:Prop) (x8:(forall (x0:fofType), (((and (cF x0)) ((cG x0)->False))->P)))=> (((((ex_ind fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))))))))))) x1) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) (cH Xx)) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))))))))) as proof of ((cI Xx)->False)
% Found (fun (Xx:fofType) (x0:(cJ Xx)) (x1:(cI Xx))=> (((fun (P:Type) (x2:(((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))->((((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False))))->P)))=> (((((and_rect ((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False))))) P) x2) x)) False) (fun (x2:((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (x3:(((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False)))))=> ((((fun (x4:((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))))=> ((x3 x4) Xx)) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> (((fun (P:Prop) (x8:(forall (x0:fofType), (((and (cF x0)) ((cG x0)->False))->P)))=> (((((ex_ind fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))))))))))) x1) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) (cH Xx)) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))))))))) as proof of ((cJ Xx)->((cI Xx)->False))
% Found (fun (x:((and ((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False)))))) (Xx:fofType) (x0:(cJ Xx)) (x1:(cI Xx))=> (((fun (P:Type) (x2:(((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))->((((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False))))->P)))=> (((((and_rect ((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False))))) P) x2) x)) False) (fun (x2:((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (x3:(((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False)))))=> ((((fun (x4:((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))))=> ((x3 x4) Xx)) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> (((fun (P:Prop) (x8:(forall (x0:fofType), (((and (cF x0)) ((cG x0)->False))->P)))=> (((((ex_ind fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))))))))))) x1) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) (cH Xx)) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))))))))) as proof of (forall (Xx:fofType), ((cJ Xx)->((cI Xx)->False)))
% Found (fun (x:((and ((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False)))))) (Xx:fofType) (x0:(cJ Xx)) (x1:(cI Xx))=> (((fun (P:Type) (x2:(((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))->((((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False))))->P)))=> (((((and_rect ((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False))))) P) x2) x)) False) (fun (x2:((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (x3:(((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False)))))=> ((((fun (x4:((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))))=> ((x3 x4) Xx)) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> (((fun (P:Prop) (x8:(forall (x0:fofType), (((and (cF x0)) ((cG x0)->False))->P)))=> (((((ex_ind fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))))))))))) x1) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) (cH Xx)) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1))))))))))) as proof of (((and ((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False)))))->(forall (Xx:fofType), ((cJ Xx)->((cI Xx)->False))))
% Got proof (fun (x:((and ((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False)))))) (Xx:fofType) (x0:(cJ Xx)) (x1:(cI Xx))=> (((fun (P:Type) (x2:(((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))->((((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False))))->P)))=> (((((and_rect ((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False))))) P) x2) x)) False) (fun (x2:((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (x3:(((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False)))))=> ((((fun (x4:((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))))=> ((x3 x4) Xx)) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> (((fun (P:Prop) (x8:(forall (x0:fofType), (((and (cF x0)) ((cG x0)->False))->P)))=> (((((ex_ind fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))))))))))) x1) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) (cH Xx)) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))))))))))
% Time elapsed = 201.292597s
% node=28525 cost=2020.000000 depth=48
% ::::::::::::::::::::::
% % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% (fun (x:((and ((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False)))))) (Xx:fofType) (x0:(cJ Xx)) (x1:(cI Xx))=> (((fun (P:Type) (x2:(((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))->((((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False))))->P)))=> (((((and_rect ((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False))))) P) x2) x)) False) (fun (x2:((and ((and ((ex fofType) (fun (Xx:fofType)=> ((and (cF Xx)) ((cG Xx)->False))))) (forall (Xx:fofType), ((cF Xx)->(cH Xx))))) (forall (Xx:fofType), (((and (cJ Xx)) (cI Xx))->(cF Xx))))) (x3:(((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False))))->(forall (Xx:fofType), ((cI Xx)->((cH Xx)->False)))))=> ((((fun (x4:((ex fofType) (fun (Xx:fofType)=> ((and (cH Xx)) ((cG Xx)->False)))))=> ((x3 x4) Xx)) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> (((fun (P:Prop) (x8:(forall (x0:fofType), (((and (cF x0)) ((cG x0)->False))->P)))=> (((((ex_ind fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False)))) P) x8) x6)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x8:fofType) (x9:((and (cF x8)) ((cG x8)->False)))=> (((fun (P:Type) (x10:((cF x8)->(((cG x8)->False)->P)))=> (((((and_rect (cF x8)) ((cG x8)->False)) P) x10) x9)) ((ex fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False))))) (fun (x10:(cF x8)) (x11:((cG x8)->False))=> ((((ex_intro fofType) (fun (Xx0:fofType)=> ((and (cH Xx0)) ((cG Xx0)->False)))) x8) ((((conj (cH x8)) ((cG x8)->False)) ((x7 x8) x10)) x11))))))))))) x1) (((fun (P:Type) (x4:(((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))->((forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))->P)))=> (((((and_rect ((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0)))) P) x4) x2)) (cH Xx)) (fun (x4:((and ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))) (x5:(forall (Xx0:fofType), (((and (cJ Xx0)) (cI Xx0))->(cF Xx0))))=> (((fun (P:Type) (x6:(((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))->((forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))->P)))=> (((((and_rect ((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (forall (Xx0:fofType), ((cF Xx0)->(cH Xx0)))) P) x6) x4)) (cH Xx)) (fun (x6:((ex fofType) (fun (Xx0:fofType)=> ((and (cF Xx0)) ((cG Xx0)->False))))) (x7:(forall (Xx0:fofType), ((cF Xx0)->(cH Xx0))))=> ((x7 Xx) ((x5 Xx) (((fun (B:Prop)=> (((conj (cJ Xx)) B) x0)) (cI Xx)) x1)))))))))))
% % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% EOF
%------------------------------------------------------------------------------