%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEU889^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 : n100.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 19.28s % Output : Proof 19.28s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SEU889^5 : TPTP v6.1.0. Released v4.0.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n100.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:40:56 CDT 2014 % % CPUTime : 19.28 % 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 0x22cbe60>, <kernel.Type object at 0x22cb4d0>) of role type named c_type % Using role type % Declaring c:Type % FOF formula (<kernel.Constant object at 0x25225f0>, <kernel.Type object at 0x22cb710>) of role type named b_type % Using role type % Declaring b:Type % FOF formula (<kernel.Constant object at 0x22cb950>, <kernel.Type object at 0x22cb5f0>) of role type named a_type % Using role type % Declaring a:Type % FOF formula (<kernel.Constant object at 0x22cb4d0>, <kernel.DependentProduct object at 0x22cb9e0>) of role type named cG % Using role type % Declaring cG:(c->b) % FOF formula (<kernel.Constant object at 0x22cb710>, <kernel.DependentProduct object at 0x22cba70>) of role type named cF % Using role type % Declaring cF:(b->a) % FOF formula (<kernel.Constant object at 0x22cb488>, <kernel.DependentProduct object at 0x22cbf80>) of role type named cS % Using role type % Declaring cS:(c->Prop) % FOF formula (forall (Xx:a), (((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) Xt) (cG Xt0)))))) (((eq a) Xx) (cF Xt)))))->((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))))) of role conjecture named cTHM29A_pme % Conjecture to prove = (forall (Xx:a), (((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) Xt) (cG Xt0)))))) (((eq a) Xx) (cF Xt)))))->((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))))):Prop % Parameter c_DUMMY:c. % Parameter b_DUMMY:b. % Parameter a_DUMMY:a. % We need to prove ['(forall (Xx:a), (((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) Xt) (cG Xt0)))))) (((eq a) Xx) (cF Xt)))))->((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))))'] % Parameter c:Type. % Parameter b:Type. % Parameter a:Type. % Parameter cG:(c->b). % Parameter cF:(b->a). % Parameter cS:(c->Prop). % Trying to prove (forall (Xx:a), (((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) Xt) (cG Xt0)))))) (((eq a) Xx) (cF Xt)))))->((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))))) % Found eta_expansion_dep000:=(eta_expansion_dep00 (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))):(((eq (c->Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) (fun (x:c)=> ((and (cS x)) (((eq a) Xx) (cF (cG x)))))) % Found (eta_expansion_dep00 (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) as proof of (((eq (c->Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) b0) % Found ((eta_expansion_dep0 (fun (x1:c)=> Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) as proof of (((eq (c->Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) b0) % Found (((eta_expansion_dep c) (fun (x1:c)=> Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) as proof of (((eq (c->Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) b0) % Found (((eta_expansion_dep c) (fun (x1:c)=> Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) as proof of (((eq (c->Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) b0) % Found (((eta_expansion_dep c) (fun (x1:c)=> Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) as proof of (((eq (c->Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG 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 (cS x0)) (((eq a) Xx) (cF (cG x0))))) % Found ((eq_ref Prop) (f x0)) as proof of (((eq Prop) (f x0)) ((and (cS x0)) (((eq a) Xx) (cF (cG x0))))) % Found ((eq_ref Prop) (f x0)) as proof of (((eq Prop) (f x0)) ((and (cS x0)) (((eq a) Xx) (cF (cG x0))))) % Found (fun (x0:c)=> ((eq_ref Prop) (f x0))) as proof of (((eq Prop) (f x0)) ((and (cS x0)) (((eq a) Xx) (cF (cG x0))))) % Found (fun (x0:c)=> ((eq_ref Prop) (f x0))) as proof of (forall (x:c), (((eq Prop) (f x)) ((and (cS x)) (((eq a) Xx) (cF (cG 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 (cS x0)) (((eq a) Xx) (cF (cG x0))))) % Found ((eq_ref Prop) (f x0)) as proof of (((eq Prop) (f x0)) ((and (cS x0)) (((eq a) Xx) (cF (cG x0))))) % Found ((eq_ref Prop) (f x0)) as proof of (((eq Prop) (f x0)) ((and (cS x0)) (((eq a) Xx) (cF (cG x0))))) % Found (fun (x0:c)=> ((eq_ref Prop) (f x0))) as proof of (((eq Prop) (f x0)) ((and (cS x0)) (((eq a) Xx) (cF (cG x0))))) % Found (fun (x0:c)=> ((eq_ref Prop) (f x0))) as proof of (forall (x:c), (((eq Prop) (f x)) ((and (cS x)) (((eq a) Xx) (cF (cG x)))))) % Found eta_expansion_dep000:=(eta_expansion_dep00 (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))):(((eq (c->Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) (fun (x:c)=> ((and (cS x)) (((eq a) Xx) (cF (cG x)))))) % Found (eta_expansion_dep00 (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) as proof of (((eq (c->Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) b0) % Found ((eta_expansion_dep0 (fun (x3:c)=> Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) as proof of (((eq (c->Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) b0) % Found (((eta_expansion_dep c) (fun (x3:c)=> Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) as proof of (((eq (c->Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) b0) % Found (((eta_expansion_dep c) (fun (x3:c)=> Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) as proof of (((eq (c->Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) b0) % Found (((eta_expansion_dep c) (fun (x3:c)=> Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) as proof of (((eq (c->Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) b0) % Found x6:(cS x4) % Instantiate: x8:=x4:c % Found x6 as proof of (cS x8) % Found eq_ref00:=(eq_ref0 (f x2)):(((eq Prop) (f x2)) (f x2)) % Found (eq_ref0 (f x2)) as proof of (((eq Prop) (f x2)) ((and (cS x2)) (((eq a) Xx) (cF (cG x2))))) % Found ((eq_ref Prop) (f x2)) as proof of (((eq Prop) (f x2)) ((and (cS x2)) (((eq a) Xx) (cF (cG x2))))) % Found ((eq_ref Prop) (f x2)) as proof of (((eq Prop) (f x2)) ((and (cS x2)) (((eq a) Xx) (cF (cG x2))))) % Found (fun (x2:c)=> ((eq_ref Prop) (f x2))) as proof of (((eq Prop) (f x2)) ((and (cS x2)) (((eq a) Xx) (cF (cG x2))))) % Found (fun (x2:c)=> ((eq_ref Prop) (f x2))) as proof of (forall (x:c), (((eq Prop) (f x)) ((and (cS x)) (((eq a) Xx) (cF (cG x)))))) % Found eq_ref00:=(eq_ref0 (f x2)):(((eq Prop) (f x2)) (f x2)) % Found (eq_ref0 (f x2)) as proof of (((eq Prop) (f x2)) ((and (cS x2)) (((eq a) Xx) (cF (cG x2))))) % Found ((eq_ref Prop) (f x2)) as proof of (((eq Prop) (f x2)) ((and (cS x2)) (((eq a) Xx) (cF (cG x2))))) % Found ((eq_ref Prop) (f x2)) as proof of (((eq Prop) (f x2)) ((and (cS x2)) (((eq a) Xx) (cF (cG x2))))) % Found (fun (x2:c)=> ((eq_ref Prop) (f x2))) as proof of (((eq Prop) (f x2)) ((and (cS x2)) (((eq a) Xx) (cF (cG x2))))) % Found (fun (x2:c)=> ((eq_ref Prop) (f x2))) as proof of (forall (x:c), (((eq Prop) (f x)) ((and (cS x)) (((eq a) Xx) (cF (cG x)))))) % Found x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0))))) % Instantiate: b0:=(fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))):(c->Prop) % Found x2 as proof of (P b0) % Found eta_expansion_dep000:=(eta_expansion_dep00 (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))):(((eq (c->Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) (fun (x:c)=> ((and (cS x)) (((eq a) Xx) (cF (cG x)))))) % Found (eta_expansion_dep00 (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) as proof of (((eq (c->Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) b0) % Found ((eta_expansion_dep0 (fun (x5:c)=> Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) as proof of (((eq (c->Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) b0) % Found (((eta_expansion_dep c) (fun (x5:c)=> Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) as proof of (((eq (c->Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) b0) % Found (((eta_expansion_dep c) (fun (x5:c)=> Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) as proof of (((eq (c->Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) b0) % Found (((eta_expansion_dep c) (fun (x5:c)=> Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) as proof of (((eq (c->Prop)) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) b0) % Found x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0))))) % Instantiate: b0:=(fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))):(c->Prop) % Found (fun (x3:(((eq a) Xx) (cF x0)))=> x2) as proof of (P b0) % Found (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> x2) as proof of ((((eq a) Xx) (cF x0))->(P b0)) % Found (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> x2) as proof of (((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))->((((eq a) Xx) (cF x0))->(P b0))) % Found (and_rect00 (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> x2)) as proof of (P b0) % Found ((and_rect0 (P b0)) (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> x2)) as proof of (P b0) % Found (((fun (P0:Type) (x2:(((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))->((((eq a) Xx) (cF x0))->P0)))=> (((((and_rect ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))) P0) x2) x1)) (P b0)) (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> x2)) as proof of (P b0) % Found (((fun (P0:Type) (x2:(((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))->((((eq a) Xx) (cF x0))->P0)))=> (((((and_rect ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))) P0) x2) x1)) (P b0)) (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> x2)) as proof of (P b0) % Found x7:(cS x5) % Instantiate: x0:=x5:c % Found x7 as proof of (cS x0) % Found x7:(cS x5) % Instantiate: x2:=x5:c % Found x7 as proof of (cS x2) % Found x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0))))) % Instantiate: b0:=(fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))):(c->Prop) % Found (fun (x3:(((eq a) Xx) (cF x0)))=> x2) as proof of (P b0) % Found (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> x2) as proof of ((((eq a) Xx) (cF x0))->(P b0)) % Found (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> x2) as proof of (((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))->((((eq a) Xx) (cF x0))->(P b0))) % Found (and_rect00 (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> x2)) as proof of (P b0) % Found ((and_rect0 (P b0)) (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> x2)) as proof of (P b0) % Found (((fun (P0:Type) (x2:(((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))->((((eq a) Xx) (cF x0))->P0)))=> (((((and_rect ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))) P0) x2) x1)) (P b0)) (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> x2)) as proof of (P b0) % Found (fun (x1:((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))))=> (((fun (P0:Type) (x2:(((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))->((((eq a) Xx) (cF x0))->P0)))=> (((((and_rect ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))) P0) x2) x1)) (P b0)) (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> x2))) as proof of (P b0) % Found x7:(cS x5) % Instantiate: x4:=x5:c % Found x7 as proof of (cS x4) % Found x7:(cS x4) % Instantiate: x6:=x4:c % Found x7 as proof of (cS x6) % Found x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0))))) % Instantiate: f:=(fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))):(c->Prop) % Found x2 as proof of (P f) % Found eq_ref00:=(eq_ref0 (f x4)):(((eq Prop) (f x4)) (f x4)) % Found (eq_ref0 (f x4)) as proof of (((eq Prop) (f x4)) ((and (cS x4)) (((eq a) Xx) (cF (cG x4))))) % Found ((eq_ref Prop) (f x4)) as proof of (((eq Prop) (f x4)) ((and (cS x4)) (((eq a) Xx) (cF (cG x4))))) % Found ((eq_ref Prop) (f x4)) as proof of (((eq Prop) (f x4)) ((and (cS x4)) (((eq a) Xx) (cF (cG x4))))) % Found (fun (x4:c)=> ((eq_ref Prop) (f x4))) as proof of (((eq Prop) (f x4)) ((and (cS x4)) (((eq a) Xx) (cF (cG x4))))) % Found (fun (x4:c)=> ((eq_ref Prop) (f x4))) as proof of (forall (x:c), (((eq Prop) (f x)) ((and (cS x)) (((eq a) Xx) (cF (cG x)))))) % Found x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0))))) % Instantiate: f:=(fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))):(c->Prop) % Found x2 as proof of (P f) % Found eq_ref00:=(eq_ref0 (f x4)):(((eq Prop) (f x4)) (f x4)) % Found (eq_ref0 (f x4)) as proof of (((eq Prop) (f x4)) ((and (cS x4)) (((eq a) Xx) (cF (cG x4))))) % Found ((eq_ref Prop) (f x4)) as proof of (((eq Prop) (f x4)) ((and (cS x4)) (((eq a) Xx) (cF (cG x4))))) % Found ((eq_ref Prop) (f x4)) as proof of (((eq Prop) (f x4)) ((and (cS x4)) (((eq a) Xx) (cF (cG x4))))) % Found (fun (x4:c)=> ((eq_ref Prop) (f x4))) as proof of (((eq Prop) (f x4)) ((and (cS x4)) (((eq a) Xx) (cF (cG x4))))) % Found (fun (x4:c)=> ((eq_ref Prop) (f x4))) as proof of (forall (x:c), (((eq Prop) (f x)) ((and (cS x)) (((eq a) Xx) (cF (cG x)))))) % Found x700:=(x70 x3):(((eq a) Xx) (cF (cG x4))) % Found (x70 x3) as proof of (((eq a) Xx) (cF (cG x8))) % Found ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3) as proof of (((eq a) Xx) (cF (cG x8))) % Found ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3) as proof of (((eq a) Xx) (cF (cG x8))) % Found ((conj00 x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3)) as proof of ((and (cS x8)) (((eq a) Xx) (cF (cG x8)))) % Found (((conj0 (((eq a) Xx) (cF (cG x8)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3)) as proof of ((and (cS x8)) (((eq a) Xx) (cF (cG x8)))) % Found ((((conj (cS x8)) (((eq a) Xx) (cF (cG x8)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3)) as proof of ((and (cS x8)) (((eq a) Xx) (cF (cG x8)))) % Found ((((conj (cS x8)) (((eq a) Xx) (cF (cG x8)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3)) as proof of ((and (cS x8)) (((eq a) Xx) (cF (cG x8)))) % Found (ex_intro000 ((((conj (cS x8)) (((eq a) Xx) (cF (cG x8)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3))) as proof of ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) % Found ((ex_intro00 x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3))) as proof of ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) % Found (((ex_intro0 (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3))) as proof of ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) % Found ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3))) as proof of ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) % Found (fun (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3)))) as proof of ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) % Found (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3)))) as proof of ((((eq b) x0) (cG x4))->((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) % Found (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3)))) as proof of ((cS x4)->((((eq b) x0) (cG x4))->((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))))) % Found (and_rect10 (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3))))) as proof of ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) % Found ((and_rect1 ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3))))) as proof of ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) % Found (((fun (P:Type) (x6:((cS x4)->((((eq b) x0) (cG x4))->P)))=> (((((and_rect (cS x4)) (((eq b) x0) (cG x4))) P) x6) x5)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3))))) as proof of ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) % Found (fun (x5:((and (cS x4)) (((eq b) x0) (cG x4))))=> (((fun (P:Type) (x6:((cS x4)->((((eq b) x0) (cG x4))->P)))=> (((((and_rect (cS x4)) (((eq b) x0) (cG x4))) P) x6) x5)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3)))))) as proof of ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) % Found (fun (x4:c) (x5:((and (cS x4)) (((eq b) x0) (cG x4))))=> (((fun (P:Type) (x6:((cS x4)->((((eq b) x0) (cG x4))->P)))=> (((((and_rect (cS x4)) (((eq b) x0) (cG x4))) P) x6) x5)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3)))))) as proof of (((and (cS x4)) (((eq b) x0) (cG x4)))->((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) % Found (fun (x4:c) (x5:((and (cS x4)) (((eq b) x0) (cG x4))))=> (((fun (P:Type) (x6:((cS x4)->((((eq b) x0) (cG x4))->P)))=> (((((and_rect (cS x4)) (((eq b) x0) (cG x4))) P) x6) x5)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3)))))) as proof of (forall (x:c), (((and (cS x)) (((eq b) x0) (cG x)))->((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))))) % Found (ex_ind10 (fun (x4:c) (x5:((and (cS x4)) (((eq b) x0) (cG x4))))=> (((fun (P:Type) (x6:((cS x4)->((((eq b) x0) (cG x4))->P)))=> (((((and_rect (cS x4)) (((eq b) x0) (cG x4))) P) x6) x5)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3))))))) as proof of ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) % Found ((ex_ind1 ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x4:c) (x5:((and (cS x4)) (((eq b) x0) (cG x4))))=> (((fun (P:Type) (x6:((cS x4)->((((eq b) x0) (cG x4))->P)))=> (((((and_rect (cS x4)) (((eq b) x0) (cG x4))) P) x6) x5)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3))))))) as proof of ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) % Found (((fun (P:Prop) (x4:(forall (x:c), (((and (cS x)) (((eq b) x0) (cG x)))->P)))=> (((((ex_ind c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0))))) P) x4) x2)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x4:c) (x5:((and (cS x4)) (((eq b) x0) (cG x4))))=> (((fun (P:Type) (x6:((cS x4)->((((eq b) x0) (cG x4))->P)))=> (((((and_rect (cS x4)) (((eq b) x0) (cG x4))) P) x6) x5)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3))))))) as proof of ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) % Found (fun (x3:(((eq a) Xx) (cF x0)))=> (((fun (P:Prop) (x4:(forall (x:c), (((and (cS x)) (((eq b) x0) (cG x)))->P)))=> (((((ex_ind c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0))))) P) x4) x2)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x4:c) (x5:((and (cS x4)) (((eq b) x0) (cG x4))))=> (((fun (P:Type) (x6:((cS x4)->((((eq b) x0) (cG x4))->P)))=> (((((and_rect (cS x4)) (((eq b) x0) (cG x4))) P) x6) x5)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3)))))))) as proof of ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) % Found (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> (((fun (P:Prop) (x4:(forall (x:c), (((and (cS x)) (((eq b) x0) (cG x)))->P)))=> (((((ex_ind c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0))))) P) x4) x2)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x4:c) (x5:((and (cS x4)) (((eq b) x0) (cG x4))))=> (((fun (P:Type) (x6:((cS x4)->((((eq b) x0) (cG x4))->P)))=> (((((and_rect (cS x4)) (((eq b) x0) (cG x4))) P) x6) x5)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3)))))))) as proof of ((((eq a) Xx) (cF x0))->((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) % Found (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> (((fun (P:Prop) (x4:(forall (x:c), (((and (cS x)) (((eq b) x0) (cG x)))->P)))=> (((((ex_ind c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0))))) P) x4) x2)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x4:c) (x5:((and (cS x4)) (((eq b) x0) (cG x4))))=> (((fun (P:Type) (x6:((cS x4)->((((eq b) x0) (cG x4))->P)))=> (((((and_rect (cS x4)) (((eq b) x0) (cG x4))) P) x6) x5)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3)))))))) as proof of (((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))->((((eq a) Xx) (cF x0))->((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))))) % Found (and_rect00 (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> (((fun (P:Prop) (x4:(forall (x:c), (((and (cS x)) (((eq b) x0) (cG x)))->P)))=> (((((ex_ind c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0))))) P) x4) x2)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x4:c) (x5:((and (cS x4)) (((eq b) x0) (cG x4))))=> (((fun (P:Type) (x6:((cS x4)->((((eq b) x0) (cG x4))->P)))=> (((((and_rect (cS x4)) (((eq b) x0) (cG x4))) P) x6) x5)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3))))))))) as proof of ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) % Found ((and_rect0 ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> (((fun (P:Prop) (x4:(forall (x:c), (((and (cS x)) (((eq b) x0) (cG x)))->P)))=> (((((ex_ind c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0))))) P) x4) x2)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x4:c) (x5:((and (cS x4)) (((eq b) x0) (cG x4))))=> (((fun (P:Type) (x6:((cS x4)->((((eq b) x0) (cG x4))->P)))=> (((((and_rect (cS x4)) (((eq b) x0) (cG x4))) P) x6) x5)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3))))))))) as proof of ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) % Found (((fun (P:Type) (x2:(((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))->((((eq a) Xx) (cF x0))->P)))=> (((((and_rect ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))) P) x2) x1)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> (((fun (P:Prop) (x4:(forall (x:c), (((and (cS x)) (((eq b) x0) (cG x)))->P)))=> (((((ex_ind c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0))))) P) x4) x2)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x4:c) (x5:((and (cS x4)) (((eq b) x0) (cG x4))))=> (((fun (P:Type) (x6:((cS x4)->((((eq b) x0) (cG x4))->P)))=> (((((and_rect (cS x4)) (((eq b) x0) (cG x4))) P) x6) x5)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3))))))))) as proof of ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) % Found (fun (x1:((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))))=> (((fun (P:Type) (x2:(((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))->((((eq a) Xx) (cF x0))->P)))=> (((((and_rect ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))) P) x2) x1)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> (((fun (P:Prop) (x4:(forall (x:c), (((and (cS x)) (((eq b) x0) (cG x)))->P)))=> (((((ex_ind c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0))))) P) x4) x2)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x4:c) (x5:((and (cS x4)) (((eq b) x0) (cG x4))))=> (((fun (P:Type) (x6:((cS x4)->((((eq b) x0) (cG x4))->P)))=> (((((and_rect (cS x4)) (((eq b) x0) (cG x4))) P) x6) x5)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3)))))))))) as proof of ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) % Found (fun (x0:b) (x1:((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))))=> (((fun (P:Type) (x2:(((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))->((((eq a) Xx) (cF x0))->P)))=> (((((and_rect ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))) P) x2) x1)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> (((fun (P:Prop) (x4:(forall (x:c), (((and (cS x)) (((eq b) x0) (cG x)))->P)))=> (((((ex_ind c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0))))) P) x4) x2)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x4:c) (x5:((and (cS x4)) (((eq b) x0) (cG x4))))=> (((fun (P:Type) (x6:((cS x4)->((((eq b) x0) (cG x4))->P)))=> (((((and_rect (cS x4)) (((eq b) x0) (cG x4))) P) x6) x5)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3)))))))))) as proof of (((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0)))->((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) % Found (fun (x0:b) (x1:((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))))=> (((fun (P:Type) (x2:(((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))->((((eq a) Xx) (cF x0))->P)))=> (((((and_rect ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))) P) x2) x1)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> (((fun (P:Prop) (x4:(forall (x:c), (((and (cS x)) (((eq b) x0) (cG x)))->P)))=> (((((ex_ind c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0))))) P) x4) x2)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x4:c) (x5:((and (cS x4)) (((eq b) x0) (cG x4))))=> (((fun (P:Type) (x6:((cS x4)->((((eq b) x0) (cG x4))->P)))=> (((((and_rect (cS x4)) (((eq b) x0) (cG x4))) P) x6) x5)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3)))))))))) as proof of (forall (x:b), (((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x) (cG Xt0)))))) (((eq a) Xx) (cF x)))->((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))))) % Found (ex_ind00 (fun (x0:b) (x1:((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))))=> (((fun (P:Type) (x2:(((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))->((((eq a) Xx) (cF x0))->P)))=> (((((and_rect ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))) P) x2) x1)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> (((fun (P:Prop) (x4:(forall (x:c), (((and (cS x)) (((eq b) x0) (cG x)))->P)))=> (((((ex_ind c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0))))) P) x4) x2)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x4:c) (x5:((and (cS x4)) (((eq b) x0) (cG x4))))=> (((fun (P:Type) (x6:((cS x4)->((((eq b) x0) (cG x4))->P)))=> (((((and_rect (cS x4)) (((eq b) x0) (cG x4))) P) x6) x5)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3))))))))))) as proof of ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) % Found ((ex_ind0 ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x0:b) (x1:((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))))=> (((fun (P:Type) (x2:(((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))->((((eq a) Xx) (cF x0))->P)))=> (((((and_rect ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))) P) x2) x1)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> (((fun (P:Prop) (x4:(forall (x:c), (((and (cS x)) (((eq b) x0) (cG x)))->P)))=> (((((ex_ind c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0))))) P) x4) x2)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x4:c) (x5:((and (cS x4)) (((eq b) x0) (cG x4))))=> (((fun (P:Type) (x6:((cS x4)->((((eq b) x0) (cG x4))->P)))=> (((((and_rect (cS x4)) (((eq b) x0) (cG x4))) P) x6) x5)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3))))))))))) as proof of ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) % Found (((fun (P:Prop) (x0:(forall (x:b), (((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x) (cG Xt0)))))) (((eq a) Xx) (cF x)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) Xt) (cG Xt0)))))) (((eq a) Xx) (cF Xt))))) P) x0) x)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x0:b) (x1:((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))))=> (((fun (P:Type) (x2:(((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))->((((eq a) Xx) (cF x0))->P)))=> (((((and_rect ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))) P) x2) x1)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> (((fun (P:Prop) (x4:(forall (x1:c), (((and (cS x1)) (((eq b) x0) (cG x1)))->P)))=> (((((ex_ind c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0))))) P) x4) x2)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x4:c) (x5:((and (cS x4)) (((eq b) x0) (cG x4))))=> (((fun (P:Type) (x6:((cS x4)->((((eq b) x0) (cG x4))->P)))=> (((((and_rect (cS x4)) (((eq b) x0) (cG x4))) P) x6) x5)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3))))))))))) as proof of ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) % Found (fun (x:((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) Xt) (cG Xt0)))))) (((eq a) Xx) (cF Xt))))))=> (((fun (P:Prop) (x0:(forall (x:b), (((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x) (cG Xt0)))))) (((eq a) Xx) (cF x)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) Xt) (cG Xt0)))))) (((eq a) Xx) (cF Xt))))) P) x0) x)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x0:b) (x1:((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))))=> (((fun (P:Type) (x2:(((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))->((((eq a) Xx) (cF x0))->P)))=> (((((and_rect ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))) P) x2) x1)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> (((fun (P:Prop) (x4:(forall (x1:c), (((and (cS x1)) (((eq b) x0) (cG x1)))->P)))=> (((((ex_ind c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0))))) P) x4) x2)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x4:c) (x5:((and (cS x4)) (((eq b) x0) (cG x4))))=> (((fun (P:Type) (x6:((cS x4)->((((eq b) x0) (cG x4))->P)))=> (((((and_rect (cS x4)) (((eq b) x0) (cG x4))) P) x6) x5)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3)))))))))))) as proof of ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) % Found (fun (Xx:a) (x:((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) Xt) (cG Xt0)))))) (((eq a) Xx) (cF Xt))))))=> (((fun (P:Prop) (x0:(forall (x:b), (((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x) (cG Xt0)))))) (((eq a) Xx) (cF x)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) Xt) (cG Xt0)))))) (((eq a) Xx) (cF Xt))))) P) x0) x)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x0:b) (x1:((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))))=> (((fun (P:Type) (x2:(((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))->((((eq a) Xx) (cF x0))->P)))=> (((((and_rect ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))) P) x2) x1)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> (((fun (P:Prop) (x4:(forall (x1:c), (((and (cS x1)) (((eq b) x0) (cG x1)))->P)))=> (((((ex_ind c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0))))) P) x4) x2)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x4:c) (x5:((and (cS x4)) (((eq b) x0) (cG x4))))=> (((fun (P:Type) (x6:((cS x4)->((((eq b) x0) (cG x4))->P)))=> (((((and_rect (cS x4)) (((eq b) x0) (cG x4))) P) x6) x5)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3)))))))))))) as proof of (((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) Xt) (cG Xt0)))))) (((eq a) Xx) (cF Xt)))))->((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) % Found (fun (Xx:a) (x:((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) Xt) (cG Xt0)))))) (((eq a) Xx) (cF Xt))))))=> (((fun (P:Prop) (x0:(forall (x:b), (((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x) (cG Xt0)))))) (((eq a) Xx) (cF x)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) Xt) (cG Xt0)))))) (((eq a) Xx) (cF Xt))))) P) x0) x)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x0:b) (x1:((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))))=> (((fun (P:Type) (x2:(((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))->((((eq a) Xx) (cF x0))->P)))=> (((((and_rect ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))) P) x2) x1)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> (((fun (P:Prop) (x4:(forall (x1:c), (((and (cS x1)) (((eq b) x0) (cG x1)))->P)))=> (((((ex_ind c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0))))) P) x4) x2)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x4:c) (x5:((and (cS x4)) (((eq b) x0) (cG x4))))=> (((fun (P:Type) (x6:((cS x4)->((((eq b) x0) (cG x4))->P)))=> (((((and_rect (cS x4)) (((eq b) x0) (cG x4))) P) x6) x5)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3)))))))))))) as proof of (forall (Xx:a), (((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) Xt) (cG Xt0)))))) (((eq a) Xx) (cF Xt)))))->((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))))) % Got proof (fun (Xx:a) (x:((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) Xt) (cG Xt0)))))) (((eq a) Xx) (cF Xt))))))=> (((fun (P:Prop) (x0:(forall (x:b), (((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x) (cG Xt0)))))) (((eq a) Xx) (cF x)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) Xt) (cG Xt0)))))) (((eq a) Xx) (cF Xt))))) P) x0) x)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x0:b) (x1:((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))))=> (((fun (P:Type) (x2:(((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))->((((eq a) Xx) (cF x0))->P)))=> (((((and_rect ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))) P) x2) x1)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> (((fun (P:Prop) (x4:(forall (x1:c), (((and (cS x1)) (((eq b) x0) (cG x1)))->P)))=> (((((ex_ind c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0))))) P) x4) x2)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x4:c) (x5:((and (cS x4)) (((eq b) x0) (cG x4))))=> (((fun (P:Type) (x6:((cS x4)->((((eq b) x0) (cG x4))->P)))=> (((((and_rect (cS x4)) (((eq b) x0) (cG x4))) P) x6) x5)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3)))))))))))) % Time elapsed = 18.807378s % node=1877 cost=1210.000000 depth=37 % :::::::::::::::::::::: % % 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:((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) Xt) (cG Xt0)))))) (((eq a) Xx) (cF Xt))))))=> (((fun (P:Prop) (x0:(forall (x:b), (((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x) (cG Xt0)))))) (((eq a) Xx) (cF x)))->P)))=> (((((ex_ind b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) Xt) (cG Xt0)))))) (((eq a) Xx) (cF Xt))))) P) x0) x)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x0:b) (x1:((and ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))))=> (((fun (P:Type) (x2:(((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))->((((eq a) Xx) (cF x0))->P)))=> (((((and_rect ((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (((eq a) Xx) (cF x0))) P) x2) x1)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x2:((ex c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0)))))) (x3:(((eq a) Xx) (cF x0)))=> (((fun (P:Prop) (x4:(forall (x1:c), (((and (cS x1)) (((eq b) x0) (cG x1)))->P)))=> (((((ex_ind c) (fun (Xt0:c)=> ((and (cS Xt0)) (((eq b) x0) (cG Xt0))))) P) x4) x2)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x4:c) (x5:((and (cS x4)) (((eq b) x0) (cG x4))))=> (((fun (P:Type) (x6:((cS x4)->((((eq b) x0) (cG x4))->P)))=> (((((and_rect (cS x4)) (((eq b) x0) (cG x4))) P) x6) x5)) ((ex c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt))))))) (fun (x6:(cS x4)) (x7:(((eq b) x0) (cG x4)))=> ((((ex_intro c) (fun (Xt:c)=> ((and (cS Xt)) (((eq a) Xx) (cF (cG Xt)))))) x4) ((((conj (cS x4)) (((eq a) Xx) (cF (cG x4)))) x6) ((x7 (fun (x10:b)=> (((eq a) Xx) (cF x10)))) x3)))))))))))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------