cocATP---0.2.0.THM-Prf.s

%------------------------------------------------------------------------------
% File     : cocATP---0.2.0
% Problem  : SEU891^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 : n091.star.cs.uiowa.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz
% Memory   : 32286.75MB
% OS       : Linux 2.6.32-431.20.3.el6.x86_64
% CPULimit : 300s
% DateTime : Thu Jul 17 13:33:20 EDT 2014

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

% Comments : 
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % Problem  : SEU891^5 : TPTP v6.1.0. Released v4.0.0.
% % Command  : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p
% % Computer : n091.star.cs.uiowa.edu
% % Model    : x86_64 x86_64
% % CPU      : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% % Memory   : 32286.75MB
% % OS       : Linux 2.6.32-431.20.3.el6.x86_64
% % CPULimit : 300
% % DateTime : Thu Jul 17 11:41:06 CDT 2014
% % CPUTime  : 76.58 
% 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 0x24660e0>, <kernel.Type object at 0x24667e8>) of role type named b_type
% Using role type
% Declaring b:Type
% FOF formula (<kernel.Constant object at 0x2466dd0>, <kernel.Type object at 0x2412b00>) of role type named a_type
% Using role type
% Declaring a:Type
% FOF formula (<kernel.Constant object at 0x2412950>, <kernel.DependentProduct object at 0x2411cf8>) of role type named cF
% Using role type
% Declaring cF:(b->a)
% FOF formula (<kernel.Constant object at 0x24667e8>, <kernel.DependentProduct object at 0x2411d40>) of role type named cS
% Using role type
% Declaring cS:(b->Prop)
% FOF formula (<kernel.Constant object at 0x2466dd0>, <kernel.DependentProduct object at 0x2411488>) of role type named cR
% Using role type
% Declaring cR:(b->Prop)
% FOF formula (forall (Xx:a), (((or ((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))) ((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))))->((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))))) of role conjecture named cTHM34B_pme
% Conjecture to prove = (forall (Xx:a), (((or ((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))) ((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))))->((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))))):Prop
% Parameter b_DUMMY:b.
% Parameter a_DUMMY:a.
% We need to prove ['(forall (Xx:a), (((or ((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))) ((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))))->((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))))']
% Parameter b:Type.
% Parameter a:Type.
% Parameter cF:(b->a).
% Parameter cS:(b->Prop).
% Parameter cR:(b->Prop).
% Trying to prove (forall (Xx:a), (((or ((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))) ((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))))->((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))))
% Found eta_expansion0000:=(eta_expansion000 (ex b)):(((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->((ex b) (fun (x:b)=> ((and (cR x)) (((eq a) Xx) (cF x))))))
% Found (eta_expansion000 (ex b)) as proof of (P (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((eta_expansion00 (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion0 Prop) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((((eta_expansion b) Prop) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((((eta_expansion b) Prop) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found eta_expansion0000:=(eta_expansion000 (ex b)):(((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))->((ex b) (fun (x:b)=> ((and (cS x)) (((eq a) Xx) (cF x))))))
% Found (eta_expansion000 (ex b)) as proof of (P (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((eta_expansion00 (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion0 Prop) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((((eta_expansion b) Prop) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((((eta_expansion b) Prop) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found eta_expansion0000:=(eta_expansion000 (ex b)):(((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))->((ex b) (fun (x:b)=> ((and (cS x)) (((eq a) Xx) (cF x))))))
% Found (eta_expansion000 (ex b)) as proof of (P (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((eta_expansion00 (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion0 Prop) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((((eta_expansion b) Prop) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((((eta_expansion b) Prop) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found eta_expansion0000:=(eta_expansion000 (ex b)):(((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->((ex b) (fun (x:b)=> ((and (cR x)) (((eq a) Xx) (cF x))))))
% Found (eta_expansion000 (ex b)) as proof of (P (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((eta_expansion00 (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion0 Prop) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((((eta_expansion b) Prop) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((((eta_expansion b) Prop) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found eta_expansion0000:=(eta_expansion000 (ex b)):(((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))->((ex b) (fun (x:b)=> ((and (cS x)) (((eq a) Xx) (cF x))))))
% Found (eta_expansion000 (ex b)) as proof of (P (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((eta_expansion00 (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion0 Prop) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((((eta_expansion b) Prop) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((((eta_expansion b) Prop) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found eta_expansion0000:=(eta_expansion000 (ex b)):(((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->((ex b) (fun (x:b)=> ((and (cR x)) (((eq a) Xx) (cF x))))))
% Found (eta_expansion000 (ex b)) as proof of (P (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((eta_expansion00 (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion0 Prop) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((((eta_expansion b) Prop) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((((eta_expansion b) Prop) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found eta_expansion_dep000:=(eta_expansion_dep00 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))):(((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) (fun (x:b)=> ((and ((or (cR x)) (cS x))) (((eq a) Xx) (cF x)))))
% Found (eta_expansion_dep00 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found ((eta_expansion_dep0 (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion_dep b) (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion_dep b) (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion_dep b) (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found eq_ref00:=(eq_ref0 (f x0)):(((eq Prop) (f x0)) (f x0))
% Found (eq_ref0 (f x0)) as proof of (((eq Prop) (f x0)) ((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0))))
% Found ((eq_ref Prop) (f x0)) as proof of (((eq Prop) (f x0)) ((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0))))
% Found ((eq_ref Prop) (f x0)) as proof of (((eq Prop) (f x0)) ((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0))))
% Found (fun (x0:b)=> ((eq_ref Prop) (f x0))) as proof of (((eq Prop) (f x0)) ((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0))))
% Found (fun (x0:b)=> ((eq_ref Prop) (f x0))) as proof of (forall (x:b), (((eq Prop) (f x)) ((and ((or (cR x)) (cS x))) (((eq a) Xx) (cF x)))))
% Found eq_ref00:=(eq_ref0 (f x0)):(((eq Prop) (f x0)) (f x0))
% Found (eq_ref0 (f x0)) as proof of (((eq Prop) (f x0)) ((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0))))
% Found ((eq_ref Prop) (f x0)) as proof of (((eq Prop) (f x0)) ((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0))))
% Found ((eq_ref Prop) (f x0)) as proof of (((eq Prop) (f x0)) ((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0))))
% Found (fun (x0:b)=> ((eq_ref Prop) (f x0))) as proof of (((eq Prop) (f x0)) ((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0))))
% Found (fun (x0:b)=> ((eq_ref Prop) (f x0))) as proof of (forall (x:b), (((eq Prop) (f x)) ((and ((or (cR x)) (cS x))) (((eq a) Xx) (cF x)))))
% Found eq_ref000:=(eq_ref00 (ex b)):(((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))->((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))))
% Found (eq_ref00 (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))->(P b0))
% Found ((eq_ref0 (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))->(P b0))
% Found (((eq_ref (b->Prop)) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))->(P b0))
% Found (((eq_ref (b->Prop)) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))->(P b0))
% Found (((eq_ref (b->Prop)) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))->(P b0))
% Found eta_expansion_dep0000:=(eta_expansion_dep000 (ex b)):(((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->((ex b) (fun (x:b)=> ((and (cR x)) (((eq a) Xx) (cF x))))))
% Found (eta_expansion_dep000 (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->(P b0))
% Found ((eta_expansion_dep00 (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->(P b0))
% Found (((eta_expansion_dep0 (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->(P b0))
% Found ((((eta_expansion_dep b) (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->(P b0))
% Found ((((eta_expansion_dep b) (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->(P b0))
% Found ((((eta_expansion_dep b) (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->(P b0))
% Found eta_expansion_dep0000:=(eta_expansion_dep000 (ex b)):(((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->((ex b) (fun (x:b)=> ((and (cR x)) (((eq a) Xx) (cF x))))))
% Found (eta_expansion_dep000 (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->(P f))
% Found ((eta_expansion_dep00 (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->(P f))
% Found (((eta_expansion_dep0 (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->(P f))
% Found ((((eta_expansion_dep b) (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->(P f))
% Found ((((eta_expansion_dep b) (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->(P f))
% Found ((((eta_expansion_dep b) (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->(P f))
% Found eta_expansion0000:=(eta_expansion000 (ex b)):(((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))->((ex b) (fun (x:b)=> ((and (cS x)) (((eq a) Xx) (cF x))))))
% Found (eta_expansion000 (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))->(P f))
% Found ((eta_expansion00 (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))->(P f))
% Found (((eta_expansion0 Prop) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))->(P f))
% Found ((((eta_expansion b) Prop) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))->(P f))
% Found ((((eta_expansion b) Prop) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))->(P f))
% Found ((((eta_expansion b) Prop) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))->(P f))
% Found eq_ref000:=(eq_ref00 (ex b)):(((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))))
% Found (eq_ref00 (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->(P f))
% Found ((eq_ref0 (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->(P f))
% Found (((eq_ref (b->Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->(P f))
% Found (((eq_ref (b->Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->(P f))
% Found (((eq_ref (b->Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->(P f))
% Found x0:((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Instantiate: f:=(fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))):(b->Prop)
% Found (fun (x0:((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))))=> x0) as proof of (P f)
% Found (fun (x0:((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))))=> x0) as proof of (((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))->(P f))
% Found x0:((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Instantiate: b0:=(fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))):(b->Prop)
% Found x0 as proof of (P b0)
% Found eq_ref00:=(eq_ref0 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))):(((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (eq_ref0 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found ((eq_ref (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found ((eq_ref (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found ((eq_ref (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found x0:((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Instantiate: b0:=(fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))):(b->Prop)
% Found x0 as proof of (P b0)
% Found eq_ref00:=(eq_ref0 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))):(((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (eq_ref0 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found ((eq_ref (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found ((eq_ref (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found ((eq_ref (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found x0:((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Instantiate: f:=(fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))):(b->Prop)
% Found x0 as proof of (P f)
% Found x0:((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Instantiate: f:=(fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))):(b->Prop)
% Found x0 as proof of (P f)
% Found x0:((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Instantiate: f:=(fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))):(b->Prop)
% Found x0 as proof of (P f)
% Found x0:((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Instantiate: f:=(fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))):(b->Prop)
% Found x0 as proof of (P f)
% Found eq_ref00:=(eq_ref0 (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))):(((eq (b->Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found (eq_ref0 (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) b0)
% Found ((eq_ref (b->Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) b0)
% Found ((eq_ref (b->Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) b0)
% Found ((eq_ref (b->Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) b0)
% Found eta_expansion000:=(eta_expansion00 b0):(((eq (b->Prop)) b0) (fun (x:b)=> (b0 x)))
% Found (eta_expansion00 b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found ((eta_expansion0 Prop) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion b) Prop) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion b) Prop) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion b) Prop) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found eq_ref00:=(eq_ref0 (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))):(((eq (b->Prop)) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found (eq_ref0 (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) b0)
% Found ((eq_ref (b->Prop)) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) b0)
% Found ((eq_ref (b->Prop)) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) b0)
% Found ((eq_ref (b->Prop)) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) b0)
% Found eta_expansion000:=(eta_expansion00 b0):(((eq (b->Prop)) b0) (fun (x:b)=> (b0 x)))
% Found (eta_expansion00 b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found ((eta_expansion0 Prop) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion b) Prop) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion b) Prop) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion b) Prop) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found eq_ref00:=(eq_ref0 (f x1)):(((eq Prop) (f x1)) (f x1))
% Found (eq_ref0 (f x1)) as proof of (((eq Prop) (f x1)) ((and ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))))
% Found ((eq_ref Prop) (f x1)) as proof of (((eq Prop) (f x1)) ((and ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))))
% Found ((eq_ref Prop) (f x1)) as proof of (((eq Prop) (f x1)) ((and ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))))
% Found (fun (x1:b)=> ((eq_ref Prop) (f x1))) as proof of (((eq Prop) (f x1)) ((and ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))))
% Found (fun (x1:b)=> ((eq_ref Prop) (f x1))) as proof of (forall (x:b), (((eq Prop) (f x)) ((and ((or (cR x)) (cS x))) (((eq a) Xx) (cF x)))))
% Found eq_ref00:=(eq_ref0 (f x1)):(((eq Prop) (f x1)) (f x1))
% Found (eq_ref0 (f x1)) as proof of (((eq Prop) (f x1)) ((and ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))))
% Found ((eq_ref Prop) (f x1)) as proof of (((eq Prop) (f x1)) ((and ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))))
% Found ((eq_ref Prop) (f x1)) as proof of (((eq Prop) (f x1)) ((and ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))))
% Found (fun (x1:b)=> ((eq_ref Prop) (f x1))) as proof of (((eq Prop) (f x1)) ((and ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))))
% Found (fun (x1:b)=> ((eq_ref Prop) (f x1))) as proof of (forall (x:b), (((eq Prop) (f x)) ((and ((or (cR x)) (cS x))) (((eq a) Xx) (cF x)))))
% Found eq_ref00:=(eq_ref0 (f x1)):(((eq Prop) (f x1)) (f x1))
% Found (eq_ref0 (f x1)) as proof of (((eq Prop) (f x1)) ((and ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))))
% Found ((eq_ref Prop) (f x1)) as proof of (((eq Prop) (f x1)) ((and ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))))
% Found ((eq_ref Prop) (f x1)) as proof of (((eq Prop) (f x1)) ((and ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))))
% Found (fun (x1:b)=> ((eq_ref Prop) (f x1))) as proof of (((eq Prop) (f x1)) ((and ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))))
% Found (fun (x1:b)=> ((eq_ref Prop) (f x1))) as proof of (forall (x:b), (((eq Prop) (f x)) ((and ((or (cR x)) (cS x))) (((eq a) Xx) (cF x)))))
% Found eq_ref00:=(eq_ref0 (f x1)):(((eq Prop) (f x1)) (f x1))
% Found (eq_ref0 (f x1)) as proof of (((eq Prop) (f x1)) ((and ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))))
% Found ((eq_ref Prop) (f x1)) as proof of (((eq Prop) (f x1)) ((and ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))))
% Found ((eq_ref Prop) (f x1)) as proof of (((eq Prop) (f x1)) ((and ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))))
% Found (fun (x1:b)=> ((eq_ref Prop) (f x1))) as proof of (((eq Prop) (f x1)) ((and ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))))
% Found (fun (x1:b)=> ((eq_ref Prop) (f x1))) as proof of (forall (x:b), (((eq Prop) (f x)) ((and ((or (cR x)) (cS x))) (((eq a) Xx) (cF x)))))
% Found eq_ref000:=(eq_ref00 (ex b)):(((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))))
% Found (eq_ref00 (ex b)) as proof of (P (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((eq_ref0 (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found (((eq_ref (b->Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found (((eq_ref (b->Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found eta_expansion_dep000:=(eta_expansion_dep00 (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))):(((eq (b->Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) (fun (x:b)=> ((and (cR x)) (((eq a) Xx) (cF x)))))
% Found (eta_expansion_dep00 (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) b0)
% Found ((eta_expansion_dep0 (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion_dep b) (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion_dep b) (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion_dep b) (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) b0)
% Found eta_expansion000:=(eta_expansion00 b0):(((eq (b->Prop)) b0) (fun (x:b)=> (b0 x)))
% Found (eta_expansion00 b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found ((eta_expansion0 Prop) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion b) Prop) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion b) Prop) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion b) Prop) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found eq_ref000:=(eq_ref00 (ex b)):(((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))->((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))))
% Found (eq_ref00 (ex b)) as proof of (P (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((eq_ref0 (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found (((eq_ref (b->Prop)) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found (((eq_ref (b->Prop)) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) (ex b)) as proof of (P (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found eta_expansion_dep000:=(eta_expansion_dep00 (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))):(((eq (b->Prop)) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) (fun (x:b)=> ((and (cS x)) (((eq a) Xx) (cF x)))))
% Found (eta_expansion_dep00 (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) b0)
% Found ((eta_expansion_dep0 (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion_dep b) (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion_dep b) (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion_dep b) (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) b0)
% Found eta_expansion000:=(eta_expansion00 b0):(((eq (b->Prop)) b0) (fun (x:b)=> (b0 x)))
% Found (eta_expansion00 b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found ((eta_expansion0 Prop) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion b) Prop) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion b) Prop) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion b) Prop) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found x5:(((eq a) Xx) (cF x2))
% Instantiate: x0:=x2:b
% Found x5 as proof of (((eq a) Xx) (cF x0))
% Found x5:(((eq a) Xx) (cF x2))
% Instantiate: x0:=x2:b
% Found x5 as proof of (((eq a) Xx) (cF x0))
% Found eq_ref000:=(eq_ref00 P):((P Xx)->(P Xx))
% Found (eq_ref00 P) as proof of (P0 Xx)
% Found ((eq_ref0 Xx) P) as proof of (P0 Xx)
% Found (((eq_ref a) Xx) P) as proof of (P0 Xx)
% Found (((eq_ref a) Xx) P) as proof of (P0 Xx)
% Found x4:(((eq a) Xx) (cF x1))
% Instantiate: x5:=x1:b
% Found x4 as proof of (((eq a) Xx) (cF x5))
% Found x4:(((eq a) Xx) (cF x1))
% Instantiate: x5:=x1:b
% Found x4 as proof of (((eq a) Xx) (cF x5))
% Found eq_ref00:=(eq_ref0 Xx):(((eq a) Xx) Xx)
% Found (eq_ref0 Xx) as proof of (((eq a) Xx) b0)
% Found ((eq_ref a) Xx) as proof of (((eq a) Xx) b0)
% Found ((eq_ref a) Xx) as proof of (((eq a) Xx) b0)
% Found ((eq_ref a) Xx) as proof of (((eq a) Xx) b0)
% Found eq_ref00:=(eq_ref0 b0):(((eq a) b0) b0)
% Found (eq_ref0 b0) as proof of (((eq a) b0) (cF x0))
% Found ((eq_ref a) b0) as proof of (((eq a) b0) (cF x0))
% Found ((eq_ref a) b0) as proof of (((eq a) b0) (cF x0))
% Found ((eq_ref a) b0) as proof of (((eq a) b0) (cF x0))
% Found x0:((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Instantiate: b0:=(fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))):(b->Prop)
% Found x0 as proof of (P b0)
% Found x0:((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Instantiate: b0:=(fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))):(b->Prop)
% Found x0 as proof of (P b0)
% Found or_introl000:=(or_introl00 (cS x0)):((or (cR x0)) (cS x0))
% Found (or_introl00 (cS x0)) as proof of ((or (cR x0)) (cS x0))
% Found ((fun (B:Prop)=> ((or_introl0 B) x4)) (cS x0)) as proof of ((or (cR x0)) (cS x0))
% Found ((fun (B:Prop)=> (((or_introl (cR x0)) B) x4)) (cS x0)) as proof of ((or (cR x0)) (cS x0))
% Found ((fun (B:Prop)=> (((or_introl (cR x0)) B) x4)) (cS x0)) as proof of ((or (cR x0)) (cS x0))
% Found (conj00 ((fun (B:Prop)=> (((or_introl (cR x0)) B) x4)) (cS x0))) as proof of ((((eq a) Xx) (cF x2))->((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0))))
% Found ((conj0 (((eq a) Xx) (cF x2))) ((fun (B:Prop)=> (((or_introl (cR x0)) B) x4)) (cS x0))) as proof of ((((eq a) Xx) (cF x2))->((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0))))
% Found (((conj ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x2))) ((fun (B:Prop)=> (((or_introl (cR x0)) B) x4)) (cS x0))) as proof of ((((eq a) Xx) (cF x2))->((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0))))
% Found (((conj ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x2))) ((fun (B:Prop)=> (((or_introl (cR x0)) B) x4)) (cS x0))) as proof of ((((eq a) Xx) (cF x2))->((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0))))
% Found (fun (x4:(cR x2))=> (((conj ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x2))) ((fun (B:Prop)=> (((or_introl (cR x0)) B) x4)) (cS x0)))) as proof of ((((eq a) Xx) (cF x2))->((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0))))
% Found (fun (x4:(cR x2))=> (((conj ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x2))) ((fun (B:Prop)=> (((or_introl (cR x0)) B) x4)) (cS x0)))) as proof of ((cR x2)->((((eq a) Xx) (cF x2))->((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0)))))
% Found (and_rect00 (fun (x4:(cR x2))=> (((conj ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x2))) ((fun (B:Prop)=> (((or_introl (cR x0)) B) x4)) (cS x0))))) as proof of ((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0)))
% Found ((and_rect0 ((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0)))) (fun (x4:(cR x2))=> (((conj ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x2))) ((fun (B:Prop)=> (((or_introl (cR x0)) B) x4)) (cS x0))))) as proof of ((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0)))
% Found (((fun (P:Type) (x4:((cR x2)->((((eq a) Xx) (cF x2))->P)))=> (((((and_rect (cR x2)) (((eq a) Xx) (cF x2))) P) x4) x3)) ((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0)))) (fun (x4:(cR x2))=> (((conj ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x2))) ((fun (B:Prop)=> (((or_introl (cR x0)) B) x4)) (cS x0))))) as proof of ((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0)))
% Found (fun (x3:((and (cR x2)) (((eq a) Xx) (cF x2))))=> (((fun (P:Type) (x4:((cR x2)->((((eq a) Xx) (cF x2))->P)))=> (((((and_rect (cR x2)) (((eq a) Xx) (cF x2))) P) x4) x3)) ((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0)))) (fun (x4:(cR x2))=> (((conj ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x2))) ((fun (B:Prop)=> (((or_introl (cR x0)) B) x4)) (cS x0)))))) as proof of ((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0)))
% Found eta_expansion000:=(eta_expansion00 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))):(((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) (fun (x:b)=> ((and ((or (cR x)) (cS x))) (((eq a) Xx) (cF x)))))
% Found (eta_expansion00 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found ((eta_expansion0 Prop) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion b) Prop) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion b) Prop) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion b) Prop) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found eta_expansion000:=(eta_expansion00 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))):(((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) (fun (x:b)=> ((and ((or (cR x)) (cS x))) (((eq a) Xx) (cF x)))))
% Found (eta_expansion00 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found ((eta_expansion0 Prop) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion b) Prop) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion b) Prop) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion b) Prop) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found x5:(((eq a) Xx) (cF x2))
% Instantiate: x1:=x2:b
% Found x5 as proof of (((eq a) Xx) (cF x1))
% Found x5:(((eq a) Xx) (cF x2))
% Instantiate: x1:=x2:b
% Found x5 as proof of (((eq a) Xx) (cF x1))
% Found x5:(((eq a) Xx) (cF x1))
% Instantiate: x3:=x1:b
% Found x5 as proof of (((eq a) Xx) (cF x3))
% Found x5:(((eq a) Xx) (cF x1))
% Instantiate: x3:=x1:b
% Found x5 as proof of (((eq a) Xx) (cF x3))
% Found x0:((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Instantiate: f:=(fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))):(b->Prop)
% Found x0 as proof of (P f)
% Found x0:((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Instantiate: f:=(fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))):(b->Prop)
% Found x0 as proof of (P f)
% Found x0:((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Instantiate: f:=(fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))):(b->Prop)
% Found x0 as proof of (P f)
% Found x0:((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Instantiate: f:=(fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))):(b->Prop)
% Found x0 as proof of (P f)
% Found x5:(((eq a) Xx) (cF x2))
% Instantiate: x0:=x2:b
% Found (fun (x5:(((eq a) Xx) (cF x2)))=> x5) as proof of (((eq a) Xx) (cF x0))
% Found (fun (x4:(cR x2)) (x5:(((eq a) Xx) (cF x2)))=> x5) as proof of ((((eq a) Xx) (cF x2))->(((eq a) Xx) (cF x0)))
% Found (fun (x4:(cR x2)) (x5:(((eq a) Xx) (cF x2)))=> x5) as proof of ((cR x2)->((((eq a) Xx) (cF x2))->(((eq a) Xx) (cF x0))))
% Found (and_rect00 (fun (x4:(cR x2)) (x5:(((eq a) Xx) (cF x2)))=> x5)) as proof of (((eq a) Xx) (cF x0))
% Found ((and_rect0 (((eq a) Xx) (cF x0))) (fun (x4:(cR x2)) (x5:(((eq a) Xx) (cF x2)))=> x5)) as proof of (((eq a) Xx) (cF x0))
% Found (((fun (P:Type) (x4:((cR x2)->((((eq a) Xx) (cF x2))->P)))=> (((((and_rect (cR x2)) (((eq a) Xx) (cF x2))) P) x4) x3)) (((eq a) Xx) (cF x0))) (fun (x4:(cR x2)) (x5:(((eq a) Xx) (cF x2)))=> x5)) as proof of (((eq a) Xx) (cF x0))
% Found (((fun (P:Type) (x4:((cR x2)->((((eq a) Xx) (cF x2))->P)))=> (((((and_rect (cR x2)) (((eq a) Xx) (cF x2))) P) x4) x3)) (((eq a) Xx) (cF x0))) (fun (x4:(cR x2)) (x5:(((eq a) Xx) (cF x2)))=> x5)) as proof of (((eq a) Xx) (cF x0))
% Found or_introl000:=(or_introl00 (cS x0)):((or (cR x0)) (cS x0))
% Found (or_introl00 (cS x0)) as proof of ((or (cR x0)) (cS x0))
% Found ((fun (B:Prop)=> ((or_introl0 B) x4)) (cS x0)) as proof of ((or (cR x0)) (cS x0))
% Found ((fun (B:Prop)=> (((or_introl (cR x0)) B) x4)) (cS x0)) as proof of ((or (cR x0)) (cS x0))
% Found (fun (x5:(((eq a) Xx) (cF x2)))=> ((fun (B:Prop)=> (((or_introl (cR x0)) B) x4)) (cS x0))) as proof of ((or (cR x0)) (cS x0))
% Found (fun (x4:(cR x2)) (x5:(((eq a) Xx) (cF x2)))=> ((fun (B:Prop)=> (((or_introl (cR x0)) B) x4)) (cS x0))) as proof of ((((eq a) Xx) (cF x2))->((or (cR x0)) (cS x0)))
% Found (fun (x4:(cR x2)) (x5:(((eq a) Xx) (cF x2)))=> ((fun (B:Prop)=> (((or_introl (cR x0)) B) x4)) (cS x0))) as proof of ((cR x2)->((((eq a) Xx) (cF x2))->((or (cR x0)) (cS x0))))
% Found (and_rect00 (fun (x4:(cR x2)) (x5:(((eq a) Xx) (cF x2)))=> ((fun (B:Prop)=> (((or_introl (cR x0)) B) x4)) (cS x0)))) as proof of ((or (cR x0)) (cS x0))
% Found ((and_rect0 ((or (cR x0)) (cS x0))) (fun (x4:(cR x2)) (x5:(((eq a) Xx) (cF x2)))=> ((fun (B:Prop)=> (((or_introl (cR x0)) B) x4)) (cS x0)))) as proof of ((or (cR x0)) (cS x0))
% Found (((fun (P:Type) (x4:((cR x2)->((((eq a) Xx) (cF x2))->P)))=> (((((and_rect (cR x2)) (((eq a) Xx) (cF x2))) P) x4) x3)) ((or (cR x0)) (cS x0))) (fun (x4:(cR x2)) (x5:(((eq a) Xx) (cF x2)))=> ((fun (B:Prop)=> (((or_introl (cR x0)) B) x4)) (cS x0)))) as proof of ((or (cR x0)) (cS x0))
% Found (((fun (P:Type) (x4:((cR x2)->((((eq a) Xx) (cF x2))->P)))=> (((((and_rect (cR x2)) (((eq a) Xx) (cF x2))) P) x4) x3)) ((or (cR x0)) (cS x0))) (fun (x4:(cR x2)) (x5:(((eq a) Xx) (cF x2)))=> ((fun (B:Prop)=> (((or_introl (cR x0)) B) x4)) (cS x0)))) as proof of ((or (cR x0)) (cS x0))
% Found ((conj00 (((fun (P:Type) (x4:((cR x2)->((((eq a) Xx) (cF x2))->P)))=> (((((and_rect (cR x2)) (((eq a) Xx) (cF x2))) P) x4) x3)) ((or (cR x0)) (cS x0))) (fun (x4:(cR x2)) (x5:(((eq a) Xx) (cF x2)))=> ((fun (B:Prop)=> (((or_introl (cR x0)) B) x4)) (cS x0))))) (((fun (P:Type) (x4:((cR x2)->((((eq a) Xx) (cF x2))->P)))=> (((((and_rect (cR x2)) (((eq a) Xx) (cF x2))) P) x4) x3)) (((eq a) Xx) (cF x0))) (fun (x4:(cR x2)) (x5:(((eq a) Xx) (cF x2)))=> x5))) as proof of ((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0)))
% Found (((conj0 (((eq a) Xx) (cF x0))) (((fun (P:Type) (x4:((cR x2)->((((eq a) Xx) (cF x2))->P)))=> (((((and_rect (cR x2)) (((eq a) Xx) (cF x2))) P) x4) x3)) ((or (cR x0)) (cS x0))) (fun (x4:(cR x2)) (x5:(((eq a) Xx) (cF x2)))=> ((fun (B:Prop)=> (((or_introl (cR x0)) B) x4)) (cS x0))))) (((fun (P:Type) (x4:((cR x2)->((((eq a) Xx) (cF x2))->P)))=> (((((and_rect (cR x2)) (((eq a) Xx) (cF x2))) P) x4) x3)) (((eq a) Xx) (cF x0))) (fun (x4:(cR x2)) (x5:(((eq a) Xx) (cF x2)))=> x5))) as proof of ((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0)))
% Found ((((conj ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0))) (((fun (P:Type) (x4:((cR x2)->((((eq a) Xx) (cF x2))->P)))=> (((((and_rect (cR x2)) (((eq a) Xx) (cF x2))) P) x4) x3)) ((or (cR x0)) (cS x0))) (fun (x4:(cR x2)) (x5:(((eq a) Xx) (cF x2)))=> ((fun (B:Prop)=> (((or_introl (cR x0)) B) x4)) (cS x0))))) (((fun (P:Type) (x4:((cR x2)->((((eq a) Xx) (cF x2))->P)))=> (((((and_rect (cR x2)) (((eq a) Xx) (cF x2))) P) x4) x3)) (((eq a) Xx) (cF x0))) (fun (x4:(cR x2)) (x5:(((eq a) Xx) (cF x2)))=> x5))) as proof of ((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0)))
% Found (fun (x3:((and (cR x2)) (((eq a) Xx) (cF x2))))=> ((((conj ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0))) (((fun (P:Type) (x4:((cR x2)->((((eq a) Xx) (cF x2))->P)))=> (((((and_rect (cR x2)) (((eq a) Xx) (cF x2))) P) x4) x3)) ((or (cR x0)) (cS x0))) (fun (x4:(cR x2)) (x5:(((eq a) Xx) (cF x2)))=> ((fun (B:Prop)=> (((or_introl (cR x0)) B) x4)) (cS x0))))) (((fun (P:Type) (x4:((cR x2)->((((eq a) Xx) (cF x2))->P)))=> (((((and_rect (cR x2)) (((eq a) Xx) (cF x2))) P) x4) x3)) (((eq a) Xx) (cF x0))) (fun (x4:(cR x2)) (x5:(((eq a) Xx) (cF x2)))=> x5)))) as proof of ((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0)))
% Found x5:(((eq a) Xx) (cF x2))
% Instantiate: x0:=x2:b
% Found (fun (x5:(((eq a) Xx) (cF x2)))=> x5) as proof of (((eq a) Xx) (cF x0))
% Found (fun (x4:(cS x2)) (x5:(((eq a) Xx) (cF x2)))=> x5) as proof of ((((eq a) Xx) (cF x2))->(((eq a) Xx) (cF x0)))
% Found (fun (x4:(cS x2)) (x5:(((eq a) Xx) (cF x2)))=> x5) as proof of ((cS x2)->((((eq a) Xx) (cF x2))->(((eq a) Xx) (cF x0))))
% Found (and_rect00 (fun (x4:(cS x2)) (x5:(((eq a) Xx) (cF x2)))=> x5)) as proof of (((eq a) Xx) (cF x0))
% Found ((and_rect0 (((eq a) Xx) (cF x0))) (fun (x4:(cS x2)) (x5:(((eq a) Xx) (cF x2)))=> x5)) as proof of (((eq a) Xx) (cF x0))
% Found (((fun (P:Type) (x4:((cS x2)->((((eq a) Xx) (cF x2))->P)))=> (((((and_rect (cS x2)) (((eq a) Xx) (cF x2))) P) x4) x3)) (((eq a) Xx) (cF x0))) (fun (x4:(cS x2)) (x5:(((eq a) Xx) (cF x2)))=> x5)) as proof of (((eq a) Xx) (cF x0))
% Found (((fun (P:Type) (x4:((cS x2)->((((eq a) Xx) (cF x2))->P)))=> (((((and_rect (cS x2)) (((eq a) Xx) (cF x2))) P) x4) x3)) (((eq a) Xx) (cF x0))) (fun (x4:(cS x2)) (x5:(((eq a) Xx) (cF x2)))=> x5)) as proof of (((eq a) Xx) (cF x0))
% Found or_intror000:=(or_intror00 x4):((or (cR x0)) (cS x0))
% Found (or_intror00 x4) as proof of ((or (cR x0)) (cS x0))
% Found ((or_intror0 (cS x0)) x4) as proof of ((or (cR x0)) (cS x0))
% Found (((or_intror (cR x0)) (cS x0)) x4) as proof of ((or (cR x0)) (cS x0))
% Found (((or_intror (cR x0)) (cS x0)) x4) as proof of ((or (cR x0)) (cS x0))
% Found (conj00 (((or_intror (cR x0)) (cS x0)) x4)) as proof of ((((eq a) Xx) (cF x2))->((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0))))
% Found ((conj0 (((eq a) Xx) (cF x2))) (((or_intror (cR x0)) (cS x0)) x4)) as proof of ((((eq a) Xx) (cF x2))->((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0))))
% Found (((conj ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x2))) (((or_intror (cR x0)) (cS x0)) x4)) as proof of ((((eq a) Xx) (cF x2))->((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0))))
% Found (((conj ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x2))) (((or_intror (cR x0)) (cS x0)) x4)) as proof of ((((eq a) Xx) (cF x2))->((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0))))
% Found (fun (x4:(cS x2))=> (((conj ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x2))) (((or_intror (cR x0)) (cS x0)) x4))) as proof of ((((eq a) Xx) (cF x2))->((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0))))
% Found (fun (x4:(cS x2))=> (((conj ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x2))) (((or_intror (cR x0)) (cS x0)) x4))) as proof of ((cS x2)->((((eq a) Xx) (cF x2))->((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0)))))
% Found (and_rect00 (fun (x4:(cS x2))=> (((conj ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x2))) (((or_intror (cR x0)) (cS x0)) x4)))) as proof of ((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0)))
% Found ((and_rect0 ((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0)))) (fun (x4:(cS x2))=> (((conj ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x2))) (((or_intror (cR x0)) (cS x0)) x4)))) as proof of ((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0)))
% Found (((fun (P:Type) (x4:((cS x2)->((((eq a) Xx) (cF x2))->P)))=> (((((and_rect (cS x2)) (((eq a) Xx) (cF x2))) P) x4) x3)) ((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0)))) (fun (x4:(cS x2))=> (((conj ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x2))) (((or_intror (cR x0)) (cS x0)) x4)))) as proof of ((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0)))
% Found (fun (x3:((and (cS x2)) (((eq a) Xx) (cF x2))))=> (((fun (P:Type) (x4:((cS x2)->((((eq a) Xx) (cF x2))->P)))=> (((((and_rect (cS x2)) (((eq a) Xx) (cF x2))) P) x4) x3)) ((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0)))) (fun (x4:(cS x2))=> (((conj ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x2))) (((or_intror (cR x0)) (cS x0)) x4))))) as proof of ((and ((or (cR x0)) (cS x0))) (((eq a) Xx) (cF x0)))
% Found eta_expansion_dep0000:=(eta_expansion_dep000 P0):((P0 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))->(P0 (fun (x:b)=> ((and ((or (cR x)) (cS x))) (((eq a) Xx) (cF x))))))
% Found (eta_expansion_dep000 P0) as proof of (P1 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found ((eta_expansion_dep00 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) P0) as proof of (P1 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion_dep0 (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) P0) as proof of (P1 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found ((((eta_expansion_dep b) (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) P0) as proof of (P1 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found ((((eta_expansion_dep b) (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) P0) as proof of (P1 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found eta_expansion_dep0000:=(eta_expansion_dep000 P0):((P0 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))->(P0 (fun (x:b)=> ((and ((or (cR x)) (cS x))) (((eq a) Xx) (cF x))))))
% Found (eta_expansion_dep000 P0) as proof of (P1 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found ((eta_expansion_dep00 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) P0) as proof of (P1 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion_dep0 (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) P0) as proof of (P1 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found ((((eta_expansion_dep b) (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) P0) as proof of (P1 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found ((((eta_expansion_dep b) (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) P0) as proof of (P1 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found eta_expansion_dep0000:=(eta_expansion_dep000 P0):((P0 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))->(P0 (fun (x:b)=> ((and ((or (cR x)) (cS x))) (((eq a) Xx) (cF x))))))
% Found (eta_expansion_dep000 P0) as proof of (P1 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found ((eta_expansion_dep00 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) P0) as proof of (P1 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion_dep0 (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) P0) as proof of (P1 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found ((((eta_expansion_dep b) (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) P0) as proof of (P1 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found ((((eta_expansion_dep b) (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) P0) as proof of (P1 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found eta_expansion_dep0000:=(eta_expansion_dep000 P0):((P0 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))->(P0 (fun (x:b)=> ((and ((or (cR x)) (cS x))) (((eq a) Xx) (cF x))))))
% Found (eta_expansion_dep000 P0) as proof of (P1 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found ((eta_expansion_dep00 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) P0) as proof of (P1 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion_dep0 (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) P0) as proof of (P1 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found ((((eta_expansion_dep b) (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) P0) as proof of (P1 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found ((((eta_expansion_dep b) (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) P0) as proof of (P1 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found eq_ref00:=(eq_ref0 (f x3)):(((eq Prop) (f x3)) (f x3))
% Found (eq_ref0 (f x3)) as proof of (((eq Prop) (f x3)) ((and ((or (cR x3)) (cS x3))) (((eq a) Xx) (cF x3))))
% Found ((eq_ref Prop) (f x3)) as proof of (((eq Prop) (f x3)) ((and ((or (cR x3)) (cS x3))) (((eq a) Xx) (cF x3))))
% Found ((eq_ref Prop) (f x3)) as proof of (((eq Prop) (f x3)) ((and ((or (cR x3)) (cS x3))) (((eq a) Xx) (cF x3))))
% Found (fun (x3:b)=> ((eq_ref Prop) (f x3))) as proof of (((eq Prop) (f x3)) ((and ((or (cR x3)) (cS x3))) (((eq a) Xx) (cF x3))))
% Found (fun (x3:b)=> ((eq_ref Prop) (f x3))) as proof of (forall (x:b), (((eq Prop) (f x)) ((and ((or (cR x)) (cS x))) (((eq a) Xx) (cF x)))))
% Found eq_ref00:=(eq_ref0 (f x3)):(((eq Prop) (f x3)) (f x3))
% Found (eq_ref0 (f x3)) as proof of (((eq Prop) (f x3)) ((and ((or (cR x3)) (cS x3))) (((eq a) Xx) (cF x3))))
% Found ((eq_ref Prop) (f x3)) as proof of (((eq Prop) (f x3)) ((and ((or (cR x3)) (cS x3))) (((eq a) Xx) (cF x3))))
% Found ((eq_ref Prop) (f x3)) as proof of (((eq Prop) (f x3)) ((and ((or (cR x3)) (cS x3))) (((eq a) Xx) (cF x3))))
% Found (fun (x3:b)=> ((eq_ref Prop) (f x3))) as proof of (((eq Prop) (f x3)) ((and ((or (cR x3)) (cS x3))) (((eq a) Xx) (cF x3))))
% Found (fun (x3:b)=> ((eq_ref Prop) (f x3))) as proof of (forall (x:b), (((eq Prop) (f x)) ((and ((or (cR x)) (cS x))) (((eq a) Xx) (cF x)))))
% Found eq_ref00:=(eq_ref0 (f x3)):(((eq Prop) (f x3)) (f x3))
% Found (eq_ref0 (f x3)) as proof of (((eq Prop) (f x3)) ((and ((or (cR x3)) (cS x3))) (((eq a) Xx) (cF x3))))
% Found ((eq_ref Prop) (f x3)) as proof of (((eq Prop) (f x3)) ((and ((or (cR x3)) (cS x3))) (((eq a) Xx) (cF x3))))
% Found ((eq_ref Prop) (f x3)) as proof of (((eq Prop) (f x3)) ((and ((or (cR x3)) (cS x3))) (((eq a) Xx) (cF x3))))
% Found (fun (x3:b)=> ((eq_ref Prop) (f x3))) as proof of (((eq Prop) (f x3)) ((and ((or (cR x3)) (cS x3))) (((eq a) Xx) (cF x3))))
% Found (fun (x3:b)=> ((eq_ref Prop) (f x3))) as proof of (forall (x:b), (((eq Prop) (f x)) ((and ((or (cR x)) (cS x))) (((eq a) Xx) (cF x)))))
% Found eq_ref00:=(eq_ref0 (f x3)):(((eq Prop) (f x3)) (f x3))
% Found (eq_ref0 (f x3)) as proof of (((eq Prop) (f x3)) ((and ((or (cR x3)) (cS x3))) (((eq a) Xx) (cF x3))))
% Found ((eq_ref Prop) (f x3)) as proof of (((eq Prop) (f x3)) ((and ((or (cR x3)) (cS x3))) (((eq a) Xx) (cF x3))))
% Found ((eq_ref Prop) (f x3)) as proof of (((eq Prop) (f x3)) ((and ((or (cR x3)) (cS x3))) (((eq a) Xx) (cF x3))))
% Found (fun (x3:b)=> ((eq_ref Prop) (f x3))) as proof of (((eq Prop) (f x3)) ((and ((or (cR x3)) (cS x3))) (((eq a) Xx) (cF x3))))
% Found (fun (x3:b)=> ((eq_ref Prop) (f x3))) as proof of (forall (x:b), (((eq Prop) (f x)) ((and ((or (cR x)) (cS x))) (((eq a) Xx) (cF x)))))
% Found eq_ref00:=(eq_ref0 b0):(((eq (b->Prop)) b0) b0)
% Found (eq_ref0 b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((eq_ref (b->Prop)) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((eq_ref (b->Prop)) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((eq_ref (b->Prop)) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found eta_expansion000:=(eta_expansion00 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))):(((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) (fun (x:b)=> ((and ((or (cR x)) (cS x))) (((eq a) Xx) (cF x)))))
% Found (eta_expansion00 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found ((eta_expansion0 Prop) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion b) Prop) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion b) Prop) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion b) Prop) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found eta_expansion_dep000:=(eta_expansion_dep00 b0):(((eq (b->Prop)) b0) (fun (x:b)=> (b0 x)))
% Found (eta_expansion_dep00 b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((eta_expansion_dep0 (fun (x1:b)=> Prop)) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion_dep b) (fun (x1:b)=> Prop)) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion_dep b) (fun (x1:b)=> Prop)) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion_dep b) (fun (x1:b)=> Prop)) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found eta_expansion000:=(eta_expansion00 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))):(((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) (fun (x:b)=> ((and ((or (cR x)) (cS x))) (((eq a) Xx) (cF x)))))
% Found (eta_expansion00 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found ((eta_expansion0 Prop) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion b) Prop) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion b) Prop) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion b) Prop) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found eta_expansion000:=(eta_expansion00 b0):(((eq (b->Prop)) b0) (fun (x:b)=> (b0 x)))
% Found (eta_expansion00 b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((eta_expansion0 Prop) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion b) Prop) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion b) Prop) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found (((eta_expansion b) Prop) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))
% Found eta_expansion000:=(eta_expansion00 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))):(((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) (fun (x:b)=> ((and ((or (cR x)) (cS x))) (((eq a) Xx) (cF x)))))
% Found (eta_expansion00 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found ((eta_expansion0 Prop) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion b) Prop) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion b) Prop) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion b) Prop) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found eq_ref00:=(eq_ref0 b0):(((eq (b->Prop)) b0) b0)
% Found (eq_ref0 b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((eq_ref (b->Prop)) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((eq_ref (b->Prop)) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found ((eq_ref (b->Prop)) b0) as proof of (((eq (b->Prop)) b0) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))
% Found eta_expansion000:=(eta_expansion00 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))):(((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) (fun (x:b)=> ((and ((or (cR x)) (cS x))) (((eq a) Xx) (cF x)))))
% Found (eta_expansion00 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found ((eta_expansion0 Prop) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion b) Prop) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion b) Prop) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found (((eta_expansion b) Prop) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) b0)
% Found or_introl000:=(or_introl00 (cS x5)):((or (cR x5)) (cS x5))
% Found (or_introl00 (cS x5)) as proof of ((or (cR x5)) (cS x5))
% Found ((fun (B:Prop)=> ((or_introl0 B) x3)) (cS x5)) as proof of ((or (cR x5)) (cS x5))
% Found ((fun (B:Prop)=> (((or_introl (cR x5)) B) x3)) (cS x5)) as proof of ((or (cR x5)) (cS x5))
% Found ((fun (B:Prop)=> (((or_introl (cR x5)) B) x3)) (cS x5)) as proof of ((or (cR x5)) (cS x5))
% Found ((conj00 ((fun (B:Prop)=> (((or_introl (cR x5)) B) x3)) (cS x5))) x4) as proof of ((and ((or (cR x5)) (cS x5))) (((eq a) Xx) (cF x5)))
% Found (((conj0 (((eq a) Xx) (cF x5))) ((fun (B:Prop)=> (((or_introl (cR x5)) B) x3)) (cS x5))) x4) as proof of ((and ((or (cR x5)) (cS x5))) (((eq a) Xx) (cF x5)))
% Found ((((conj ((or (cR x5)) (cS x5))) (((eq a) Xx) (cF x5))) ((fun (B:Prop)=> (((or_introl (cR x5)) B) x3)) (cS x5))) x4) as proof of ((and ((or (cR x5)) (cS x5))) (((eq a) Xx) (cF x5)))
% Found ((((conj ((or (cR x5)) (cS x5))) (((eq a) Xx) (cF x5))) ((fun (B:Prop)=> (((or_introl (cR x5)) B) x3)) (cS x5))) x4) as proof of ((and ((or (cR x5)) (cS x5))) (((eq a) Xx) (cF x5)))
% Found (ex_intro000 ((((conj ((or (cR x5)) (cS x5))) (((eq a) Xx) (cF x5))) ((fun (B:Prop)=> (((or_introl (cR x5)) B) x3)) (cS x5))) x4)) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found ((ex_intro00 x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) ((fun (B:Prop)=> (((or_introl (cR x1)) B) x3)) (cS x1))) x4)) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (((ex_intro0 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) ((fun (B:Prop)=> (((or_introl (cR x1)) B) x3)) (cS x1))) x4)) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) ((fun (B:Prop)=> (((or_introl (cR x1)) B) x3)) (cS x1))) x4)) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (fun (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) ((fun (B:Prop)=> (((or_introl (cR x1)) B) x3)) (cS x1))) x4))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (fun (x3:(cR x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) ((fun (B:Prop)=> (((or_introl (cR x1)) B) x3)) (cS x1))) x4))) as proof of ((((eq a) Xx) (cF x1))->((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))))
% Found (fun (x3:(cR x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) ((fun (B:Prop)=> (((or_introl (cR x1)) B) x3)) (cS x1))) x4))) as proof of ((cR x1)->((((eq a) Xx) (cF x1))->((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))))
% Found (and_rect00 (fun (x3:(cR x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) ((fun (B:Prop)=> (((or_introl (cR x1)) B) x3)) (cS x1))) x4)))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found ((and_rect0 ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cR x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) ((fun (B:Prop)=> (((or_introl (cR x1)) B) x3)) (cS x1))) x4)))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (((fun (P:Type) (x3:((cR x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cR x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cR x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) ((fun (B:Prop)=> (((or_introl (cR x1)) B) x3)) (cS x1))) x4)))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (fun (x2:((and (cR x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cR x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cR x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cR x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) ((fun (B:Prop)=> (((or_introl (cR x1)) B) x3)) (cS x1))) x4))))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (fun (x1:b) (x2:((and (cR x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cR x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cR x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cR x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) ((fun (B:Prop)=> (((or_introl (cR x1)) B) x3)) (cS x1))) x4))))) as proof of (((and (cR x1)) (((eq a) Xx) (cF x1)))->((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))))
% Found (fun (x1:b) (x2:((and (cR x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cR x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cR x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cR x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) ((fun (B:Prop)=> (((or_introl (cR x1)) B) x3)) (cS x1))) x4))))) as proof of (forall (x:b), (((and (cR x)) (((eq a) Xx) (cF x)))->((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))))
% Found (ex_ind00 (fun (x1:b) (x2:((and (cR x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cR x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cR x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cR x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) ((fun (B:Prop)=> (((or_introl (cR x1)) B) x3)) (cS x1))) x4)))))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found ((ex_ind0 ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x1:b) (x2:((and (cR x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cR x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cR x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cR x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) ((fun (B:Prop)=> (((or_introl (cR x1)) B) x3)) (cS x1))) x4)))))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (((fun (P:Prop) (x1:(forall (x:b), (((and (cR x)) (((eq a) Xx) (cF x)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) P) x1) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x1:b) (x2:((and (cR x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cR x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cR x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cR x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) ((fun (B:Prop)=> (((or_introl (cR x1)) B) x3)) (cS x1))) x4)))))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (fun (x0:((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))))=> (((fun (P:Prop) (x1:(forall (x:b), (((and (cR x)) (((eq a) Xx) (cF x)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) P) x1) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x1:b) (x2:((and (cR x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cR x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cR x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cR x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) ((fun (B:Prop)=> (((or_introl (cR x1)) B) x3)) (cS x1))) x4))))))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (fun (x0:((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))))=> (((fun (P:Prop) (x1:(forall (x:b), (((and (cR x)) (((eq a) Xx) (cF x)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) P) x1) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x1:b) (x2:((and (cR x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cR x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cR x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cR x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) ((fun (B:Prop)=> (((or_introl (cR x1)) B) x3)) (cS x1))) x4))))))) as proof of (((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))))
% Found x3:(cS x1)
% Instantiate: x5:=x1:b
% Found x3 as proof of (cS x5)
% Found (or_intror00 x3) as proof of ((or (cR x5)) (cS x5))
% Found ((or_intror0 (cS x5)) x3) as proof of ((or (cR x5)) (cS x5))
% Found (((or_intror (cR x5)) (cS x5)) x3) as proof of ((or (cR x5)) (cS x5))
% Found (((or_intror (cR x5)) (cS x5)) x3) as proof of ((or (cR x5)) (cS x5))
% Found ((conj00 (((or_intror (cR x5)) (cS x5)) x3)) x4) as proof of ((and ((or (cR x5)) (cS x5))) (((eq a) Xx) (cF x5)))
% Found (((conj0 (((eq a) Xx) (cF x5))) (((or_intror (cR x5)) (cS x5)) x3)) x4) as proof of ((and ((or (cR x5)) (cS x5))) (((eq a) Xx) (cF x5)))
% Found ((((conj ((or (cR x5)) (cS x5))) (((eq a) Xx) (cF x5))) (((or_intror (cR x5)) (cS x5)) x3)) x4) as proof of ((and ((or (cR x5)) (cS x5))) (((eq a) Xx) (cF x5)))
% Found ((((conj ((or (cR x5)) (cS x5))) (((eq a) Xx) (cF x5))) (((or_intror (cR x5)) (cS x5)) x3)) x4) as proof of ((and ((or (cR x5)) (cS x5))) (((eq a) Xx) (cF x5)))
% Found (ex_intro000 ((((conj ((or (cR x5)) (cS x5))) (((eq a) Xx) (cF x5))) (((or_intror (cR x5)) (cS x5)) x3)) x4)) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found ((ex_intro00 x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) (((or_intror (cR x1)) (cS x1)) x3)) x4)) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (((ex_intro0 (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) (((or_intror (cR x1)) (cS x1)) x3)) x4)) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) (((or_intror (cR x1)) (cS x1)) x3)) x4)) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (fun (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) (((or_intror (cR x1)) (cS x1)) x3)) x4))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (fun (x3:(cS x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) (((or_intror (cR x1)) (cS x1)) x3)) x4))) as proof of ((((eq a) Xx) (cF x1))->((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))))
% Found (fun (x3:(cS x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) (((or_intror (cR x1)) (cS x1)) x3)) x4))) as proof of ((cS x1)->((((eq a) Xx) (cF x1))->((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))))
% Found (and_rect00 (fun (x3:(cS x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) (((or_intror (cR x1)) (cS x1)) x3)) x4)))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found ((and_rect0 ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cS x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) (((or_intror (cR x1)) (cS x1)) x3)) x4)))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (((fun (P:Type) (x3:((cS x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cS x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cS x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) (((or_intror (cR x1)) (cS x1)) x3)) x4)))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (fun (x2:((and (cS x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cS x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cS x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cS x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) (((or_intror (cR x1)) (cS x1)) x3)) x4))))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (fun (x1:b) (x2:((and (cS x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cS x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cS x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cS x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) (((or_intror (cR x1)) (cS x1)) x3)) x4))))) as proof of (((and (cS x1)) (((eq a) Xx) (cF x1)))->((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))))
% Found (fun (x1:b) (x2:((and (cS x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cS x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cS x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cS x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) (((or_intror (cR x1)) (cS x1)) x3)) x4))))) as proof of (forall (x:b), (((and (cS x)) (((eq a) Xx) (cF x)))->((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))))
% Found (ex_ind00 (fun (x1:b) (x2:((and (cS x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cS x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cS x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cS x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) (((or_intror (cR x1)) (cS x1)) x3)) x4)))))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found ((ex_ind0 ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x1:b) (x2:((and (cS x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cS x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cS x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cS x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) (((or_intror (cR x1)) (cS x1)) x3)) x4)))))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (((fun (P:Prop) (x1:(forall (x:b), (((and (cS x)) (((eq a) Xx) (cF x)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) P) x1) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x1:b) (x2:((and (cS x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cS x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cS x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cS x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) (((or_intror (cR x1)) (cS x1)) x3)) x4)))))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (fun (x0:((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))))=> (((fun (P:Prop) (x1:(forall (x:b), (((and (cS x)) (((eq a) Xx) (cF x)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) P) x1) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x1:b) (x2:((and (cS x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cS x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cS x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cS x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) (((or_intror (cR x1)) (cS x1)) x3)) x4))))))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (fun (x0:((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))))=> (((fun (P:Prop) (x1:(forall (x:b), (((and (cS x)) (((eq a) Xx) (cF x)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) P) x1) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x1:b) (x2:((and (cS x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cS x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cS x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cS x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) (((or_intror (cR x1)) (cS x1)) x3)) x4))))))) as proof of (((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))->((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))))
% Found ((or_ind00 (fun (x0:((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))))=> (((fun (P:Prop) (x1:(forall (x:b), (((and (cR x)) (((eq a) Xx) (cF x)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) P) x1) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x1:b) (x2:((and (cR x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cR x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cR x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cR x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) ((fun (B:Prop)=> (((or_introl (cR x1)) B) x3)) (cS x1))) x4)))))))) (fun (x0:((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))))=> (((fun (P:Prop) (x1:(forall (x:b), (((and (cS x)) (((eq a) Xx) (cF x)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) P) x1) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x1:b) (x2:((and (cS x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cS x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cS x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cS x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) (((or_intror (cR x1)) (cS x1)) x3)) x4)))))))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (((or_ind0 ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x0:((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))))=> (((fun (P:Prop) (x1:(forall (x:b), (((and (cR x)) (((eq a) Xx) (cF x)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) P) x1) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x1:b) (x2:((and (cR x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cR x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cR x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cR x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) ((fun (B:Prop)=> (((or_introl (cR x1)) B) x3)) (cS x1))) x4)))))))) (fun (x0:((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))))=> (((fun (P:Prop) (x1:(forall (x:b), (((and (cS x)) (((eq a) Xx) (cF x)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) P) x1) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x1:b) (x2:((and (cS x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cS x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cS x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cS x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) (((or_intror (cR x1)) (cS x1)) x3)) x4)))))))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found ((((fun (P:Prop) (x0:(((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->P)) (x1:(((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))->P))=> ((((((or_ind ((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))) ((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))) P) x0) x1) x)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x0:((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))))=> (((fun (P:Prop) (x1:(forall (x0:b), (((and (cR x0)) (((eq a) Xx) (cF x0)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) P) x1) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x1:b) (x2:((and (cR x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cR x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cR x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cR x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) ((fun (B:Prop)=> (((or_introl (cR x1)) B) x3)) (cS x1))) x4)))))))) (fun (x0:((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))))=> (((fun (P:Prop) (x1:(forall (x0:b), (((and (cS x0)) (((eq a) Xx) (cF x0)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) P) x1) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x1:b) (x2:((and (cS x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cS x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cS x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cS x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) (((or_intror (cR x1)) (cS x1)) x3)) x4)))))))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (fun (x:((or ((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))) ((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))))=> ((((fun (P:Prop) (x0:(((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->P)) (x1:(((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))->P))=> ((((((or_ind ((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))) ((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))) P) x0) x1) x)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x0:((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))))=> (((fun (P:Prop) (x1:(forall (x0:b), (((and (cR x0)) (((eq a) Xx) (cF x0)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) P) x1) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x1:b) (x2:((and (cR x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cR x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cR x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cR x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) ((fun (B:Prop)=> (((or_introl (cR x1)) B) x3)) (cS x1))) x4)))))))) (fun (x0:((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))))=> (((fun (P:Prop) (x1:(forall (x0:b), (((and (cS x0)) (((eq a) Xx) (cF x0)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) P) x1) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x1:b) (x2:((and (cS x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cS x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cS x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cS x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) (((or_intror (cR x1)) (cS x1)) x3)) x4))))))))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))
% Found (fun (Xx:a) (x:((or ((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))) ((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))))=> ((((fun (P:Prop) (x0:(((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->P)) (x1:(((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))->P))=> ((((((or_ind ((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))) ((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))) P) x0) x1) x)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x0:((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))))=> (((fun (P:Prop) (x1:(forall (x0:b), (((and (cR x0)) (((eq a) Xx) (cF x0)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) P) x1) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x1:b) (x2:((and (cR x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cR x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cR x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cR x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) ((fun (B:Prop)=> (((or_introl (cR x1)) B) x3)) (cS x1))) x4)))))))) (fun (x0:((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))))=> (((fun (P:Prop) (x1:(forall (x0:b), (((and (cS x0)) (((eq a) Xx) (cF x0)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) P) x1) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x1:b) (x2:((and (cS x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cS x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cS x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cS x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) (((or_intror (cR x1)) (cS x1)) x3)) x4))))))))) as proof of (((or ((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))) ((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))))->((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))))
% Found (fun (Xx:a) (x:((or ((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))) ((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))))=> ((((fun (P:Prop) (x0:(((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->P)) (x1:(((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))->P))=> ((((((or_ind ((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))) ((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))) P) x0) x1) x)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x0:((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))))=> (((fun (P:Prop) (x1:(forall (x0:b), (((and (cR x0)) (((eq a) Xx) (cF x0)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) P) x1) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x1:b) (x2:((and (cR x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cR x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cR x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cR x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) ((fun (B:Prop)=> (((or_introl (cR x1)) B) x3)) (cS x1))) x4)))))))) (fun (x0:((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))))=> (((fun (P:Prop) (x1:(forall (x0:b), (((and (cS x0)) (((eq a) Xx) (cF x0)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) P) x1) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x1:b) (x2:((and (cS x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cS x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cS x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cS x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) (((or_intror (cR x1)) (cS x1)) x3)) x4))))))))) as proof of (forall (Xx:a), (((or ((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))) ((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))))->((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))))
% Got proof (fun (Xx:a) (x:((or ((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))) ((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))))=> ((((fun (P:Prop) (x0:(((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->P)) (x1:(((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))->P))=> ((((((or_ind ((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))) ((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))) P) x0) x1) x)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x0:((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))))=> (((fun (P:Prop) (x1:(forall (x0:b), (((and (cR x0)) (((eq a) Xx) (cF x0)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) P) x1) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x1:b) (x2:((and (cR x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cR x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cR x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cR x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) ((fun (B:Prop)=> (((or_introl (cR x1)) B) x3)) (cS x1))) x4)))))))) (fun (x0:((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))))=> (((fun (P:Prop) (x1:(forall (x0:b), (((and (cS x0)) (((eq a) Xx) (cF x0)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) P) x1) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x1:b) (x2:((and (cS x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cS x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cS x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cS x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) (((or_intror (cR x1)) (cS x1)) x3)) x4)))))))))
% Time elapsed = 75.671150s
% node=9751 cost=1021.000000 depth=32
% ::::::::::::::::::::::
% % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% (fun (Xx:a) (x:((or ((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))) ((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))))=> ((((fun (P:Prop) (x0:(((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))->P)) (x1:(((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))->P))=> ((((((or_ind ((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt)))))) ((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt)))))) P) x0) x1) x)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x0:((ex b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))))=> (((fun (P:Prop) (x1:(forall (x0:b), (((and (cR x0)) (((eq a) Xx) (cF x0)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and (cR Xt)) (((eq a) Xx) (cF Xt))))) P) x1) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x1:b) (x2:((and (cR x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cR x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cR x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cR x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) ((fun (B:Prop)=> (((or_introl (cR x1)) B) x3)) (cS x1))) x4)))))))) (fun (x0:((ex b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))))=> (((fun (P:Prop) (x1:(forall (x0:b), (((and (cS x0)) (((eq a) Xx) (cF x0)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and (cS Xt)) (((eq a) Xx) (cF Xt))))) P) x1) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x1:b) (x2:((and (cS x1)) (((eq a) Xx) (cF x1))))=> (((fun (P:Type) (x3:((cS x1)->((((eq a) Xx) (cF x1))->P)))=> (((((and_rect (cS x1)) (((eq a) Xx) (cF x1))) P) x3) x2)) ((ex b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt)))))) (fun (x3:(cS x1)) (x4:(((eq a) Xx) (cF x1)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (cR Xt)) (cS Xt))) (((eq a) Xx) (cF Xt))))) x1) ((((conj ((or (cR x1)) (cS x1))) (((eq a) Xx) (cF x1))) (((or_intror (cR x1)) (cS x1)) x3)) x4)))))))))
% % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% EOF
%------------------------------------------------------------------------------