%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEU887^5 : TPTP v6.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n094.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32286.75MB % OS : Linux 2.6.32-431.20.3.el6.x86_64 % CPULimit : 300s % DateTime : Thu Jul 17 13:33:20 EDT 2014 % Result : Theorem 20.55s % Output : Proof 20.55s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SEU887^5 : TPTP v6.1.0. Released v4.0.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n094.star.cs.uiowa.edu % % Model : x86_64 x86_64 % % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % % Memory : 32286.75MB % % OS : Linux 2.6.32-431.20.3.el6.x86_64 % % CPULimit : 300 % % DateTime : Thu Jul 17 11:40:46 CDT 2014 % % CPUTime : 20.55 % 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 0xfac680>, <kernel.Type object at 0xfac518>) of role type named b_type % Using role type % Declaring b:Type % FOF formula (<kernel.Constant object at 0x13e63f8>, <kernel.Type object at 0xfac3f8>) of role type named a_type % Using role type % Declaring a:Type % FOF formula (<kernel.Constant object at 0xfacbd8>, <kernel.Type object at 0xfacc20>) of role type named c_type % Using role type % Declaring c:Type % FOF formula (forall (F:(b->a)) (G:(c->b)) (S:(c->Prop)) (Xx:a), (((ex c) (fun (Xt:c)=> ((and (S Xt)) (((eq a) Xx) (F (G Xt))))))->((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))))) of role conjecture named cTHM28_pme % Conjecture to prove = (forall (F:(b->a)) (G:(c->b)) (S:(c->Prop)) (Xx:a), (((ex c) (fun (Xt:c)=> ((and (S Xt)) (((eq a) Xx) (F (G Xt))))))->((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))))):Prop % Parameter b_DUMMY:b. % Parameter a_DUMMY:a. % Parameter c_DUMMY:c. % We need to prove ['(forall (F:(b->a)) (G:(c->b)) (S:(c->Prop)) (Xx:a), (((ex c) (fun (Xt:c)=> ((and (S Xt)) (((eq a) Xx) (F (G Xt))))))->((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))))'] % Parameter b:Type. % Parameter a:Type. % Parameter c:Type. % Trying to prove (forall (F:(b->a)) (G:(c->b)) (S:(c->Prop)) (Xx:a), (((ex c) (fun (Xt:c)=> ((and (S Xt)) (((eq a) Xx) (F (G Xt))))))->((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))))) % Found x3:(((eq a) Xx) (F (G x0))) % Instantiate: x4:=(G x0):b % Found x3 as proof of (((eq a) Xx) (F x4)) % Found x4:(((eq a) Xx) (F (G x1))) % Instantiate: x0:=(G x1):b % Found x4 as proof of (((eq a) Xx) (F x0)) % Found x4:(((eq a) Xx) (F (G x0))) % Instantiate: x2:=(G x0):b % Found x4 as proof of (((eq a) Xx) (F x2)) % Found eta_expansion_dep000:=(eta_expansion_dep00 (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))):(((eq (b->Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) (fun (x:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x) (G Xt0)))))) (((eq a) Xx) (F x))))) % Found (eta_expansion_dep00 (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) b0) % Found ((eta_expansion_dep0 (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) b0) % Found (((eta_expansion_dep b) (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) b0) % Found (((eta_expansion_dep b) (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) b0) % Found (((eta_expansion_dep b) (fun (x1:b)=> Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) b0) % Found x4:(((eq a) Xx) (F (G x1))) % Instantiate: x0:=(G x1):b % Found (fun (x4:(((eq a) Xx) (F (G x1))))=> x4) as proof of (((eq a) Xx) (F x0)) % Found (fun (x3:(S x1)) (x4:(((eq a) Xx) (F (G x1))))=> x4) as proof of ((((eq a) Xx) (F (G x1)))->(((eq a) Xx) (F x0))) % Found (fun (x3:(S x1)) (x4:(((eq a) Xx) (F (G x1))))=> x4) as proof of ((S x1)->((((eq a) Xx) (F (G x1)))->(((eq a) Xx) (F x0)))) % Found (and_rect00 (fun (x3:(S x1)) (x4:(((eq a) Xx) (F (G x1))))=> x4)) as proof of (((eq a) Xx) (F x0)) % Found ((and_rect0 (((eq a) Xx) (F x0))) (fun (x3:(S x1)) (x4:(((eq a) Xx) (F (G x1))))=> x4)) as proof of (((eq a) Xx) (F x0)) % Found (((fun (P:Type) (x3:((S x1)->((((eq a) Xx) (F (G x1)))->P)))=> (((((and_rect (S x1)) (((eq a) Xx) (F (G x1)))) P) x3) x2)) (((eq a) Xx) (F x0))) (fun (x3:(S x1)) (x4:(((eq a) Xx) (F (G x1))))=> x4)) as proof of (((eq a) Xx) (F x0)) % Found (((fun (P:Type) (x3:((S x1)->((((eq a) Xx) (F (G x1)))->P)))=> (((((and_rect (S x1)) (((eq a) Xx) (F (G x1)))) P) x3) x2)) (((eq a) Xx) (F x0))) (fun (x3:(S x1)) (x4:(((eq a) Xx) (F (G x1))))=> x4)) as proof of (((eq a) Xx) (F x0)) % Found x4:(((eq a) Xx) (F (G x0))) % Instantiate: x2:=(G x0):b % Found (fun (x4:(((eq a) Xx) (F (G x0))))=> x4) as proof of (((eq a) Xx) (F x2)) % Found (fun (x3:(S x0)) (x4:(((eq a) Xx) (F (G x0))))=> x4) as proof of ((((eq a) Xx) (F (G x0)))->(((eq a) Xx) (F x2))) % Found (fun (x3:(S x0)) (x4:(((eq a) Xx) (F (G x0))))=> x4) as proof of ((S x0)->((((eq a) Xx) (F (G x0)))->(((eq a) Xx) (F x2)))) % Found (and_rect00 (fun (x3:(S x0)) (x4:(((eq a) Xx) (F (G x0))))=> x4)) as proof of (((eq a) Xx) (F x2)) % Found ((and_rect0 (((eq a) Xx) (F x2))) (fun (x3:(S x0)) (x4:(((eq a) Xx) (F (G x0))))=> x4)) as proof of (((eq a) Xx) (F x2)) % Found (((fun (P:Type) (x3:((S x0)->((((eq a) Xx) (F (G x0)))->P)))=> (((((and_rect (S x0)) (((eq a) Xx) (F (G x0)))) P) x3) x1)) (((eq a) Xx) (F x2))) (fun (x3:(S x0)) (x4:(((eq a) Xx) (F (G x0))))=> x4)) as proof of (((eq a) Xx) (F x2)) % Found (((fun (P:Type) (x3:((S x0)->((((eq a) Xx) (F (G x0)))->P)))=> (((((and_rect (S x0)) (((eq a) Xx) (F (G x0)))) P) x3) x1)) (((eq a) Xx) (F x2))) (fun (x3:(S x0)) (x4:(((eq a) Xx) (F (G x0))))=> x4)) as proof of (((eq a) Xx) (F x2)) % 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 ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x0) (G Xt0)))))) (((eq a) Xx) (F x0)))) % Found ((eq_ref Prop) (f x0)) as proof of (((eq Prop) (f x0)) ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x0) (G Xt0)))))) (((eq a) Xx) (F x0)))) % Found ((eq_ref Prop) (f x0)) as proof of (((eq Prop) (f x0)) ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x0) (G Xt0)))))) (((eq a) Xx) (F x0)))) % Found (fun (x0:b)=> ((eq_ref Prop) (f x0))) as proof of (((eq Prop) (f x0)) ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x0) (G Xt0)))))) (((eq a) Xx) (F x0)))) % Found (fun (x0:b)=> ((eq_ref Prop) (f x0))) as proof of (forall (x:b), (((eq Prop) (f x)) ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x) (G Xt0)))))) (((eq a) Xx) (F 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 ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x0) (G Xt0)))))) (((eq a) Xx) (F x0)))) % Found ((eq_ref Prop) (f x0)) as proof of (((eq Prop) (f x0)) ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x0) (G Xt0)))))) (((eq a) Xx) (F x0)))) % Found ((eq_ref Prop) (f x0)) as proof of (((eq Prop) (f x0)) ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x0) (G Xt0)))))) (((eq a) Xx) (F x0)))) % Found (fun (x0:b)=> ((eq_ref Prop) (f x0))) as proof of (((eq Prop) (f x0)) ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x0) (G Xt0)))))) (((eq a) Xx) (F x0)))) % Found (fun (x0:b)=> ((eq_ref Prop) (f x0))) as proof of (forall (x:b), (((eq Prop) (f x)) ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x) (G Xt0)))))) (((eq a) Xx) (F x))))) % Found eta_expansion_dep000:=(eta_expansion_dep00 (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))):(((eq (b->Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) (fun (x:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x) (G Xt0)))))) (((eq a) Xx) (F x))))) % Found (eta_expansion_dep00 (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) b0) % Found ((eta_expansion_dep0 (fun (x3:b)=> Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) b0) % Found (((eta_expansion_dep b) (fun (x3:b)=> Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) b0) % Found (((eta_expansion_dep b) (fun (x3:b)=> Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) b0) % Found (((eta_expansion_dep b) (fun (x3:b)=> Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) b0) % 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 ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x2) (G Xt0)))))) (((eq a) Xx) (F x2)))) % Found ((eq_ref Prop) (f x2)) as proof of (((eq Prop) (f x2)) ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x2) (G Xt0)))))) (((eq a) Xx) (F x2)))) % Found ((eq_ref Prop) (f x2)) as proof of (((eq Prop) (f x2)) ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x2) (G Xt0)))))) (((eq a) Xx) (F x2)))) % Found (fun (x2:b)=> ((eq_ref Prop) (f x2))) as proof of (((eq Prop) (f x2)) ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x2) (G Xt0)))))) (((eq a) Xx) (F x2)))) % Found (fun (x2:b)=> ((eq_ref Prop) (f x2))) as proof of (forall (x:b), (((eq Prop) (f x)) ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x) (G Xt0)))))) (((eq a) Xx) (F 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 ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x2) (G Xt0)))))) (((eq a) Xx) (F x2)))) % Found ((eq_ref Prop) (f x2)) as proof of (((eq Prop) (f x2)) ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x2) (G Xt0)))))) (((eq a) Xx) (F x2)))) % Found ((eq_ref Prop) (f x2)) as proof of (((eq Prop) (f x2)) ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x2) (G Xt0)))))) (((eq a) Xx) (F x2)))) % Found (fun (x2:b)=> ((eq_ref Prop) (f x2))) as proof of (((eq Prop) (f x2)) ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x2) (G Xt0)))))) (((eq a) Xx) (F x2)))) % Found (fun (x2:b)=> ((eq_ref Prop) (f x2))) as proof of (forall (x:b), (((eq Prop) (f x)) ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x) (G Xt0)))))) (((eq a) Xx) (F x))))) % Found x4:(((eq a) Xx) (F (G x1))) % Instantiate: x0:=(G x1):b % Found (fun (x4:(((eq a) Xx) (F (G x1))))=> x4) as proof of (((eq a) Xx) (F x0)) % Found (fun (x3:(S x1)) (x4:(((eq a) Xx) (F (G x1))))=> x4) as proof of ((((eq a) Xx) (F (G x1)))->(((eq a) Xx) (F x0))) % Found (fun (x3:(S x1)) (x4:(((eq a) Xx) (F (G x1))))=> x4) as proof of ((S x1)->((((eq a) Xx) (F (G x1)))->(((eq a) Xx) (F x0)))) % Found (and_rect00 (fun (x3:(S x1)) (x4:(((eq a) Xx) (F (G x1))))=> x4)) as proof of (((eq a) Xx) (F x0)) % Found ((and_rect0 (((eq a) Xx) (F x0))) (fun (x3:(S x1)) (x4:(((eq a) Xx) (F (G x1))))=> x4)) as proof of (((eq a) Xx) (F x0)) % Found (((fun (P:Type) (x3:((S x1)->((((eq a) Xx) (F (G x1)))->P)))=> (((((and_rect (S x1)) (((eq a) Xx) (F (G x1)))) P) x3) x2)) (((eq a) Xx) (F x0))) (fun (x3:(S x1)) (x4:(((eq a) Xx) (F (G x1))))=> x4)) as proof of (((eq a) Xx) (F x0)) % Found (fun (x2:((and (S x1)) (((eq a) Xx) (F (G x1)))))=> (((fun (P:Type) (x3:((S x1)->((((eq a) Xx) (F (G x1)))->P)))=> (((((and_rect (S x1)) (((eq a) Xx) (F (G x1)))) P) x3) x2)) (((eq a) Xx) (F x0))) (fun (x3:(S x1)) (x4:(((eq a) Xx) (F (G x1))))=> x4))) as proof of (((eq a) Xx) (F x0)) % Found eq_ref00:=(eq_ref0 (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))):(((eq (b->Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) % Found (eq_ref0 (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) b0) % Found ((eq_ref (b->Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) b0) % Found ((eq_ref (b->Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) b0) % Found ((eq_ref (b->Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) b0) % 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 ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0)))))) (((eq a) Xx) (F x4)))) % Found ((eq_ref Prop) (f x4)) as proof of (((eq Prop) (f x4)) ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0)))))) (((eq a) Xx) (F x4)))) % Found ((eq_ref Prop) (f x4)) as proof of (((eq Prop) (f x4)) ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0)))))) (((eq a) Xx) (F x4)))) % Found (fun (x4:b)=> ((eq_ref Prop) (f x4))) as proof of (((eq Prop) (f x4)) ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0)))))) (((eq a) Xx) (F x4)))) % Found (fun (x4:b)=> ((eq_ref Prop) (f x4))) as proof of (forall (x:b), (((eq Prop) (f x)) ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x) (G Xt0)))))) (((eq a) Xx) (F x))))) % 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 ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0)))))) (((eq a) Xx) (F x4)))) % Found ((eq_ref Prop) (f x4)) as proof of (((eq Prop) (f x4)) ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0)))))) (((eq a) Xx) (F x4)))) % Found ((eq_ref Prop) (f x4)) as proof of (((eq Prop) (f x4)) ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0)))))) (((eq a) Xx) (F x4)))) % Found (fun (x4:b)=> ((eq_ref Prop) (f x4))) as proof of (((eq Prop) (f x4)) ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0)))))) (((eq a) Xx) (F x4)))) % Found (fun (x4:b)=> ((eq_ref Prop) (f x4))) as proof of (forall (x:b), (((eq Prop) (f x)) ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x) (G Xt0)))))) (((eq a) Xx) (F x))))) % 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 eq_sym010:=(eq_sym01 (F (G x1))):((((eq a) Xx) (F (G x1)))->(((eq a) (F (G x1))) Xx)) % Found (eq_sym01 (F (G x1))) as proof of ((((eq a) Xx) (F (G x1)))->(((eq a) (F x0)) Xx)) % Found ((eq_sym0 Xx) (F (G x1))) as proof of ((((eq a) Xx) (F (G x1)))->(((eq a) (F x0)) Xx)) % Found ((eq_sym0 Xx) (F (G x1))) as proof of ((((eq a) Xx) (F (G x1)))->(((eq a) (F x0)) Xx)) % Found (fun (x3:(S x1))=> ((eq_sym0 Xx) (F (G x1)))) as proof of ((((eq a) Xx) (F (G x1)))->(((eq a) (F x0)) Xx)) % Found (fun (x3:(S x1))=> ((eq_sym0 Xx) (F (G x1)))) as proof of ((S x1)->((((eq a) Xx) (F (G x1)))->(((eq a) (F x0)) Xx))) % Found (and_rect00 (fun (x3:(S x1))=> ((eq_sym0 Xx) (F (G x1))))) as proof of (((eq a) (F x0)) Xx) % Found ((and_rect0 (((eq a) (F x0)) Xx)) (fun (x3:(S x1))=> ((eq_sym0 Xx) (F (G x1))))) as proof of (((eq a) (F x0)) Xx) % Found (((fun (P:Type) (x3:((S x1)->((((eq a) Xx) (F (G x1)))->P)))=> (((((and_rect (S x1)) (((eq a) Xx) (F (G x1)))) P) x3) x2)) (((eq a) (F x0)) Xx)) (fun (x3:(S x1))=> ((eq_sym0 Xx) (F (G x1))))) as proof of (((eq a) (F x0)) Xx) % Found (((fun (P:Type) (x3:((S x1)->((((eq a) Xx) (F (G x1)))->P)))=> (((((and_rect (S x1)) (((eq a) Xx) (F (G x1)))) P) x3) x2)) (((eq a) (F x0)) Xx)) (fun (x3:(S x1))=> ((eq_sym0 Xx) (F (G x1))))) as proof of (((eq a) (F x0)) Xx) % Found (eq_sym000 (((fun (P:Type) (x3:((S x1)->((((eq a) Xx) (F (G x1)))->P)))=> (((((and_rect (S x1)) (((eq a) Xx) (F (G x1)))) P) x3) x2)) (((eq a) (F x0)) Xx)) (fun (x3:(S x1))=> ((eq_sym0 Xx) (F (G x1)))))) as proof of (((eq a) Xx) (F x0)) % Found ((eq_sym00 Xx) (((fun (P:Type) (x3:((S x1)->((((eq a) Xx) (F (G x1)))->P)))=> (((((and_rect (S x1)) (((eq a) Xx) (F (G x1)))) P) x3) x2)) (((eq a) (F x0)) Xx)) (fun (x3:(S x1))=> ((eq_sym0 Xx) (F (G x1)))))) as proof of (((eq a) Xx) (F x0)) % Found (((eq_sym0 (F x0)) Xx) (((fun (P:Type) (x3:((S x1)->((((eq a) Xx) (F (G x1)))->P)))=> (((((and_rect (S x1)) (((eq a) Xx) (F (G x1)))) P) x3) x2)) (((eq a) (F x0)) Xx)) (fun (x3:(S x1))=> ((eq_sym0 Xx) (F (G x1)))))) as proof of (((eq a) Xx) (F x0)) % Found ((((eq_sym a) (F x0)) Xx) (((fun (P:Type) (x3:((S x1)->((((eq a) Xx) (F (G x1)))->P)))=> (((((and_rect (S x1)) (((eq a) Xx) (F (G x1)))) P) x3) x2)) (((eq a) (F x0)) Xx)) (fun (x3:(S x1))=> (((eq_sym a) Xx) (F (G x1)))))) as proof of (((eq a) Xx) (F x0)) % Found (fun (x2:((and (S x1)) (((eq a) Xx) (F (G x1)))))=> ((((eq_sym a) (F x0)) Xx) (((fun (P:Type) (x3:((S x1)->((((eq a) Xx) (F (G x1)))->P)))=> (((((and_rect (S x1)) (((eq a) Xx) (F (G x1)))) P) x3) x2)) (((eq a) (F x0)) Xx)) (fun (x3:(S x1))=> (((eq_sym a) Xx) (F (G x1))))))) as proof of (((eq a) Xx) (F x0)) % Found eq_sym010:=(eq_sym01 (F (G x1))):((((eq a) Xx) (F (G x1)))->(((eq a) (F (G x1))) Xx)) % Found (eq_sym01 (F (G x1))) as proof of ((((eq a) Xx) (F (G x1)))->(((eq a) (F x0)) Xx)) % Found ((eq_sym0 Xx) (F (G x1))) as proof of ((((eq a) Xx) (F (G x1)))->(((eq a) (F x0)) Xx)) % Found ((eq_sym0 Xx) (F (G x1))) as proof of ((((eq a) Xx) (F (G x1)))->(((eq a) (F x0)) Xx)) % Found (fun (x3:(S x1))=> ((eq_sym0 Xx) (F (G x1)))) as proof of ((((eq a) Xx) (F (G x1)))->(((eq a) (F x0)) Xx)) % Found (fun (x3:(S x1))=> ((eq_sym0 Xx) (F (G x1)))) as proof of ((S x1)->((((eq a) Xx) (F (G x1)))->(((eq a) (F x0)) Xx))) % Found (and_rect00 (fun (x3:(S x1))=> ((eq_sym0 Xx) (F (G x1))))) as proof of (((eq a) (F x0)) Xx) % Found ((and_rect0 (((eq a) (F x0)) Xx)) (fun (x3:(S x1))=> ((eq_sym0 Xx) (F (G x1))))) as proof of (((eq a) (F x0)) Xx) % Found (((fun (P:Type) (x3:((S x1)->((((eq a) Xx) (F (G x1)))->P)))=> (((((and_rect (S x1)) (((eq a) Xx) (F (G x1)))) P) x3) x2)) (((eq a) (F x0)) Xx)) (fun (x3:(S x1))=> ((eq_sym0 Xx) (F (G x1))))) as proof of (((eq a) (F x0)) Xx) % Found (fun (x2:((and (S x1)) (((eq a) Xx) (F (G x1)))))=> (((fun (P:Type) (x3:((S x1)->((((eq a) Xx) (F (G x1)))->P)))=> (((((and_rect (S x1)) (((eq a) Xx) (F (G x1)))) P) x3) x2)) (((eq a) (F x0)) Xx)) (fun (x3:(S x1))=> ((eq_sym0 Xx) (F (G x1)))))) as proof of (((eq a) (F x0)) Xx) % Found eq_ref00:=(eq_ref0 x2):(((eq b) x2) x2) % Found (eq_ref0 x2) as proof of (((eq b) x2) (G x3)) % Found ((eq_ref b) x2) as proof of (((eq b) x2) (G x3)) % Found ((eq_ref b) x2) as proof of (((eq b) x2) (G x3)) % Found ((eq_ref b) x2) as proof of (((eq b) x2) (G x3)) % 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) (F x0)) % Found ((eq_ref a) b0) as proof of (((eq a) b0) (F x0)) % Found ((eq_ref a) b0) as proof of (((eq a) b0) (F x0)) % Found ((eq_ref a) b0) as proof of (((eq a) b0) (F x0)) % Found eq_ref00:=(eq_ref0 x2):(((eq b) x2) x2) % Found (eq_ref0 x2) as proof of (((eq b) x2) (G x3)) % Found ((eq_ref b) x2) as proof of (((eq b) x2) (G x3)) % Found ((eq_ref b) x2) as proof of (((eq b) x2) (G x3)) % Found ((eq_ref b) x2) as proof of (((eq b) x2) (G x3)) % Found eq_ref00:=(eq_ref0 x0):(((eq b) x0) x0) % Found (eq_ref0 x0) as proof of (((eq b) x0) (G x3)) % Found ((eq_ref b) x0) as proof of (((eq b) x0) (G x3)) % Found ((eq_ref b) x0) as proof of (((eq b) x0) (G x3)) % Found ((eq_ref b) x0) as proof of (((eq b) x0) (G x3)) % Found eq_ref00:=(eq_ref0 x0):(((eq b) x0) x0) % Found (eq_ref0 x0) as proof of (((eq b) x0) (G x3)) % Found ((eq_ref b) x0) as proof of (((eq b) x0) (G x3)) % Found ((eq_ref b) x0) as proof of (((eq b) x0) (G x3)) % Found ((eq_ref b) x0) as proof of (((eq b) x0) (G x3)) % Found x2:(S x0) % Instantiate: x5:=x0:c % Found x2 as proof of (S x5) % Found eq_ref00:=(eq_ref0 x4):(((eq b) x4) x4) % Found (eq_ref0 x4) as proof of (((eq b) x4) (G x5)) % Found ((eq_ref b) x4) as proof of (((eq b) x4) (G x5)) % Found ((eq_ref b) x4) as proof of (((eq b) x4) (G x5)) % Found ((eq_ref b) x4) as proof of (((eq b) x4) (G x5)) % Found ((conj10 x2) ((eq_ref b) x4)) as proof of ((and (S x5)) (((eq b) x4) (G x5))) % Found (((conj1 (((eq b) x4) (G x5))) x2) ((eq_ref b) x4)) as proof of ((and (S x5)) (((eq b) x4) (G x5))) % Found ((((conj (S x5)) (((eq b) x4) (G x5))) x2) ((eq_ref b) x4)) as proof of ((and (S x5)) (((eq b) x4) (G x5))) % Found ((((conj (S x5)) (((eq b) x4) (G x5))) x2) ((eq_ref b) x4)) as proof of ((and (S x5)) (((eq b) x4) (G x5))) % Found (ex_intro100 ((((conj (S x5)) (((eq b) x4) (G x5))) x2) ((eq_ref b) x4))) as proof of ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0))))) % Found ((ex_intro10 x0) ((((conj (S x0)) (((eq b) x4) (G x0))) x2) ((eq_ref b) x4))) as proof of ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0))))) % Found (((ex_intro1 (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) x4) (G x0))) x2) ((eq_ref b) x4))) as proof of ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0))))) % Found ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) x4) (G x0))) x2) ((eq_ref b) x4))) as proof of ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0))))) % Found ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) x4) (G x0))) x2) ((eq_ref b) x4))) as proof of ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0))))) % Found ((conj00 ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) x4) (G x0))) x2) ((eq_ref b) x4)))) x3) as proof of ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0)))))) (((eq a) Xx) (F x4))) % Found (((conj0 (((eq a) Xx) (F x4))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) x4) (G x0))) x2) ((eq_ref b) x4)))) x3) as proof of ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0)))))) (((eq a) Xx) (F x4))) % Found ((((conj ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0)))))) (((eq a) Xx) (F x4))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) x4) (G x0))) x2) ((eq_ref b) x4)))) x3) as proof of ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0)))))) (((eq a) Xx) (F x4))) % Found ((((conj ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0)))))) (((eq a) Xx) (F x4))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) x4) (G x0))) x2) ((eq_ref b) x4)))) x3) as proof of ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0)))))) (((eq a) Xx) (F x4))) % Found (ex_intro000 ((((conj ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0)))))) (((eq a) Xx) (F x4))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) x4) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) x4) (G x0))) x2) ((eq_ref b) x4)))) x3)) as proof of ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) % Found ((ex_intro00 (G x0)) ((((conj ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0)))))) (((eq a) Xx) (F (G x0)))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) (G x0)) (G x0))) x2) ((eq_ref b) (G x0))))) x3)) as proof of ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) % Found (((ex_intro0 (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) (G x0)) ((((conj ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0)))))) (((eq a) Xx) (F (G x0)))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) (G x0)) (G x0))) x2) ((eq_ref b) (G x0))))) x3)) as proof of ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) % Found ((((ex_intro b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) (G x0)) ((((conj ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0)))))) (((eq a) Xx) (F (G x0)))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) (G x0)) (G x0))) x2) ((eq_ref b) (G x0))))) x3)) as proof of ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) % Found (fun (x3:(((eq a) Xx) (F (G x0))))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) (G x0)) ((((conj ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0)))))) (((eq a) Xx) (F (G x0)))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) (G x0)) (G x0))) x2) ((eq_ref b) (G x0))))) x3))) as proof of ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) % Found (fun (x2:(S x0)) (x3:(((eq a) Xx) (F (G x0))))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) (G x0)) ((((conj ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0)))))) (((eq a) Xx) (F (G x0)))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) (G x0)) (G x0))) x2) ((eq_ref b) (G x0))))) x3))) as proof of ((((eq a) Xx) (F (G x0)))->((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) % Found (fun (x2:(S x0)) (x3:(((eq a) Xx) (F (G x0))))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) (G x0)) ((((conj ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0)))))) (((eq a) Xx) (F (G x0)))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) (G x0)) (G x0))) x2) ((eq_ref b) (G x0))))) x3))) as proof of ((S x0)->((((eq a) Xx) (F (G x0)))->((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))))) % Found (and_rect00 (fun (x2:(S x0)) (x3:(((eq a) Xx) (F (G x0))))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) (G x0)) ((((conj ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0)))))) (((eq a) Xx) (F (G x0)))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) (G x0)) (G x0))) x2) ((eq_ref b) (G x0))))) x3)))) as proof of ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) % Found ((and_rect0 ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) (fun (x2:(S x0)) (x3:(((eq a) Xx) (F (G x0))))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) (G x0)) ((((conj ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0)))))) (((eq a) Xx) (F (G x0)))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) (G x0)) (G x0))) x2) ((eq_ref b) (G x0))))) x3)))) as proof of ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) % Found (((fun (P:Type) (x2:((S x0)->((((eq a) Xx) (F (G x0)))->P)))=> (((((and_rect (S x0)) (((eq a) Xx) (F (G x0)))) P) x2) x1)) ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) (fun (x2:(S x0)) (x3:(((eq a) Xx) (F (G x0))))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) (G x0)) ((((conj ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0)))))) (((eq a) Xx) (F (G x0)))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) (G x0)) (G x0))) x2) ((eq_ref b) (G x0))))) x3)))) as proof of ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) % Found (fun (x1:((and (S x0)) (((eq a) Xx) (F (G x0)))))=> (((fun (P:Type) (x2:((S x0)->((((eq a) Xx) (F (G x0)))->P)))=> (((((and_rect (S x0)) (((eq a) Xx) (F (G x0)))) P) x2) x1)) ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) (fun (x2:(S x0)) (x3:(((eq a) Xx) (F (G x0))))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) (G x0)) ((((conj ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0)))))) (((eq a) Xx) (F (G x0)))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) (G x0)) (G x0))) x2) ((eq_ref b) (G x0))))) x3))))) as proof of ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) % Found (fun (x0:c) (x1:((and (S x0)) (((eq a) Xx) (F (G x0)))))=> (((fun (P:Type) (x2:((S x0)->((((eq a) Xx) (F (G x0)))->P)))=> (((((and_rect (S x0)) (((eq a) Xx) (F (G x0)))) P) x2) x1)) ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) (fun (x2:(S x0)) (x3:(((eq a) Xx) (F (G x0))))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) (G x0)) ((((conj ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0)))))) (((eq a) Xx) (F (G x0)))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) (G x0)) (G x0))) x2) ((eq_ref b) (G x0))))) x3))))) as proof of (((and (S x0)) (((eq a) Xx) (F (G x0))))->((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) % Found (fun (x0:c) (x1:((and (S x0)) (((eq a) Xx) (F (G x0)))))=> (((fun (P:Type) (x2:((S x0)->((((eq a) Xx) (F (G x0)))->P)))=> (((((and_rect (S x0)) (((eq a) Xx) (F (G x0)))) P) x2) x1)) ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) (fun (x2:(S x0)) (x3:(((eq a) Xx) (F (G x0))))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) (G x0)) ((((conj ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0)))))) (((eq a) Xx) (F (G x0)))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) (G x0)) (G x0))) x2) ((eq_ref b) (G x0))))) x3))))) as proof of (forall (x:c), (((and (S x)) (((eq a) Xx) (F (G x))))->((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))))) % Found (ex_ind00 (fun (x0:c) (x1:((and (S x0)) (((eq a) Xx) (F (G x0)))))=> (((fun (P:Type) (x2:((S x0)->((((eq a) Xx) (F (G x0)))->P)))=> (((((and_rect (S x0)) (((eq a) Xx) (F (G x0)))) P) x2) x1)) ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) (fun (x2:(S x0)) (x3:(((eq a) Xx) (F (G x0))))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) (G x0)) ((((conj ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0)))))) (((eq a) Xx) (F (G x0)))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) (G x0)) (G x0))) x2) ((eq_ref b) (G x0))))) x3)))))) as proof of ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) % Found ((ex_ind0 ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) (fun (x0:c) (x1:((and (S x0)) (((eq a) Xx) (F (G x0)))))=> (((fun (P:Type) (x2:((S x0)->((((eq a) Xx) (F (G x0)))->P)))=> (((((and_rect (S x0)) (((eq a) Xx) (F (G x0)))) P) x2) x1)) ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) (fun (x2:(S x0)) (x3:(((eq a) Xx) (F (G x0))))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) (G x0)) ((((conj ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0)))))) (((eq a) Xx) (F (G x0)))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) (G x0)) (G x0))) x2) ((eq_ref b) (G x0))))) x3)))))) as proof of ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) % Found (((fun (P:Prop) (x0:(forall (x:c), (((and (S x)) (((eq a) Xx) (F (G x))))->P)))=> (((((ex_ind c) (fun (Xt:c)=> ((and (S Xt)) (((eq a) Xx) (F (G Xt)))))) P) x0) x)) ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) (fun (x0:c) (x1:((and (S x0)) (((eq a) Xx) (F (G x0)))))=> (((fun (P:Type) (x2:((S x0)->((((eq a) Xx) (F (G x0)))->P)))=> (((((and_rect (S x0)) (((eq a) Xx) (F (G x0)))) P) x2) x1)) ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) (fun (x2:(S x0)) (x3:(((eq a) Xx) (F (G x0))))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) (G x0)) ((((conj ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0)))))) (((eq a) Xx) (F (G x0)))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) (G x0)) (G x0))) x2) ((eq_ref b) (G x0))))) x3)))))) as proof of ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) % Found (fun (x:((ex c) (fun (Xt:c)=> ((and (S Xt)) (((eq a) Xx) (F (G Xt)))))))=> (((fun (P:Prop) (x0:(forall (x:c), (((and (S x)) (((eq a) Xx) (F (G x))))->P)))=> (((((ex_ind c) (fun (Xt:c)=> ((and (S Xt)) (((eq a) Xx) (F (G Xt)))))) P) x0) x)) ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) (fun (x0:c) (x1:((and (S x0)) (((eq a) Xx) (F (G x0)))))=> (((fun (P:Type) (x2:((S x0)->((((eq a) Xx) (F (G x0)))->P)))=> (((((and_rect (S x0)) (((eq a) Xx) (F (G x0)))) P) x2) x1)) ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) (fun (x2:(S x0)) (x3:(((eq a) Xx) (F (G x0))))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) (G x0)) ((((conj ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0)))))) (((eq a) Xx) (F (G x0)))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) (G x0)) (G x0))) x2) ((eq_ref b) (G x0))))) x3))))))) as proof of ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) % Found (fun (Xx:a) (x:((ex c) (fun (Xt:c)=> ((and (S Xt)) (((eq a) Xx) (F (G Xt)))))))=> (((fun (P:Prop) (x0:(forall (x:c), (((and (S x)) (((eq a) Xx) (F (G x))))->P)))=> (((((ex_ind c) (fun (Xt:c)=> ((and (S Xt)) (((eq a) Xx) (F (G Xt)))))) P) x0) x)) ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) (fun (x0:c) (x1:((and (S x0)) (((eq a) Xx) (F (G x0)))))=> (((fun (P:Type) (x2:((S x0)->((((eq a) Xx) (F (G x0)))->P)))=> (((((and_rect (S x0)) (((eq a) Xx) (F (G x0)))) P) x2) x1)) ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) (fun (x2:(S x0)) (x3:(((eq a) Xx) (F (G x0))))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) (G x0)) ((((conj ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0)))))) (((eq a) Xx) (F (G x0)))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) (G x0)) (G x0))) x2) ((eq_ref b) (G x0))))) x3))))))) as proof of (((ex c) (fun (Xt:c)=> ((and (S Xt)) (((eq a) Xx) (F (G Xt))))))->((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) % Found (fun (S:(c->Prop)) (Xx:a) (x:((ex c) (fun (Xt:c)=> ((and (S Xt)) (((eq a) Xx) (F (G Xt)))))))=> (((fun (P:Prop) (x0:(forall (x:c), (((and (S x)) (((eq a) Xx) (F (G x))))->P)))=> (((((ex_ind c) (fun (Xt:c)=> ((and (S Xt)) (((eq a) Xx) (F (G Xt)))))) P) x0) x)) ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) (fun (x0:c) (x1:((and (S x0)) (((eq a) Xx) (F (G x0)))))=> (((fun (P:Type) (x2:((S x0)->((((eq a) Xx) (F (G x0)))->P)))=> (((((and_rect (S x0)) (((eq a) Xx) (F (G x0)))) P) x2) x1)) ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) (fun (x2:(S x0)) (x3:(((eq a) Xx) (F (G x0))))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) (G x0)) ((((conj ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0)))))) (((eq a) Xx) (F (G x0)))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) (G x0)) (G x0))) x2) ((eq_ref b) (G x0))))) x3))))))) as proof of (forall (Xx:a), (((ex c) (fun (Xt:c)=> ((and (S Xt)) (((eq a) Xx) (F (G Xt))))))->((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))))) % Found (fun (G:(c->b)) (S:(c->Prop)) (Xx:a) (x:((ex c) (fun (Xt:c)=> ((and (S Xt)) (((eq a) Xx) (F (G Xt)))))))=> (((fun (P:Prop) (x0:(forall (x:c), (((and (S x)) (((eq a) Xx) (F (G x))))->P)))=> (((((ex_ind c) (fun (Xt:c)=> ((and (S Xt)) (((eq a) Xx) (F (G Xt)))))) P) x0) x)) ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) (fun (x0:c) (x1:((and (S x0)) (((eq a) Xx) (F (G x0)))))=> (((fun (P:Type) (x2:((S x0)->((((eq a) Xx) (F (G x0)))->P)))=> (((((and_rect (S x0)) (((eq a) Xx) (F (G x0)))) P) x2) x1)) ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) (fun (x2:(S x0)) (x3:(((eq a) Xx) (F (G x0))))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) (G x0)) ((((conj ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0)))))) (((eq a) Xx) (F (G x0)))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) (G x0)) (G x0))) x2) ((eq_ref b) (G x0))))) x3))))))) as proof of (forall (S:(c->Prop)) (Xx:a), (((ex c) (fun (Xt:c)=> ((and (S Xt)) (((eq a) Xx) (F (G Xt))))))->((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))))) % Found (fun (F:(b->a)) (G:(c->b)) (S:(c->Prop)) (Xx:a) (x:((ex c) (fun (Xt:c)=> ((and (S Xt)) (((eq a) Xx) (F (G Xt)))))))=> (((fun (P:Prop) (x0:(forall (x:c), (((and (S x)) (((eq a) Xx) (F (G x))))->P)))=> (((((ex_ind c) (fun (Xt:c)=> ((and (S Xt)) (((eq a) Xx) (F (G Xt)))))) P) x0) x)) ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) (fun (x0:c) (x1:((and (S x0)) (((eq a) Xx) (F (G x0)))))=> (((fun (P:Type) (x2:((S x0)->((((eq a) Xx) (F (G x0)))->P)))=> (((((and_rect (S x0)) (((eq a) Xx) (F (G x0)))) P) x2) x1)) ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) (fun (x2:(S x0)) (x3:(((eq a) Xx) (F (G x0))))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) (G x0)) ((((conj ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0)))))) (((eq a) Xx) (F (G x0)))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) (G x0)) (G x0))) x2) ((eq_ref b) (G x0))))) x3))))))) as proof of (forall (G:(c->b)) (S:(c->Prop)) (Xx:a), (((ex c) (fun (Xt:c)=> ((and (S Xt)) (((eq a) Xx) (F (G Xt))))))->((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))))) % Found (fun (F:(b->a)) (G:(c->b)) (S:(c->Prop)) (Xx:a) (x:((ex c) (fun (Xt:c)=> ((and (S Xt)) (((eq a) Xx) (F (G Xt)))))))=> (((fun (P:Prop) (x0:(forall (x:c), (((and (S x)) (((eq a) Xx) (F (G x))))->P)))=> (((((ex_ind c) (fun (Xt:c)=> ((and (S Xt)) (((eq a) Xx) (F (G Xt)))))) P) x0) x)) ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) (fun (x0:c) (x1:((and (S x0)) (((eq a) Xx) (F (G x0)))))=> (((fun (P:Type) (x2:((S x0)->((((eq a) Xx) (F (G x0)))->P)))=> (((((and_rect (S x0)) (((eq a) Xx) (F (G x0)))) P) x2) x1)) ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) (fun (x2:(S x0)) (x3:(((eq a) Xx) (F (G x0))))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) (G x0)) ((((conj ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0)))))) (((eq a) Xx) (F (G x0)))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) (G x0)) (G x0))) x2) ((eq_ref b) (G x0))))) x3))))))) as proof of (forall (F:(b->a)) (G:(c->b)) (S:(c->Prop)) (Xx:a), (((ex c) (fun (Xt:c)=> ((and (S Xt)) (((eq a) Xx) (F (G Xt))))))->((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))))) % Got proof (fun (F:(b->a)) (G:(c->b)) (S:(c->Prop)) (Xx:a) (x:((ex c) (fun (Xt:c)=> ((and (S Xt)) (((eq a) Xx) (F (G Xt)))))))=> (((fun (P:Prop) (x0:(forall (x:c), (((and (S x)) (((eq a) Xx) (F (G x))))->P)))=> (((((ex_ind c) (fun (Xt:c)=> ((and (S Xt)) (((eq a) Xx) (F (G Xt)))))) P) x0) x)) ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) (fun (x0:c) (x1:((and (S x0)) (((eq a) Xx) (F (G x0)))))=> (((fun (P:Type) (x2:((S x0)->((((eq a) Xx) (F (G x0)))->P)))=> (((((and_rect (S x0)) (((eq a) Xx) (F (G x0)))) P) x2) x1)) ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) (fun (x2:(S x0)) (x3:(((eq a) Xx) (F (G x0))))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) (G x0)) ((((conj ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0)))))) (((eq a) Xx) (F (G x0)))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) (G x0)) (G x0))) x2) ((eq_ref b) (G x0))))) x3))))))) % Time elapsed = 20.074580s % node=2941 cost=1702.000000 depth=38 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % (fun (F:(b->a)) (G:(c->b)) (S:(c->Prop)) (Xx:a) (x:((ex c) (fun (Xt:c)=> ((and (S Xt)) (((eq a) Xx) (F (G Xt)))))))=> (((fun (P:Prop) (x0:(forall (x:c), (((and (S x)) (((eq a) Xx) (F (G x))))->P)))=> (((((ex_ind c) (fun (Xt:c)=> ((and (S Xt)) (((eq a) Xx) (F (G Xt)))))) P) x0) x)) ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) (fun (x0:c) (x1:((and (S x0)) (((eq a) Xx) (F (G x0)))))=> (((fun (P:Type) (x2:((S x0)->((((eq a) Xx) (F (G x0)))->P)))=> (((((and_rect (S x0)) (((eq a) Xx) (F (G x0)))) P) x2) x1)) ((ex b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt)))))) (fun (x2:(S x0)) (x3:(((eq a) Xx) (F (G x0))))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) Xt) (G Xt0)))))) (((eq a) Xx) (F Xt))))) (G x0)) ((((conj ((ex c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0)))))) (((eq a) Xx) (F (G x0)))) ((((ex_intro c) (fun (Xt0:c)=> ((and (S Xt0)) (((eq b) (G x0)) (G Xt0))))) x0) ((((conj (S x0)) (((eq b) (G x0)) (G x0))) x2) ((eq_ref b) (G x0))))) x3))))))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------