%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEU686^2 : TPTP v6.1.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n096.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:32:49 EDT 2014 % Result : Theorem 142.39s % Output : Proof 142.39s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SEU686^2 : TPTP v6.1.0. Released v3.7.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n096.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:10:51 CDT 2014 % % CPUTime : 142.39 % 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 0x27b8ea8>, <kernel.DependentProduct object at 0x27b86c8>) of role type named in_type % Using role type % Declaring in:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x27ba3f8>, <kernel.Single object at 0x27b8998>) of role type named emptyset_type % Using role type % Declaring emptyset:fofType % FOF formula (<kernel.Constant object at 0x27b86c8>, <kernel.DependentProduct object at 0x27b8cf8>) of role type named setadjoin_type % Using role type % Declaring setadjoin:(fofType->(fofType->fofType)) % FOF formula (<kernel.Constant object at 0x27b88c0>, <kernel.DependentProduct object at 0x27b8128>) of role type named dsetconstr_type % Using role type % Declaring dsetconstr:(fofType->((fofType->Prop)->fofType)) % FOF formula (<kernel.Constant object at 0x27b83f8>, <kernel.DependentProduct object at 0x27b86c8>) of role type named subset_type % Using role type % Declaring subset:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x27b84d0>, <kernel.DependentProduct object at 0x27b88c0>) of role type named kpair_type % Using role type % Declaring kpair:(fofType->(fofType->fofType)) % FOF formula (<kernel.Constant object at 0x27b85f0>, <kernel.DependentProduct object at 0x27b83f8>) of role type named cartprod_type % Using role type % Declaring cartprod:(fofType->(fofType->fofType)) % FOF formula (<kernel.Constant object at 0x27b8cf8>, <kernel.DependentProduct object at 0x27b8a70>) of role type named singleton_type % Using role type % Declaring singleton:(fofType->Prop) % FOF formula (((eq (fofType->Prop)) singleton) (fun (A:fofType)=> ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (((eq fofType) A) ((setadjoin Xx) emptyset))))))) of role definition named singleton % A new definition: (((eq (fofType->Prop)) singleton) (fun (A:fofType)=> ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (((eq fofType) A) ((setadjoin Xx) emptyset))))))) % Defined: singleton:=(fun (A:fofType)=> ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (((eq fofType) A) ((setadjoin Xx) emptyset)))))) % FOF formula (<kernel.Constant object at 0x27b8a70>, <kernel.DependentProduct object at 0x27b8dd0>) of role type named ex1_type % Using role type % Declaring ex1:(fofType->((fofType->Prop)->Prop)) % FOF formula (((eq (fofType->((fofType->Prop)->Prop))) ex1) (fun (A:fofType) (Xphi:(fofType->Prop))=> (singleton ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))))) of role definition named ex1 % A new definition: (((eq (fofType->((fofType->Prop)->Prop))) ex1) (fun (A:fofType) (Xphi:(fofType->Prop))=> (singleton ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))))) % Defined: ex1:=(fun (A:fofType) (Xphi:(fofType->Prop))=> (singleton ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) % FOF formula (<kernel.Constant object at 0x27b8dd0>, <kernel.DependentProduct object at 0x27b8050>) of role type named breln_type % Using role type % Declaring breln:(fofType->(fofType->(fofType->Prop))) % FOF formula (((eq (fofType->(fofType->(fofType->Prop)))) breln) (fun (A:fofType) (B:fofType) (C:fofType)=> ((subset C) ((cartprod A) B)))) of role definition named breln % A new definition: (((eq (fofType->(fofType->(fofType->Prop)))) breln) (fun (A:fofType) (B:fofType) (C:fofType)=> ((subset C) ((cartprod A) B)))) % Defined: breln:=(fun (A:fofType) (B:fofType) (C:fofType)=> ((subset C) ((cartprod A) B))) % FOF formula (<kernel.Constant object at 0x27b8ab8>, <kernel.DependentProduct object at 0x27b8488>) of role type named func_type % Using role type % Declaring func:(fofType->(fofType->(fofType->Prop))) % FOF formula (((eq (fofType->(fofType->(fofType->Prop)))) func) (fun (A:fofType) (B:fofType) (R:fofType)=> ((and (((breln A) B) R)) (forall (Xx:fofType), (((in Xx) A)->((ex1 B) (fun (Xy:fofType)=> ((in ((kpair Xx) Xy)) R)))))))) of role definition named func % A new definition: (((eq (fofType->(fofType->(fofType->Prop)))) func) (fun (A:fofType) (B:fofType) (R:fofType)=> ((and (((breln A) B) R)) (forall (Xx:fofType), (((in Xx) A)->((ex1 B) (fun (Xy:fofType)=> ((in ((kpair Xx) Xy)) R)))))))) % Defined: func:=(fun (A:fofType) (B:fofType) (R:fofType)=> ((and (((breln A) B) R)) (forall (Xx:fofType), (((in Xx) A)->((ex1 B) (fun (Xy:fofType)=> ((in ((kpair Xx) Xy)) R))))))) % FOF formula (<kernel.Constant object at 0x2a19f38>, <kernel.DependentProduct object at 0x27b83f8>) of role type named ap_type % Using role type % Declaring ap:(fofType->(fofType->(fofType->(fofType->fofType)))) % FOF formula (<kernel.Constant object at 0x27b8dd0>, <kernel.Sort object at 0x2874878>) of role type named app_type % Using role type % Declaring app:Prop % FOF formula (((eq Prop) app) (forall (A:fofType) (B:fofType) (Xf:fofType), ((((func A) B) Xf)->(forall (Xx:fofType), (((in Xx) A)->((in ((((ap A) B) Xf) Xx)) B)))))) of role definition named app % A new definition: (((eq Prop) app) (forall (A:fofType) (B:fofType) (Xf:fofType), ((((func A) B) Xf)->(forall (Xx:fofType), (((in Xx) A)->((in ((((ap A) B) Xf) Xx)) B)))))) % Defined: app:=(forall (A:fofType) (B:fofType) (Xf:fofType), ((((func A) B) Xf)->(forall (Xx:fofType), (((in Xx) A)->((in ((((ap A) B) Xf) Xx)) B))))) % FOF formula (<kernel.Constant object at 0x27b8320>, <kernel.Sort object at 0x2874878>) of role type named ex1E2_type % Using role type % Declaring ex1E2:Prop % FOF formula (((eq Prop) ex1E2) (forall (A:fofType) (Xphi:(fofType->Prop)), (((ex1 A) (fun (Xx:fofType)=> (Xphi Xx)))->(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) A)->((Xphi Xx)->((Xphi Xy)->(((eq fofType) Xx) Xy)))))))))) of role definition named ex1E2 % A new definition: (((eq Prop) ex1E2) (forall (A:fofType) (Xphi:(fofType->Prop)), (((ex1 A) (fun (Xx:fofType)=> (Xphi Xx)))->(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) A)->((Xphi Xx)->((Xphi Xy)->(((eq fofType) Xx) Xy)))))))))) % Defined: ex1E2:=(forall (A:fofType) (Xphi:(fofType->Prop)), (((ex1 A) (fun (Xx:fofType)=> (Xphi Xx)))->(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) A)->((Xphi Xx)->((Xphi Xy)->(((eq fofType) Xx) Xy))))))))) % FOF formula (<kernel.Constant object at 0x27b8b48>, <kernel.Sort object at 0x2874878>) of role type named funcGraphProp1_type % Using role type % Declaring funcGraphProp1:Prop % FOF formula (((eq Prop) funcGraphProp1) (forall (A:fofType) (B:fofType) (Xf:fofType), ((((func A) B) Xf)->(forall (Xx:fofType), (((in Xx) A)->((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf)))))) of role definition named funcGraphProp1 % A new definition: (((eq Prop) funcGraphProp1) (forall (A:fofType) (B:fofType) (Xf:fofType), ((((func A) B) Xf)->(forall (Xx:fofType), (((in Xx) A)->((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf)))))) % Defined: funcGraphProp1:=(forall (A:fofType) (B:fofType) (Xf:fofType), ((((func A) B) Xf)->(forall (Xx:fofType), (((in Xx) A)->((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf))))) % FOF formula (app->(ex1E2->(funcGraphProp1->(forall (A:fofType) (B:fofType) (Xf:fofType), ((((func A) B) Xf)->(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) Xf)->(((eq fofType) ((((ap A) B) Xf) Xx)) Xy))))))))))) of role conjecture named funcGraphProp2 % Conjecture to prove = (app->(ex1E2->(funcGraphProp1->(forall (A:fofType) (B:fofType) (Xf:fofType), ((((func A) B) Xf)->(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) Xf)->(((eq fofType) ((((ap A) B) Xf) Xx)) Xy))))))))))):Prop % We need to prove ['(app->(ex1E2->(funcGraphProp1->(forall (A:fofType) (B:fofType) (Xf:fofType), ((((func A) B) Xf)->(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) Xf)->(((eq fofType) ((((ap A) B) Xf) Xx)) Xy)))))))))))'] % Parameter fofType:Type. % Parameter in:(fofType->(fofType->Prop)). % Parameter emptyset:fofType. % Parameter setadjoin:(fofType->(fofType->fofType)). % Parameter dsetconstr:(fofType->((fofType->Prop)->fofType)). % Parameter subset:(fofType->(fofType->Prop)). % Parameter kpair:(fofType->(fofType->fofType)). % Parameter cartprod:(fofType->(fofType->fofType)). % Definition singleton:=(fun (A:fofType)=> ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (((eq fofType) A) ((setadjoin Xx) emptyset)))))):(fofType->Prop). % Definition ex1:=(fun (A:fofType) (Xphi:(fofType->Prop))=> (singleton ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))):(fofType->((fofType->Prop)->Prop)). % Definition breln:=(fun (A:fofType) (B:fofType) (C:fofType)=> ((subset C) ((cartprod A) B))):(fofType->(fofType->(fofType->Prop))). % Definition func:=(fun (A:fofType) (B:fofType) (R:fofType)=> ((and (((breln A) B) R)) (forall (Xx:fofType), (((in Xx) A)->((ex1 B) (fun (Xy:fofType)=> ((in ((kpair Xx) Xy)) R))))))):(fofType->(fofType->(fofType->Prop))). % Parameter ap:(fofType->(fofType->(fofType->(fofType->fofType)))). % Definition app:=(forall (A:fofType) (B:fofType) (Xf:fofType), ((((func A) B) Xf)->(forall (Xx:fofType), (((in Xx) A)->((in ((((ap A) B) Xf) Xx)) B))))):Prop. % Definition ex1E2:=(forall (A:fofType) (Xphi:(fofType->Prop)), (((ex1 A) (fun (Xx:fofType)=> (Xphi Xx)))->(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) A)->((Xphi Xx)->((Xphi Xy)->(((eq fofType) Xx) Xy))))))))):Prop. % Definition funcGraphProp1:=(forall (A:fofType) (B:fofType) (Xf:fofType), ((((func A) B) Xf)->(forall (Xx:fofType), (((in Xx) A)->((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf))))):Prop. % Trying to prove (app->(ex1E2->(funcGraphProp1->(forall (A:fofType) (B:fofType) (Xf:fofType), ((((func A) B) Xf)->(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) Xf)->(((eq fofType) ((((ap A) B) Xf) Xx)) Xy))))))))))) % Found x60:(P ((((ap A) B) Xf) Xx)) % Found (fun (x60:(P ((((ap A) B) Xf) Xx)))=> x60) as proof of (P ((((ap A) B) Xf) Xx)) % Found (fun (x60:(P ((((ap A) B) Xf) Xx)))=> x60) as proof of (P0 ((((ap A) B) Xf) Xx)) % Found eq_ref00:=(eq_ref0 ((((ap A) B) Xf) Xx)):(((eq fofType) ((((ap A) B) Xf) Xx)) ((((ap A) B) Xf) Xx)) % Found (eq_ref0 ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found ((eq_ref fofType) ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found ((eq_ref fofType) ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found ((eq_ref fofType) ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) Xy) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xy) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xy) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xy) % Found x80:(P ((((ap A) B) Xf) Xx)) % Found (fun (x80:(P ((((ap A) B) Xf) Xx)))=> x80) as proof of (P ((((ap A) B) Xf) Xx)) % Found (fun (x80:(P ((((ap A) B) Xf) Xx)))=> x80) as proof of (P0 ((((ap A) B) Xf) Xx)) % Found eq_ref00:=(eq_ref0 ((((ap A) B) Xf) Xx)):(((eq fofType) ((((ap A) B) Xf) Xx)) ((((ap A) B) Xf) Xx)) % Found (eq_ref0 ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found ((eq_ref fofType) ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found ((eq_ref fofType) ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found ((eq_ref fofType) ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) Xy) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xy) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xy) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xy) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) ((((ap A) B) Xf) Xx)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((((ap A) B) Xf) Xx)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((((ap A) B) Xf) Xx)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((((ap A) B) Xf) Xx)) % Found eq_ref00:=(eq_ref0 Xy):(((eq fofType) Xy) Xy) % Found (eq_ref0 Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found x4:((in Xy) B) % Instantiate: A0:=B:fofType % Found x4 as proof of ((in Xy) A0) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found eq_ref00:=(eq_ref0 Xy):(((eq fofType) Xy) Xy) % Found (eq_ref0 Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) ((((ap A) B) Xf) Xx)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((((ap A) B) Xf) Xx)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((((ap A) B) Xf) Xx)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((((ap A) B) Xf) Xx)) % Found x6:(P ((((ap A) B) Xf) Xx)) % Instantiate: b:=((((ap A) B) Xf) Xx):fofType % Found x6 as proof of (P0 b) % Found eq_ref00:=(eq_ref0 Xy):(((eq fofType) Xy) Xy) % Found (eq_ref0 Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) ((((ap A) B) Xf) Xx)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((((ap A) B) Xf) Xx)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((((ap A) B) Xf) Xx)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((((ap A) B) Xf) Xx)) % Found eq_ref00:=(eq_ref0 Xy):(((eq fofType) Xy) Xy) % Found (eq_ref0 Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found eq_ref00:=(eq_ref0 ((((ap A) B) Xf) Xx)):(((eq fofType) ((((ap A) B) Xf) Xx)) ((((ap A) B) Xf) Xx)) % Found (eq_ref0 ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found ((eq_ref fofType) ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found ((eq_ref fofType) ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found ((eq_ref fofType) ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) Xy) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xy) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xy) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xy) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found eq_ref00:=(eq_ref0 Xy):(((eq fofType) Xy) Xy) % Found (eq_ref0 Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found x6:(P0 b) % Instantiate: b:=((((ap A) B) Xf) Xx):fofType % Found (fun (x6:(P0 b))=> x6) as proof of (P0 ((((ap A) B) Xf) Xx)) % Found (fun (P0:(fofType->Prop)) (x6:(P0 b))=> x6) as proof of ((P0 b)->(P0 ((((ap A) B) Xf) Xx))) % Found (fun (P0:(fofType->Prop)) (x6:(P0 b))=> x6) as proof of (P b) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x6:(P Xy) % Instantiate: b:=Xy:fofType % Found x6 as proof of (P0 b) % Found eq_ref00:=(eq_ref0 ((((ap A) B) Xf) Xx)):(((eq fofType) ((((ap A) B) Xf) Xx)) ((((ap A) B) Xf) Xx)) % Found (eq_ref0 ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found ((eq_ref fofType) ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found ((eq_ref fofType) ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found ((eq_ref fofType) ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found x600000:=(x60000 x3):((in ((((ap A) B) Xf) Xx)) B) % Found (x60000 x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found ((x6000 Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found (((x600 x2) Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found ((((x60 Xf) x2) Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found (((((x6 B) Xf) x2) Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found ((((((x A) B) Xf) x2) Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found ((((((x A) B) Xf) x2) Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found x8:(P ((((ap A) B) Xf) Xx)) % Instantiate: b:=((((ap A) B) Xf) Xx):fofType % Found x8 as proof of (P0 b) % Found eq_ref00:=(eq_ref0 Xy):(((eq fofType) Xy) Xy) % Found (eq_ref0 Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found x60:(P ((((ap A) B) Xf) Xx)) % Found (fun (x60:(P ((((ap A) B) Xf) Xx)))=> x60) as proof of (P ((((ap A) B) Xf) Xx)) % Found (fun (x60:(P ((((ap A) B) Xf) Xx)))=> x60) as proof of (P0 ((((ap A) B) Xf) Xx)) % Found eq_ref00:=(eq_ref0 ((((ap A) B) Xf) Xx)):(((eq fofType) ((((ap A) B) Xf) Xx)) ((((ap A) B) Xf) Xx)) % Found (eq_ref0 ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found ((eq_ref fofType) ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found ((eq_ref fofType) ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found ((eq_ref fofType) ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) Xy) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xy) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xy) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xy) % Found x600000:=(x60000 x3):((in ((((ap A) B) Xf) Xx)) B) % Found (x60000 x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found ((x6000 Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found (((x600 x2) Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found ((((x60 Xf) x2) Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found (((((x6 B) Xf) x2) Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found ((((((x A) B) Xf) x2) Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found ((((((x A) B) Xf) x2) Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found x700:=(x70 x3):((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx) Xy0)) Xf))) % Found (x70 x3) as proof of ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf))) % Found ((x7 Xx) x3) as proof of ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf))) % Found ((x7 Xx) x3) as proof of ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf))) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x700:=(x70 x3):((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx) Xy0)) Xf))) % Found (x70 x3) as proof of ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf))) % Found ((x7 Xx) x3) as proof of ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf))) % Found ((x7 Xx) x3) as proof of ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf))) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) ((((ap A) B) Xf) Xx)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((((ap A) B) Xf) Xx)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((((ap A) B) Xf) Xx)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((((ap A) B) Xf) Xx)) % Found eq_ref00:=(eq_ref0 Xy):(((eq fofType) Xy) Xy) % Found (eq_ref0 Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) ((((ap A) B) Xf) Xx)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((((ap A) B) Xf) Xx)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((((ap A) B) Xf) Xx)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((((ap A) B) Xf) Xx)) % Found eq_ref00:=(eq_ref0 Xy):(((eq fofType) Xy) Xy) % Found (eq_ref0 Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found eq_ref00:=(eq_ref0 Xy):(((eq fofType) Xy) Xy) % Found (eq_ref0 Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) ((((ap A) B) Xf) Xx)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((((ap A) B) Xf) Xx)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((((ap A) B) Xf) Xx)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((((ap A) B) Xf) Xx)) % Found eq_ref00:=(eq_ref0 ((((ap A) B) Xf) Xx)):(((eq fofType) ((((ap A) B) Xf) Xx)) ((((ap A) B) Xf) Xx)) % Found (eq_ref0 ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found ((eq_ref fofType) ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found ((eq_ref fofType) ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found ((eq_ref fofType) ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) Xy) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xy) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xy) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xy) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x60:(P b) % Found (fun (x60:(P b))=> x60) as proof of (P b) % Found (fun (x60:(P b))=> x60) as proof of (P0 b) % Found eq_ref00:=(eq_ref0 Xy):(((eq fofType) Xy) Xy) % Found (eq_ref0 Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found ((eq_ref fofType) Xy) as proof of (((eq fofType) Xy) b) % Found x8:(P0 b) % Instantiate: b:=((((ap A) B) Xf) Xx):fofType % Found (fun (x8:(P0 b))=> x8) as proof of (P0 ((((ap A) B) Xf) Xx)) % Found (fun (P0:(fofType->Prop)) (x8:(P0 b))=> x8) as proof of ((P0 b)->(P0 ((((ap A) B) Xf) Xx))) % Found (fun (P0:(fofType->Prop)) (x8:(P0 b))=> x8) as proof of (P b) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x4:((in Xy) B) % Found x4 as proof of ((in Xy) B) % Found x8:(P Xy) % Instantiate: b:=Xy:fofType % Found x8 as proof of (P0 b) % Found eq_ref00:=(eq_ref0 ((((ap A) B) Xf) Xx)):(((eq fofType) ((((ap A) B) Xf) Xx)) ((((ap A) B) Xf) Xx)) % Found (eq_ref0 ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found ((eq_ref fofType) ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found ((eq_ref fofType) ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found ((eq_ref fofType) ((((ap A) B) Xf) Xx)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) b) % Found x600000:=(x60000 x3):((in ((((ap A) B) Xf) Xx)) B) % Found (x60000 x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found ((x6000 Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found (((x600 x2) Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found ((((x60 Xf) x2) Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found (((((x6 B) Xf) x2) Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found ((((((x A) B) Xf) x2) Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found ((((((x A) B) Xf) x2) Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found x600000:=(x60000 x3):((in ((((ap A) B) Xf) Xx)) B) % Found (x60000 x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found ((x6000 Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found (((x600 x2) Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found ((((x60 Xf) x2) Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found (((((x6 B) Xf) x2) Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found ((((((x A) B) Xf) x2) Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found ((((((x A) B) Xf) x2) Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found x1000000:=(x100000 x3):((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf) % Found (x100000 x3) as proof of ((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf) % Found ((x10000 Xx) x3) as proof of ((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf) % Found (((x1000 x2) Xx) x3) as proof of ((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf) % Found ((((x100 Xf) x2) Xx) x3) as proof of ((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf) % Found (((((x10 B) Xf) x2) Xx) x3) as proof of ((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf) % Found ((((((x1 A) B) Xf) x2) Xx) x3) as proof of ((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf) % Found ((((((x1 A) B) Xf) x2) Xx) x3) as proof of ((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf) % Found x600000:=(x60000 x3):((in ((((ap A) B) Xf) Xx)) B) % Found (x60000 x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found ((x6000 Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found (((x600 x2) Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found ((((x60 Xf) x2) Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found (((((x6 B) Xf) x2) Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found ((((((x A) B) Xf) x2) Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found ((((((x A) B) Xf) x2) Xx) x3) as proof of ((in ((((ap A) B) Xf) Xx)) B) % Found x700:=(x70 x3):((ex1 B) (fun (Xy:fofType)=> ((in ((kpair Xx) Xy)) Xf))) % Found (x70 x3) as proof of ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf))) % Found ((x7 Xx) x3) as proof of ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf))) % Found (fun (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy:fofType)=> ((in ((kpair Xx0) Xy)) Xf))))))=> ((x7 Xx) x3)) as proof of ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf))) % Found (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy:fofType)=> ((in ((kpair Xx0) Xy)) Xf))))))=> ((x7 Xx) x3)) as proof of ((forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy:fofType)=> ((in ((kpair Xx0) Xy)) Xf)))))->((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) % Found (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy:fofType)=> ((in ((kpair Xx0) Xy)) Xf))))))=> ((x7 Xx) x3)) as proof of ((((breln A) B) Xf)->((forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy:fofType)=> ((in ((kpair Xx0) Xy)) Xf)))))->((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf))))) % Found (and_rect00 (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy:fofType)=> ((in ((kpair Xx0) Xy)) Xf))))))=> ((x7 Xx) x3))) as proof of ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf))) % Found ((and_rect0 ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy:fofType)=> ((in ((kpair Xx0) Xy)) Xf))))))=> ((x7 Xx) x3))) as proof of ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf))) % Found (((fun (P:Type) (x6:((((breln A) B) Xf)->((forall (Xx:fofType), (((in Xx) A)->((ex1 B) (fun (Xy:fofType)=> ((in ((kpair Xx) Xy)) Xf)))))->P)))=> (((((and_rect (((breln A) B) Xf)) (forall (Xx:fofType), (((in Xx) A)->((ex1 B) (fun (Xy:fofType)=> ((in ((kpair Xx) Xy)) Xf)))))) P) x6) x2)) ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy:fofType)=> ((in ((kpair Xx0) Xy)) Xf))))))=> ((x7 Xx) x3))) as proof of ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf))) % Found (((fun (P:Type) (x6:((((breln A) B) Xf)->((forall (Xx:fofType), (((in Xx) A)->((ex1 B) (fun (Xy:fofType)=> ((in ((kpair Xx) Xy)) Xf)))))->P)))=> (((((and_rect (((breln A) B) Xf)) (forall (Xx:fofType), (((in Xx) A)->((ex1 B) (fun (Xy:fofType)=> ((in ((kpair Xx) Xy)) Xf)))))) P) x6) x2)) ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy:fofType)=> ((in ((kpair Xx0) Xy)) Xf))))))=> ((x7 Xx) x3))) as proof of ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf))) % Found ((((x000000 (((fun (P:Type) (x6:((((breln A) B) Xf)->((forall (Xx:fofType), (((in Xx) A)->((ex1 B) (fun (Xy:fofType)=> ((in ((kpair Xx) Xy)) Xf)))))->P)))=> (((((and_rect (((breln A) B) Xf)) (forall (Xx:fofType), (((in Xx) A)->((ex1 B) (fun (Xy:fofType)=> ((in ((kpair Xx) Xy)) Xf)))))) P) x6) x2)) ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy:fofType)=> ((in ((kpair Xx0) Xy)) Xf))))))=> ((x7 Xx) x3)))) ((((((x A) B) Xf) x2) Xx) x3)) x4) ((((((x1 A) B) Xf) x2) Xx) x3)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) Xy) % Found (((((x00000 B) (((fun (P:Type) (x6:((((breln A) B) Xf)->((forall (Xx:fofType), (((in Xx) A)->((ex1 B) (fun (Xy:fofType)=> ((in ((kpair Xx) Xy)) Xf)))))->P)))=> (((((and_rect (((breln A) B) Xf)) (forall (Xx:fofType), (((in Xx) A)->((ex1 B) (fun (Xy:fofType)=> ((in ((kpair Xx) Xy)) Xf)))))) P) x6) x2)) ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy:fofType)=> ((in ((kpair Xx0) Xy)) Xf))))))=> ((x7 Xx) x3)))) ((((((x A) B) Xf) x2) Xx) x3)) x4) ((((((x1 A) B) Xf) x2) Xx) x3)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) Xy) % Found ((((((fun (A0:fofType) (x6:((ex1 A0) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (x7:((in ((((ap A) B) Xf) Xx)) A0)) (x8:((in Xy) A0)) (x9:((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf))=> ((((((x0000 A0) x6) x7) x8) x9) x5)) B) (((fun (P:Type) (x6:((((breln A) B) Xf)->((forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))->P)))=> (((((and_rect (((breln A) B) Xf)) (forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))) P) x6) x2)) ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf))))))=> ((x7 Xx) x3)))) ((((((x A) B) Xf) x2) Xx) x3)) x4) ((((((x1 A) B) Xf) x2) Xx) x3)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) Xy) % Found ((((((fun (A0:fofType) (x6:((ex1 A0) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (x7:((in ((((ap A) B) Xf) Xx)) A0)) (x8:((in Xy) A0)) (x9:((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf))=> (((((((fun (A0:fofType)=> ((x000 A0) (fun (x10:fofType)=> ((in ((kpair Xx) x10)) Xf)))) A0) x6) x7) x8) x9) x5)) B) (((fun (P:Type) (x6:((((breln A) B) Xf)->((forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))->P)))=> (((((and_rect (((breln A) B) Xf)) (forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))) P) x6) x2)) ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf))))))=> ((x7 Xx) x3)))) ((((((x A) B) Xf) x2) Xx) x3)) x4) ((((((x1 A) B) Xf) x2) Xx) x3)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) Xy) % Found ((((((fun (A0:fofType) (x6:((ex1 A0) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (x7:((in ((((ap A) B) Xf) Xx)) A0)) (x8:((in Xy) A0)) (x9:((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf))=> (((((((fun (A0:fofType)=> (((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx:fofType)=> (Xphi Xx)))) (x7:((in ((((ap A) B) Xf) Xx)) A0))=> (((((x00 A0) Xphi) x6) x7) Xy)) A0) (fun (x10:fofType)=> ((in ((kpair Xx) x10)) Xf)))) A0) x6) x7) x8) x9) x5)) B) (((fun (P:Type) (x6:((((breln A) B) Xf)->((forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))->P)))=> (((((and_rect (((breln A) B) Xf)) (forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))) P) x6) x2)) ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf))))))=> ((x7 Xx) x3)))) ((((((x A) B) Xf) x2) Xx) x3)) x4) ((((((x1 A) B) Xf) x2) Xx) x3)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) Xy) % Found ((((((fun (A0:fofType) (x6:((ex1 A0) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (x7:((in ((((ap A) B) Xf) Xx)) A0)) (x8:((in Xy) A0)) (x9:((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf))=> (((((((fun (A0:fofType)=> (((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx0:fofType)=> (Xphi Xx0)))) (x7:((in ((((ap A) B) Xf) Xx)) A0))=> ((((((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx:fofType)=> (Xphi Xx))))=> ((((x0 A0) Xphi) x6) ((((ap A) B) Xf) Xx))) A0) Xphi) x6) x7) Xy)) A0) (fun (x10:fofType)=> ((in ((kpair Xx) x10)) Xf)))) A0) x6) x7) x8) x9) x5)) B) (((fun (P:Type) (x6:((((breln A) B) Xf)->((forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))->P)))=> (((((and_rect (((breln A) B) Xf)) (forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))) P) x6) x2)) ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf))))))=> ((x7 Xx) x3)))) ((((((x A) B) Xf) x2) Xx) x3)) x4) ((((((x1 A) B) Xf) x2) Xx) x3)) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) Xy) % Found (fun (x5:((in ((kpair Xx) Xy)) Xf))=> ((((((fun (A0:fofType) (x6:((ex1 A0) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (x7:((in ((((ap A) B) Xf) Xx)) A0)) (x8:((in Xy) A0)) (x9:((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf))=> (((((((fun (A0:fofType)=> (((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx0:fofType)=> (Xphi Xx0)))) (x7:((in ((((ap A) B) Xf) Xx)) A0))=> ((((((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx:fofType)=> (Xphi Xx))))=> ((((x0 A0) Xphi) x6) ((((ap A) B) Xf) Xx))) A0) Xphi) x6) x7) Xy)) A0) (fun (x10:fofType)=> ((in ((kpair Xx) x10)) Xf)))) A0) x6) x7) x8) x9) x5)) B) (((fun (P:Type) (x6:((((breln A) B) Xf)->((forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))->P)))=> (((((and_rect (((breln A) B) Xf)) (forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))) P) x6) x2)) ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf))))))=> ((x7 Xx) x3)))) ((((((x A) B) Xf) x2) Xx) x3)) x4) ((((((x1 A) B) Xf) x2) Xx) x3))) as proof of (((eq fofType) ((((ap A) B) Xf) Xx)) Xy) % Found (fun (x4:((in Xy) B)) (x5:((in ((kpair Xx) Xy)) Xf))=> ((((((fun (A0:fofType) (x6:((ex1 A0) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (x7:((in ((((ap A) B) Xf) Xx)) A0)) (x8:((in Xy) A0)) (x9:((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf))=> (((((((fun (A0:fofType)=> (((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx0:fofType)=> (Xphi Xx0)))) (x7:((in ((((ap A) B) Xf) Xx)) A0))=> ((((((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx:fofType)=> (Xphi Xx))))=> ((((x0 A0) Xphi) x6) ((((ap A) B) Xf) Xx))) A0) Xphi) x6) x7) Xy)) A0) (fun (x10:fofType)=> ((in ((kpair Xx) x10)) Xf)))) A0) x6) x7) x8) x9) x5)) B) (((fun (P:Type) (x6:((((breln A) B) Xf)->((forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))->P)))=> (((((and_rect (((breln A) B) Xf)) (forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))) P) x6) x2)) ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf))))))=> ((x7 Xx) x3)))) ((((((x A) B) Xf) x2) Xx) x3)) x4) ((((((x1 A) B) Xf) x2) Xx) x3))) as proof of (((in ((kpair Xx) Xy)) Xf)->(((eq fofType) ((((ap A) B) Xf) Xx)) Xy)) % Found (fun (Xy:fofType) (x4:((in Xy) B)) (x5:((in ((kpair Xx) Xy)) Xf))=> ((((((fun (A0:fofType) (x6:((ex1 A0) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (x7:((in ((((ap A) B) Xf) Xx)) A0)) (x8:((in Xy) A0)) (x9:((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf))=> (((((((fun (A0:fofType)=> (((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx0:fofType)=> (Xphi Xx0)))) (x7:((in ((((ap A) B) Xf) Xx)) A0))=> ((((((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx:fofType)=> (Xphi Xx))))=> ((((x0 A0) Xphi) x6) ((((ap A) B) Xf) Xx))) A0) Xphi) x6) x7) Xy)) A0) (fun (x10:fofType)=> ((in ((kpair Xx) x10)) Xf)))) A0) x6) x7) x8) x9) x5)) B) (((fun (P:Type) (x6:((((breln A) B) Xf)->((forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))->P)))=> (((((and_rect (((breln A) B) Xf)) (forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))) P) x6) x2)) ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf))))))=> ((x7 Xx) x3)))) ((((((x A) B) Xf) x2) Xx) x3)) x4) ((((((x1 A) B) Xf) x2) Xx) x3))) as proof of (((in Xy) B)->(((in ((kpair Xx) Xy)) Xf)->(((eq fofType) ((((ap A) B) Xf) Xx)) Xy))) % Found (fun (x3:((in Xx) A)) (Xy:fofType) (x4:((in Xy) B)) (x5:((in ((kpair Xx) Xy)) Xf))=> ((((((fun (A0:fofType) (x6:((ex1 A0) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (x7:((in ((((ap A) B) Xf) Xx)) A0)) (x8:((in Xy) A0)) (x9:((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf))=> (((((((fun (A0:fofType)=> (((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx0:fofType)=> (Xphi Xx0)))) (x7:((in ((((ap A) B) Xf) Xx)) A0))=> ((((((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx:fofType)=> (Xphi Xx))))=> ((((x0 A0) Xphi) x6) ((((ap A) B) Xf) Xx))) A0) Xphi) x6) x7) Xy)) A0) (fun (x10:fofType)=> ((in ((kpair Xx) x10)) Xf)))) A0) x6) x7) x8) x9) x5)) B) (((fun (P:Type) (x6:((((breln A) B) Xf)->((forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))->P)))=> (((((and_rect (((breln A) B) Xf)) (forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))) P) x6) x2)) ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf))))))=> ((x7 Xx) x3)))) ((((((x A) B) Xf) x2) Xx) x3)) x4) ((((((x1 A) B) Xf) x2) Xx) x3))) as proof of (forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) Xf)->(((eq fofType) ((((ap A) B) Xf) Xx)) Xy)))) % Found (fun (Xx:fofType) (x3:((in Xx) A)) (Xy:fofType) (x4:((in Xy) B)) (x5:((in ((kpair Xx) Xy)) Xf))=> ((((((fun (A0:fofType) (x6:((ex1 A0) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (x7:((in ((((ap A) B) Xf) Xx)) A0)) (x8:((in Xy) A0)) (x9:((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf))=> (((((((fun (A0:fofType)=> (((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx0:fofType)=> (Xphi Xx0)))) (x7:((in ((((ap A) B) Xf) Xx)) A0))=> ((((((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx:fofType)=> (Xphi Xx))))=> ((((x0 A0) Xphi) x6) ((((ap A) B) Xf) Xx))) A0) Xphi) x6) x7) Xy)) A0) (fun (x10:fofType)=> ((in ((kpair Xx) x10)) Xf)))) A0) x6) x7) x8) x9) x5)) B) (((fun (P:Type) (x6:((((breln A) B) Xf)->((forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))->P)))=> (((((and_rect (((breln A) B) Xf)) (forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))) P) x6) x2)) ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf))))))=> ((x7 Xx) x3)))) ((((((x A) B) Xf) x2) Xx) x3)) x4) ((((((x1 A) B) Xf) x2) Xx) x3))) as proof of (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) Xf)->(((eq fofType) ((((ap A) B) Xf) Xx)) Xy))))) % Found (fun (x2:(((func A) B) Xf)) (Xx:fofType) (x3:((in Xx) A)) (Xy:fofType) (x4:((in Xy) B)) (x5:((in ((kpair Xx) Xy)) Xf))=> ((((((fun (A0:fofType) (x6:((ex1 A0) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (x7:((in ((((ap A) B) Xf) Xx)) A0)) (x8:((in Xy) A0)) (x9:((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf))=> (((((((fun (A0:fofType)=> (((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx0:fofType)=> (Xphi Xx0)))) (x7:((in ((((ap A) B) Xf) Xx)) A0))=> ((((((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx:fofType)=> (Xphi Xx))))=> ((((x0 A0) Xphi) x6) ((((ap A) B) Xf) Xx))) A0) Xphi) x6) x7) Xy)) A0) (fun (x10:fofType)=> ((in ((kpair Xx) x10)) Xf)))) A0) x6) x7) x8) x9) x5)) B) (((fun (P:Type) (x6:((((breln A) B) Xf)->((forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))->P)))=> (((((and_rect (((breln A) B) Xf)) (forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))) P) x6) x2)) ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf))))))=> ((x7 Xx) x3)))) ((((((x A) B) Xf) x2) Xx) x3)) x4) ((((((x1 A) B) Xf) x2) Xx) x3))) as proof of (forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) Xf)->(((eq fofType) ((((ap A) B) Xf) Xx)) Xy)))))) % Found (fun (Xf:fofType) (x2:(((func A) B) Xf)) (Xx:fofType) (x3:((in Xx) A)) (Xy:fofType) (x4:((in Xy) B)) (x5:((in ((kpair Xx) Xy)) Xf))=> ((((((fun (A0:fofType) (x6:((ex1 A0) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (x7:((in ((((ap A) B) Xf) Xx)) A0)) (x8:((in Xy) A0)) (x9:((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf))=> (((((((fun (A0:fofType)=> (((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx0:fofType)=> (Xphi Xx0)))) (x7:((in ((((ap A) B) Xf) Xx)) A0))=> ((((((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx:fofType)=> (Xphi Xx))))=> ((((x0 A0) Xphi) x6) ((((ap A) B) Xf) Xx))) A0) Xphi) x6) x7) Xy)) A0) (fun (x10:fofType)=> ((in ((kpair Xx) x10)) Xf)))) A0) x6) x7) x8) x9) x5)) B) (((fun (P:Type) (x6:((((breln A) B) Xf)->((forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))->P)))=> (((((and_rect (((breln A) B) Xf)) (forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))) P) x6) x2)) ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf))))))=> ((x7 Xx) x3)))) ((((((x A) B) Xf) x2) Xx) x3)) x4) ((((((x1 A) B) Xf) x2) Xx) x3))) as proof of ((((func A) B) Xf)->(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) Xf)->(((eq fofType) ((((ap A) B) Xf) Xx)) Xy))))))) % Found (fun (B:fofType) (Xf:fofType) (x2:(((func A) B) Xf)) (Xx:fofType) (x3:((in Xx) A)) (Xy:fofType) (x4:((in Xy) B)) (x5:((in ((kpair Xx) Xy)) Xf))=> ((((((fun (A0:fofType) (x6:((ex1 A0) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (x7:((in ((((ap A) B) Xf) Xx)) A0)) (x8:((in Xy) A0)) (x9:((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf))=> (((((((fun (A0:fofType)=> (((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx0:fofType)=> (Xphi Xx0)))) (x7:((in ((((ap A) B) Xf) Xx)) A0))=> ((((((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx:fofType)=> (Xphi Xx))))=> ((((x0 A0) Xphi) x6) ((((ap A) B) Xf) Xx))) A0) Xphi) x6) x7) Xy)) A0) (fun (x10:fofType)=> ((in ((kpair Xx) x10)) Xf)))) A0) x6) x7) x8) x9) x5)) B) (((fun (P:Type) (x6:((((breln A) B) Xf)->((forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))->P)))=> (((((and_rect (((breln A) B) Xf)) (forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))) P) x6) x2)) ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf))))))=> ((x7 Xx) x3)))) ((((((x A) B) Xf) x2) Xx) x3)) x4) ((((((x1 A) B) Xf) x2) Xx) x3))) as proof of (forall (Xf:fofType), ((((func A) B) Xf)->(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) Xf)->(((eq fofType) ((((ap A) B) Xf) Xx)) Xy)))))))) % Found (fun (A:fofType) (B:fofType) (Xf:fofType) (x2:(((func A) B) Xf)) (Xx:fofType) (x3:((in Xx) A)) (Xy:fofType) (x4:((in Xy) B)) (x5:((in ((kpair Xx) Xy)) Xf))=> ((((((fun (A0:fofType) (x6:((ex1 A0) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (x7:((in ((((ap A) B) Xf) Xx)) A0)) (x8:((in Xy) A0)) (x9:((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf))=> (((((((fun (A0:fofType)=> (((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx0:fofType)=> (Xphi Xx0)))) (x7:((in ((((ap A) B) Xf) Xx)) A0))=> ((((((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx:fofType)=> (Xphi Xx))))=> ((((x0 A0) Xphi) x6) ((((ap A) B) Xf) Xx))) A0) Xphi) x6) x7) Xy)) A0) (fun (x10:fofType)=> ((in ((kpair Xx) x10)) Xf)))) A0) x6) x7) x8) x9) x5)) B) (((fun (P:Type) (x6:((((breln A) B) Xf)->((forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))->P)))=> (((((and_rect (((breln A) B) Xf)) (forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))) P) x6) x2)) ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf))))))=> ((x7 Xx) x3)))) ((((((x A) B) Xf) x2) Xx) x3)) x4) ((((((x1 A) B) Xf) x2) Xx) x3))) as proof of (forall (B:fofType) (Xf:fofType), ((((func A) B) Xf)->(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) Xf)->(((eq fofType) ((((ap A) B) Xf) Xx)) Xy)))))))) % Found (fun (x1:funcGraphProp1) (A:fofType) (B:fofType) (Xf:fofType) (x2:(((func A) B) Xf)) (Xx:fofType) (x3:((in Xx) A)) (Xy:fofType) (x4:((in Xy) B)) (x5:((in ((kpair Xx) Xy)) Xf))=> ((((((fun (A0:fofType) (x6:((ex1 A0) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (x7:((in ((((ap A) B) Xf) Xx)) A0)) (x8:((in Xy) A0)) (x9:((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf))=> (((((((fun (A0:fofType)=> (((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx0:fofType)=> (Xphi Xx0)))) (x7:((in ((((ap A) B) Xf) Xx)) A0))=> ((((((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx:fofType)=> (Xphi Xx))))=> ((((x0 A0) Xphi) x6) ((((ap A) B) Xf) Xx))) A0) Xphi) x6) x7) Xy)) A0) (fun (x10:fofType)=> ((in ((kpair Xx) x10)) Xf)))) A0) x6) x7) x8) x9) x5)) B) (((fun (P:Type) (x6:((((breln A) B) Xf)->((forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))->P)))=> (((((and_rect (((breln A) B) Xf)) (forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))) P) x6) x2)) ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf))))))=> ((x7 Xx) x3)))) ((((((x A) B) Xf) x2) Xx) x3)) x4) ((((((x1 A) B) Xf) x2) Xx) x3))) as proof of (forall (A:fofType) (B:fofType) (Xf:fofType), ((((func A) B) Xf)->(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) Xf)->(((eq fofType) ((((ap A) B) Xf) Xx)) Xy)))))))) % Found (fun (x0:ex1E2) (x1:funcGraphProp1) (A:fofType) (B:fofType) (Xf:fofType) (x2:(((func A) B) Xf)) (Xx:fofType) (x3:((in Xx) A)) (Xy:fofType) (x4:((in Xy) B)) (x5:((in ((kpair Xx) Xy)) Xf))=> ((((((fun (A0:fofType) (x6:((ex1 A0) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (x7:((in ((((ap A) B) Xf) Xx)) A0)) (x8:((in Xy) A0)) (x9:((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf))=> (((((((fun (A0:fofType)=> (((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx0:fofType)=> (Xphi Xx0)))) (x7:((in ((((ap A) B) Xf) Xx)) A0))=> ((((((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx:fofType)=> (Xphi Xx))))=> ((((x0 A0) Xphi) x6) ((((ap A) B) Xf) Xx))) A0) Xphi) x6) x7) Xy)) A0) (fun (x10:fofType)=> ((in ((kpair Xx) x10)) Xf)))) A0) x6) x7) x8) x9) x5)) B) (((fun (P:Type) (x6:((((breln A) B) Xf)->((forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))->P)))=> (((((and_rect (((breln A) B) Xf)) (forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))) P) x6) x2)) ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf))))))=> ((x7 Xx) x3)))) ((((((x A) B) Xf) x2) Xx) x3)) x4) ((((((x1 A) B) Xf) x2) Xx) x3))) as proof of (funcGraphProp1->(forall (A:fofType) (B:fofType) (Xf:fofType), ((((func A) B) Xf)->(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) Xf)->(((eq fofType) ((((ap A) B) Xf) Xx)) Xy))))))))) % Found (fun (x:app) (x0:ex1E2) (x1:funcGraphProp1) (A:fofType) (B:fofType) (Xf:fofType) (x2:(((func A) B) Xf)) (Xx:fofType) (x3:((in Xx) A)) (Xy:fofType) (x4:((in Xy) B)) (x5:((in ((kpair Xx) Xy)) Xf))=> ((((((fun (A0:fofType) (x6:((ex1 A0) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (x7:((in ((((ap A) B) Xf) Xx)) A0)) (x8:((in Xy) A0)) (x9:((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf))=> (((((((fun (A0:fofType)=> (((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx0:fofType)=> (Xphi Xx0)))) (x7:((in ((((ap A) B) Xf) Xx)) A0))=> ((((((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx:fofType)=> (Xphi Xx))))=> ((((x0 A0) Xphi) x6) ((((ap A) B) Xf) Xx))) A0) Xphi) x6) x7) Xy)) A0) (fun (x10:fofType)=> ((in ((kpair Xx) x10)) Xf)))) A0) x6) x7) x8) x9) x5)) B) (((fun (P:Type) (x6:((((breln A) B) Xf)->((forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))->P)))=> (((((and_rect (((breln A) B) Xf)) (forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))) P) x6) x2)) ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf))))))=> ((x7 Xx) x3)))) ((((((x A) B) Xf) x2) Xx) x3)) x4) ((((((x1 A) B) Xf) x2) Xx) x3))) as proof of (ex1E2->(funcGraphProp1->(forall (A:fofType) (B:fofType) (Xf:fofType), ((((func A) B) Xf)->(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) Xf)->(((eq fofType) ((((ap A) B) Xf) Xx)) Xy)))))))))) % Found (fun (x:app) (x0:ex1E2) (x1:funcGraphProp1) (A:fofType) (B:fofType) (Xf:fofType) (x2:(((func A) B) Xf)) (Xx:fofType) (x3:((in Xx) A)) (Xy:fofType) (x4:((in Xy) B)) (x5:((in ((kpair Xx) Xy)) Xf))=> ((((((fun (A0:fofType) (x6:((ex1 A0) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (x7:((in ((((ap A) B) Xf) Xx)) A0)) (x8:((in Xy) A0)) (x9:((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf))=> (((((((fun (A0:fofType)=> (((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx0:fofType)=> (Xphi Xx0)))) (x7:((in ((((ap A) B) Xf) Xx)) A0))=> ((((((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx:fofType)=> (Xphi Xx))))=> ((((x0 A0) Xphi) x6) ((((ap A) B) Xf) Xx))) A0) Xphi) x6) x7) Xy)) A0) (fun (x10:fofType)=> ((in ((kpair Xx) x10)) Xf)))) A0) x6) x7) x8) x9) x5)) B) (((fun (P:Type) (x6:((((breln A) B) Xf)->((forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))->P)))=> (((((and_rect (((breln A) B) Xf)) (forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))) P) x6) x2)) ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf))))))=> ((x7 Xx) x3)))) ((((((x A) B) Xf) x2) Xx) x3)) x4) ((((((x1 A) B) Xf) x2) Xx) x3))) as proof of (app->(ex1E2->(funcGraphProp1->(forall (A:fofType) (B:fofType) (Xf:fofType), ((((func A) B) Xf)->(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) Xf)->(((eq fofType) ((((ap A) B) Xf) Xx)) Xy))))))))))) % Got proof (fun (x:app) (x0:ex1E2) (x1:funcGraphProp1) (A:fofType) (B:fofType) (Xf:fofType) (x2:(((func A) B) Xf)) (Xx:fofType) (x3:((in Xx) A)) (Xy:fofType) (x4:((in Xy) B)) (x5:((in ((kpair Xx) Xy)) Xf))=> ((((((fun (A0:fofType) (x6:((ex1 A0) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (x7:((in ((((ap A) B) Xf) Xx)) A0)) (x8:((in Xy) A0)) (x9:((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf))=> (((((((fun (A0:fofType)=> (((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx0:fofType)=> (Xphi Xx0)))) (x7:((in ((((ap A) B) Xf) Xx)) A0))=> ((((((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx:fofType)=> (Xphi Xx))))=> ((((x0 A0) Xphi) x6) ((((ap A) B) Xf) Xx))) A0) Xphi) x6) x7) Xy)) A0) (fun (x10:fofType)=> ((in ((kpair Xx) x10)) Xf)))) A0) x6) x7) x8) x9) x5)) B) (((fun (P:Type) (x6:((((breln A) B) Xf)->((forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))->P)))=> (((((and_rect (((breln A) B) Xf)) (forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))) P) x6) x2)) ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf))))))=> ((x7 Xx) x3)))) ((((((x A) B) Xf) x2) Xx) x3)) x4) ((((((x1 A) B) Xf) x2) Xx) x3))) % Time elapsed = 141.169153s % node=17416 cost=1242.000000 depth=27 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % (fun (x:app) (x0:ex1E2) (x1:funcGraphProp1) (A:fofType) (B:fofType) (Xf:fofType) (x2:(((func A) B) Xf)) (Xx:fofType) (x3:((in Xx) A)) (Xy:fofType) (x4:((in Xy) B)) (x5:((in ((kpair Xx) Xy)) Xf))=> ((((((fun (A0:fofType) (x6:((ex1 A0) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (x7:((in ((((ap A) B) Xf) Xx)) A0)) (x8:((in Xy) A0)) (x9:((in ((kpair Xx) ((((ap A) B) Xf) Xx))) Xf))=> (((((((fun (A0:fofType)=> (((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx0:fofType)=> (Xphi Xx0)))) (x7:((in ((((ap A) B) Xf) Xx)) A0))=> ((((((fun (A0:fofType) (Xphi:(fofType->Prop)) (x6:((ex1 A0) (fun (Xx:fofType)=> (Xphi Xx))))=> ((((x0 A0) Xphi) x6) ((((ap A) B) Xf) Xx))) A0) Xphi) x6) x7) Xy)) A0) (fun (x10:fofType)=> ((in ((kpair Xx) x10)) Xf)))) A0) x6) x7) x8) x9) x5)) B) (((fun (P:Type) (x6:((((breln A) B) Xf)->((forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))->P)))=> (((((and_rect (((breln A) B) Xf)) (forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf)))))) P) x6) x2)) ((ex1 B) (fun (Xx0:fofType)=> ((in ((kpair Xx) Xx0)) Xf)))) (fun (x6:(((breln A) B) Xf)) (x7:(forall (Xx0:fofType), (((in Xx0) A)->((ex1 B) (fun (Xy0:fofType)=> ((in ((kpair Xx0) Xy0)) Xf))))))=> ((x7 Xx) x3)))) ((((((x A) B) Xf) x2) Xx) x3)) x4) ((((((x1 A) B) Xf) x2) Xx) x3))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------