%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEU789^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 : n102.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:07 EDT 2014 % Result : Theorem 115.75s % Output : Proof 115.75s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SEU789^2 : TPTP v6.1.0. Released v3.7.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n102.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:28:56 CDT 2014 % % CPUTime : 115.75 % 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 0xc463b0>, <kernel.DependentProduct object at 0xc450e0>) of role type named in_type % Using role type % Declaring in:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0xc463b0>, <kernel.DependentProduct object at 0xc450e0>) of role type named subset_type % Using role type % Declaring subset:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0xc26128>, <kernel.Sort object at 0x931fc8>) of role type named setextsub_type % Using role type % Declaring setextsub:Prop % FOF formula (((eq Prop) setextsub) (forall (A:fofType) (B:fofType), (((subset A) B)->(((subset B) A)->(((eq fofType) A) B))))) of role definition named setextsub % A new definition: (((eq Prop) setextsub) (forall (A:fofType) (B:fofType), (((subset A) B)->(((subset B) A)->(((eq fofType) A) B))))) % Defined: setextsub:=(forall (A:fofType) (B:fofType), (((subset A) B)->(((subset B) A)->(((eq fofType) A) B)))) % FOF formula (<kernel.Constant object at 0xc45368>, <kernel.DependentProduct object at 0xc45c20>) of role type named kpair_type % Using role type % Declaring kpair:(fofType->(fofType->fofType)) % FOF formula (<kernel.Constant object at 0xc454d0>, <kernel.DependentProduct object at 0xc45bd8>) of role type named breln1_type % Using role type % Declaring breln1:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0xc457e8>, <kernel.Sort object at 0x931fc8>) of role type named subbreln1_type % Using role type % Declaring subbreln1:Prop % FOF formula (((eq Prop) subbreln1) (forall (A:fofType) (R:fofType), (((breln1 A) R)->(forall (S:fofType), (((breln1 A) S)->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) A)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))->((subset R) S))))))) of role definition named subbreln1 % A new definition: (((eq Prop) subbreln1) (forall (A:fofType) (R:fofType), (((breln1 A) R)->(forall (S:fofType), (((breln1 A) S)->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) A)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))->((subset R) S))))))) % Defined: subbreln1:=(forall (A:fofType) (R:fofType), (((breln1 A) R)->(forall (S:fofType), (((breln1 A) S)->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) A)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))->((subset R) S)))))) % FOF formula (<kernel.Constant object at 0x933830>, <kernel.DependentProduct object at 0xc45878>) of role type named breln1invset_type % Using role type % Declaring breln1invset:(fofType->(fofType->fofType)) % FOF formula (<kernel.Constant object at 0x933830>, <kernel.Sort object at 0x931fc8>) of role type named breln1invprop_type % Using role type % Declaring breln1invprop:Prop % FOF formula (((eq Prop) breln1invprop) (forall (A:fofType) (R:fofType), (((breln1 A) R)->((breln1 A) ((breln1invset A) R))))) of role definition named breln1invprop % A new definition: (((eq Prop) breln1invprop) (forall (A:fofType) (R:fofType), (((breln1 A) R)->((breln1 A) ((breln1invset A) R))))) % Defined: breln1invprop:=(forall (A:fofType) (R:fofType), (((breln1 A) R)->((breln1 A) ((breln1invset A) R)))) % FOF formula (<kernel.Constant object at 0xc45bd8>, <kernel.Sort object at 0x931fc8>) of role type named breln1invI_type % Using role type % Declaring breln1invI:Prop % FOF formula (((eq Prop) breln1invI) (forall (A:fofType) (R:fofType), (((breln1 A) R)->(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) A)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xy) Xx)) ((breln1invset A) R)))))))))) of role definition named breln1invI % A new definition: (((eq Prop) breln1invI) (forall (A:fofType) (R:fofType), (((breln1 A) R)->(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) A)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xy) Xx)) ((breln1invset A) R)))))))))) % Defined: breln1invI:=(forall (A:fofType) (R:fofType), (((breln1 A) R)->(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) A)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xy) Xx)) ((breln1invset A) R))))))))) % FOF formula (<kernel.Constant object at 0xc45368>, <kernel.Sort object at 0x931fc8>) of role type named breln1invE_type % Using role type % Declaring breln1invE:Prop % FOF formula (((eq Prop) breln1invE) (forall (A:fofType) (R:fofType), (((breln1 A) R)->(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) A)->(((in ((kpair Xy) Xx)) ((breln1invset A) R))->((in ((kpair Xx) Xy)) R))))))))) of role definition named breln1invE % A new definition: (((eq Prop) breln1invE) (forall (A:fofType) (R:fofType), (((breln1 A) R)->(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) A)->(((in ((kpair Xy) Xx)) ((breln1invset A) R))->((in ((kpair Xx) Xy)) R))))))))) % Defined: breln1invE:=(forall (A:fofType) (R:fofType), (((breln1 A) R)->(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) A)->(((in ((kpair Xy) Xx)) ((breln1invset A) R))->((in ((kpair Xx) Xy)) R)))))))) % FOF formula (setextsub->(subbreln1->(breln1invprop->(breln1invI->(breln1invE->(forall (A:fofType) (R:fofType), (((breln1 A) R)->(((eq fofType) R) ((breln1invset A) ((breln1invset A) R)))))))))) of role conjecture named woz2Ex % Conjecture to prove = (setextsub->(subbreln1->(breln1invprop->(breln1invI->(breln1invE->(forall (A:fofType) (R:fofType), (((breln1 A) R)->(((eq fofType) R) ((breln1invset A) ((breln1invset A) R)))))))))):Prop % Parameter fofType_DUMMY:fofType. % We need to prove ['(setextsub->(subbreln1->(breln1invprop->(breln1invI->(breln1invE->(forall (A:fofType) (R:fofType), (((breln1 A) R)->(((eq fofType) R) ((breln1invset A) ((breln1invset A) R))))))))))'] % Parameter fofType:Type. % Parameter in:(fofType->(fofType->Prop)). % Parameter subset:(fofType->(fofType->Prop)). % Definition setextsub:=(forall (A:fofType) (B:fofType), (((subset A) B)->(((subset B) A)->(((eq fofType) A) B)))):Prop. % Parameter kpair:(fofType->(fofType->fofType)). % Parameter breln1:(fofType->(fofType->Prop)). % Definition subbreln1:=(forall (A:fofType) (R:fofType), (((breln1 A) R)->(forall (S:fofType), (((breln1 A) S)->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) A)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))->((subset R) S)))))):Prop. % Parameter breln1invset:(fofType->(fofType->fofType)). % Definition breln1invprop:=(forall (A:fofType) (R:fofType), (((breln1 A) R)->((breln1 A) ((breln1invset A) R)))):Prop. % Definition breln1invI:=(forall (A:fofType) (R:fofType), (((breln1 A) R)->(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) A)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xy) Xx)) ((breln1invset A) R))))))))):Prop. % Definition breln1invE:=(forall (A:fofType) (R:fofType), (((breln1 A) R)->(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) A)->(((in ((kpair Xy) Xx)) ((breln1invset A) R))->((in ((kpair Xx) Xy)) R)))))))):Prop. % Trying to prove (setextsub->(subbreln1->(breln1invprop->(breln1invI->(breln1invE->(forall (A:fofType) (R:fofType), (((breln1 A) R)->(((eq fofType) R) ((breln1invset A) ((breln1invset A) R)))))))))) % Found x60:(P R) % Found (fun (x60:(P R))=> x60) as proof of (P R) % Found (fun (x60:(P R))=> x60) as proof of (P0 R) % Found x50:(P R) % Found (fun (x50:(P R))=> x50) as proof of (P R) % Found (fun (x50:(P R))=> x50) as proof of (P0 R) % Found eq_ref00:=(eq_ref0 R):(((eq fofType) R) R) % Found (eq_ref0 R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found eq_ref00:=(eq_ref0 ((breln1invset A) ((breln1invset A) R))):(((eq fofType) ((breln1invset A) ((breln1invset A) R))) ((breln1invset A) ((breln1invset A) R))) % Found (eq_ref0 ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x5:(P R) % Instantiate: b:=R:fofType % Found x5 as proof of (P0 b) % Found eq_ref00:=(eq_ref0 ((breln1invset A) ((breln1invset A) R))):(((eq fofType) ((breln1invset A) ((breln1invset A) R))) ((breln1invset A) ((breln1invset A) R))) % Found (eq_ref0 ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found x5:(P R) % Instantiate: A0:=R:fofType % Found x5 as proof of (P0 A0) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found eq_ref00:=(eq_ref0 R):(((eq fofType) R) R) % Found (eq_ref0 R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found eq_ref00:=(eq_ref0 ((breln1invset A) ((breln1invset A) R))):(((eq fofType) ((breln1invset A) ((breln1invset A) R))) ((breln1invset A) ((breln1invset A) R))) % Found (eq_ref0 ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found x5:(P0 b) % Instantiate: b:=R:fofType % Found (fun (x5:(P0 b))=> x5) as proof of (P0 R) % Found (fun (P0:(fofType->Prop)) (x5:(P0 b))=> x5) as proof of ((P0 b)->(P0 R)) % Found (fun (P0:(fofType->Prop)) (x5:(P0 b))=> x5) as proof of (P b) % Found x5:(P ((breln1invset A) ((breln1invset A) R))) % Instantiate: b:=((breln1invset A) ((breln1invset A) R)):fofType % Found x5 as proof of (P0 b) % Found eq_ref00:=(eq_ref0 R):(((eq fofType) R) R) % Found (eq_ref0 R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found eq_ref00:=(eq_ref0 R):(((eq fofType) R) R) % Found (eq_ref0 R) as proof of (((eq fofType) R) b0) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b0) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b0) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b0) % Found eq_ref00:=(eq_ref0 b0):(((eq fofType) b0) b0) % Found (eq_ref0 b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found x50:(P R) % Found (fun (x50:(P R))=> x50) as proof of (P R) % Found (fun (x50:(P R))=> x50) as proof of (P0 R) % Found eq_ref00:=(eq_ref0 R):(((eq fofType) R) R) % Found (eq_ref0 R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found x5:(P ((breln1invset A) ((breln1invset A) R))) % Instantiate: A0:=((breln1invset A) ((breln1invset A) R)):fofType % Found x5 as proof of (P0 A0) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found eq_ref00:=(eq_ref0 a):(((eq fofType) a) a) % Found (eq_ref0 a) as proof of (((eq fofType) a) ((breln1invset A) R)) % Found ((eq_ref fofType) a) as proof of (((eq fofType) a) ((breln1invset A) R)) % Found ((eq_ref fofType) a) as proof of (((eq fofType) a) ((breln1invset A) R)) % Found ((eq_ref fofType) a) as proof of (((eq fofType) a) ((breln1invset A) R)) % Found eq_ref00:=(eq_ref0 a):(((eq fofType) a) a) % Found (eq_ref0 a) as proof of (((eq fofType) a) ((breln1invset A) R)) % Found ((eq_ref fofType) a) as proof of (((eq fofType) a) ((breln1invset A) R)) % Found ((eq_ref fofType) a) as proof of (((eq fofType) a) ((breln1invset A) R)) % Found ((eq_ref fofType) a) as proof of (((eq fofType) a) ((breln1invset A) R)) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found eq_ref00:=(eq_ref0 ((breln1invset A) ((breln1invset A) R))):(((eq fofType) ((breln1invset A) ((breln1invset A) R))) ((breln1invset A) ((breln1invset A) R))) % Found (eq_ref0 ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found eq_ref00:=(eq_ref0 ((breln1invset A) ((breln1invset A) R))):(((eq fofType) ((breln1invset A) ((breln1invset A) R))) ((breln1invset A) ((breln1invset A) R))) % Found (eq_ref0 ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found eq_ref00:=(eq_ref0 ((breln1invset A) ((breln1invset A) R))):(((eq fofType) ((breln1invset A) ((breln1invset A) R))) ((breln1invset A) ((breln1invset A) R))) % Found (eq_ref0 ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) 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 x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x50:(P b) % Found (fun (x50:(P b))=> x50) as proof of (P b) % Found (fun (x50:(P b))=> x50) as proof of (P0 b) % Found eq_ref00:=(eq_ref0 b0):(((eq fofType) b0) b0) % Found (eq_ref0 b0) as proof of (((eq fofType) b0) R) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) R) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) R) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) R) % Found eq_ref00:=(eq_ref0 ((breln1invset A) ((breln1invset A) R))):(((eq fofType) ((breln1invset A) ((breln1invset A) R))) ((breln1invset A) ((breln1invset A) R))) % Found (eq_ref0 ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b0) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b0) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b0) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b0) % Found x60:(P R) % Found (fun (x60:(P R))=> x60) as proof of (P R) % Found (fun (x60:(P R))=> x60) as proof of (P0 R) % Found x50:(P R) % Found (fun (x50:(P R))=> x50) as proof of (P R) % Found (fun (x50:(P R))=> x50) as proof of (P0 R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found eq_ref00:=(eq_ref0 R):(((eq fofType) R) R) % Found (eq_ref0 R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x50:(P ((breln1invset A) ((breln1invset A) R))) % Found (fun (x50:(P ((breln1invset A) ((breln1invset A) R))))=> x50) as proof of (P ((breln1invset A) ((breln1invset A) R))) % Found (fun (x50:(P ((breln1invset A) ((breln1invset A) R))))=> x50) as proof of (P0 ((breln1invset A) ((breln1invset A) R))) % Found eq_ref00:=(eq_ref0 ((breln1invset A) ((breln1invset A) R))):(((eq fofType) ((breln1invset A) ((breln1invset A) R))) ((breln1invset A) ((breln1invset A) R))) % Found (eq_ref0 ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b0) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b0) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b0) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b0) % Found eq_ref00:=(eq_ref0 b0):(((eq fofType) b0) b0) % Found (eq_ref0 b0) as proof of (((eq fofType) b0) b) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) b) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) b) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) b) % Found x60:(P ((breln1invset A) ((breln1invset A) R))) % Found (fun (x60:(P ((breln1invset A) ((breln1invset A) R))))=> x60) as proof of (P ((breln1invset A) ((breln1invset A) R))) % Found (fun (x60:(P ((breln1invset A) ((breln1invset A) R))))=> x60) as proof of (P0 ((breln1invset A) ((breln1invset A) R))) % Found x60:(P ((breln1invset A) ((breln1invset A) R))) % Found (fun (x60:(P ((breln1invset A) ((breln1invset A) R))))=> x60) as proof of (P ((breln1invset A) ((breln1invset A) R))) % Found (fun (x60:(P ((breln1invset A) ((breln1invset A) R))))=> x60) as proof of (P0 ((breln1invset A) ((breln1invset A) R))) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found eq_ref00:=(eq_ref0 ((breln1invset A) ((breln1invset A) R))):(((eq fofType) ((breln1invset A) ((breln1invset A) R))) ((breln1invset A) ((breln1invset A) R))) % Found (eq_ref0 ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found eq_ref00:=(eq_ref0 ((breln1invset A) ((breln1invset A) R))):(((eq fofType) ((breln1invset A) ((breln1invset A) R))) ((breln1invset A) ((breln1invset A) R))) % Found (eq_ref0 ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found eq_ref00:=(eq_ref0 ((breln1invset A) ((breln1invset A) R))):(((eq fofType) ((breln1invset A) ((breln1invset A) R))) ((breln1invset A) ((breln1invset A) R))) % Found (eq_ref0 ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found eq_ref00:=(eq_ref0 ((breln1invset A) ((breln1invset A) R))):(((eq fofType) ((breln1invset A) ((breln1invset A) R))) ((breln1invset A) ((breln1invset A) R))) % Found (eq_ref0 ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found eq_ref00:=(eq_ref0 b0):(((eq fofType) b0) b0) % Found (eq_ref0 b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) b0) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) b0) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) b0) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) b0) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) A0) % Found eq_ref00:=(eq_ref0 R):(((eq fofType) R) R) % Found (eq_ref0 R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) 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 x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) A0) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x5:(P R) % Instantiate: b:=R:fofType % Found x5 as proof of (P0 b) % Found eq_ref00:=(eq_ref0 ((breln1invset A) ((breln1invset A) R))):(((eq fofType) ((breln1invset A) ((breln1invset A) R))) ((breln1invset A) ((breln1invset A) R))) % Found (eq_ref0 ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Instantiate: A0:=R:fofType % Found x4 as proof of ((breln1 A) A0) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x4:((breln1 A) R) % Instantiate: A0:=R:fofType % Found x4 as proof of ((breln1 A) A0) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x5:(P R) % Instantiate: A0:=R:fofType % Found x5 as proof of (P0 A0) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b0) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x1000:=(x100 x4):((breln1 A) ((breln1invset A) R)) % Found (x100 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found eq_ref00:=(eq_ref0 R):(((eq fofType) R) R) % Found (eq_ref0 R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Instantiate: A0:=R:fofType % Found x4 as proof of ((breln1 A) A0) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found eq_ref00:=(eq_ref0 ((breln1invset A) ((breln1invset A) R))):(((eq fofType) ((breln1invset A) ((breln1invset A) R))) ((breln1invset A) ((breln1invset A) R))) % Found (eq_ref0 ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found x5:(P0 b) % Instantiate: b:=R:fofType % Found (fun (x5:(P0 b))=> x5) as proof of (P0 R) % Found (fun (P0:(fofType->Prop)) (x5:(P0 b))=> x5) as proof of ((P0 b)->(P0 R)) % Found (fun (P0:(fofType->Prop)) (x5:(P0 b))=> x5) as proof of (P b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Instantiate: A0:=R:fofType % Found x4 as proof of ((breln1 A) A0) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x5:(P ((breln1invset A) ((breln1invset A) R))) % Instantiate: b:=((breln1invset A) ((breln1invset A) R)):fofType % Found x5 as proof of (P0 b) % Found eq_ref00:=(eq_ref0 R):(((eq fofType) R) R) % Found (eq_ref0 R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x9:((in ((kpair Xx) Xy)) A0) % Instantiate: A0:=R:fofType % Found (fun (x9:((in ((kpair Xx) Xy)) A0))=> x9) as proof of ((in ((kpair Xx) Xy)) R) % Found (fun (x8:((in Xy) A)) (x9:((in ((kpair Xx) Xy)) A0))=> x9) as proof of (((in ((kpair Xx) Xy)) A0)->((in ((kpair Xx) Xy)) R)) % Found (fun (Xy:fofType) (x8:((in Xy) A)) (x9:((in ((kpair Xx) Xy)) A0))=> x9) as proof of (((in Xy) A)->(((in ((kpair Xx) Xy)) A0)->((in ((kpair Xx) Xy)) R))) % Found (fun (x7:((in Xx) A)) (Xy:fofType) (x8:((in Xy) A)) (x9:((in ((kpair Xx) Xy)) A0))=> x9) as proof of (forall (Xy:fofType), (((in Xy) A)->(((in ((kpair Xx) Xy)) A0)->((in ((kpair Xx) Xy)) R)))) % Found (fun (Xx:fofType) (x7:((in Xx) A)) (Xy:fofType) (x8:((in Xy) A)) (x9:((in ((kpair Xx) Xy)) A0))=> x9) as proof of (((in Xx) A)->(forall (Xy:fofType), (((in Xy) A)->(((in ((kpair Xx) Xy)) A0)->((in ((kpair Xx) Xy)) R))))) % Found (fun (Xx:fofType) (x7:((in Xx) A)) (Xy:fofType) (x8:((in Xy) A)) (x9:((in ((kpair Xx) Xy)) A0))=> x9) as proof of (forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) A)->(((in ((kpair Xx) Xy)) A0)->((in ((kpair Xx) Xy)) R)))))) % Found (((x0000 x4) x4) (fun (Xx:fofType) (x7:((in Xx) A)) (Xy:fofType) (x8:((in Xy) A)) (x9:((in ((kpair Xx) Xy)) A0))=> x9)) as proof of ((subset A0) R) % Found ((((x000 A) x4) x4) (fun (Xx:fofType) (x7:((in Xx) A)) (Xy:fofType) (x8:((in Xy) A)) (x9:((in ((kpair Xx) Xy)) A0))=> x9)) as proof of ((subset A0) R) % Found (((((fun (A1:fofType) (x7:((breln1 A1) A0))=> (((x00 A1) x7) R)) A) x4) x4) (fun (Xx:fofType) (x7:((in Xx) A)) (Xy:fofType) (x8:((in Xy) A)) (x9:((in ((kpair Xx) Xy)) A0))=> x9)) as proof of ((subset A0) R) % Found (((((fun (A1:fofType) (x7:((breln1 A1) A0))=> ((((fun (A1:fofType)=> ((x0 A1) A0)) A1) x7) R)) A) x4) x4) (fun (Xx:fofType) (x7:((in Xx) A)) (Xy:fofType) (x8:((in Xy) A)) (x9:((in ((kpair Xx) Xy)) A0))=> x9)) as proof of ((subset A0) R) % Found (((((fun (A1:fofType) (x7:((breln1 A1) A0))=> ((((fun (A1:fofType)=> ((x0 A1) A0)) A1) x7) R)) A) x4) x4) (fun (Xx:fofType) (x7:((in Xx) A)) (Xy:fofType) (x8:((in Xy) A)) (x9:((in ((kpair Xx) Xy)) A0))=> x9)) as proof of ((subset A0) R) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x1000:=(x100 x4):((breln1 A) ((breln1invset A) R)) % Found (x100 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found x1000:=(x100 x4):((breln1 A) ((breln1invset A) R)) % Found (x100 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found x1000:=(x100 x4):((breln1 A) ((breln1invset A) R)) % Found (x100 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found eq_ref00:=(eq_ref0 R):(((eq fofType) R) R) % Found (eq_ref0 R) as proof of (((eq fofType) R) b0) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b0) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b0) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b0) % Found eq_ref00:=(eq_ref0 b0):(((eq fofType) b0) b0) % Found (eq_ref0 b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found x50:(P R) % Found (fun (x50:(P R))=> x50) as proof of (P R) % Found (fun (x50:(P R))=> x50) as proof of (P0 R) % Found eq_ref00:=(eq_ref0 R):(((eq fofType) R) R) % Found (eq_ref0 R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found x5:(P R) % Instantiate: a:=R:fofType % Found x5 as proof of (P0 a) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((breln1invset A) ((breln1invset A) R))) % Found eq_ref00:=(eq_ref0 a):(((eq fofType) a) a) % Found (eq_ref0 a) as proof of (((eq fofType) a) b) % Found ((eq_ref fofType) a) as proof of (((eq fofType) a) b) % Found ((eq_ref fofType) a) as proof of (((eq fofType) a) b) % Found ((eq_ref fofType) a) as proof of (((eq fofType) a) b) % Found eq_ref00:=(eq_ref0 a):(((eq fofType) a) a) % Found (eq_ref0 a) as proof of (((eq fofType) a) b) % Found ((eq_ref fofType) a) as proof of (((eq fofType) a) b) % Found ((eq_ref fofType) a) as proof of (((eq fofType) a) b) % Found ((eq_ref fofType) a) as proof of (((eq fofType) a) b) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x5:(P ((breln1invset A) ((breln1invset A) R))) % Instantiate: A0:=((breln1invset A) ((breln1invset A) R)):fofType % Found x5 as proof of (P0 A0) % Found x5:(P ((breln1invset A) ((breln1invset A) R))) % Instantiate: A0:=((breln1invset A) ((breln1invset A) R)):fofType % Found x5 as proof of (P0 A0) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b0) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x1000:=(x100 x4):((breln1 A) ((breln1invset A) R)) % Found (x100 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x1000:=(x100 x4):((breln1 A) ((breln1invset A) R)) % Found (x100 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found x1000:=(x100 x4):((breln1 A) ((breln1invset A) R)) % Found (x100 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found x1000:=(x100 x4):((breln1 A) ((breln1invset A) R)) % Found (x100 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found eq_ref00:=(eq_ref0 a):(((eq fofType) a) a) % Found (eq_ref0 a) as proof of (((eq fofType) a) ((breln1invset A) R)) % Found ((eq_ref fofType) a) as proof of (((eq fofType) a) ((breln1invset A) R)) % Found ((eq_ref fofType) a) as proof of (((eq fofType) a) ((breln1invset A) R)) % Found ((eq_ref fofType) a) as proof of (((eq fofType) a) ((breln1invset A) R)) % Found eq_ref00:=(eq_ref0 a):(((eq fofType) a) a) % Found (eq_ref0 a) as proof of (((eq fofType) a) ((breln1invset A) R)) % Found ((eq_ref fofType) a) as proof of (((eq fofType) a) ((breln1invset A) R)) % Found ((eq_ref fofType) a) as proof of (((eq fofType) a) ((breln1invset A) R)) % Found ((eq_ref fofType) a) as proof of (((eq fofType) a) ((breln1invset A) R)) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found eq_ref00:=(eq_ref0 ((breln1invset A) ((breln1invset A) R))):(((eq fofType) ((breln1invset A) ((breln1invset A) R))) ((breln1invset A) ((breln1invset A) R))) % Found (eq_ref0 ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found x5:(P2 b) % Instantiate: b:=R:fofType % Found (fun (x5:(P2 b))=> x5) as proof of (P2 R) % Found (fun (P2:(fofType->Prop)) (x5:(P2 b))=> x5) as proof of ((P2 b)->(P2 R)) % Found (fun (P2:(fofType->Prop)) (x5:(P2 b))=> x5) as proof of (P1 b) % Found eq_ref00:=(eq_ref0 ((breln1invset A) ((breln1invset A) R))):(((eq fofType) ((breln1invset A) ((breln1invset A) R))) ((breln1invset A) ((breln1invset A) R))) % Found (eq_ref0 ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found x5:(P2 b) % Instantiate: b:=R:fofType % Found (fun (x5:(P2 b))=> x5) as proof of (P2 R) % Found (fun (P2:(fofType->Prop)) (x5:(P2 b))=> x5) as proof of ((P2 b)->(P2 R)) % Found (fun (P2:(fofType->Prop)) (x5:(P2 b))=> x5) as proof of (P1 b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x4:((breln1 A) R) % Instantiate: b:=R:fofType % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x5:(P1 ((breln1invset A) ((breln1invset A) R))) % Instantiate: b:=((breln1invset A) ((breln1invset A) R)):fofType % Found x5 as proof of (P2 b) % Found eq_ref00:=(eq_ref0 R):(((eq fofType) R) R) % Found (eq_ref0 R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found x5:(P1 ((breln1invset A) ((breln1invset A) R))) % Instantiate: b:=((breln1invset A) ((breln1invset A) R)):fofType % Found x5 as proof of (P2 b) % Found eq_ref00:=(eq_ref0 R):(((eq fofType) R) R) % Found (eq_ref0 R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x4:((breln1 A) R) % Instantiate: b:=R:fofType % Found x4 as proof of ((breln1 A) b) % Found x1000:=(x100 x4):((breln1 A) ((breln1invset A) R)) % Found (x100 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found x1000:=(x100 x4):((breln1 A) ((breln1invset A) R)) % Found (x100 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x9:((in ((kpair Xx) Xy)) R) % Instantiate: A0:=R:fofType % Found (fun (x9:((in ((kpair Xx) Xy)) R))=> x9) as proof of ((in ((kpair Xx) Xy)) A0) % Found (fun (x8:((in Xy) A)) (x9:((in ((kpair Xx) Xy)) R))=> x9) as proof of (((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) A0)) % Found (fun (Xy:fofType) (x8:((in Xy) A)) (x9:((in ((kpair Xx) Xy)) R))=> x9) as proof of (((in Xy) A)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) A0))) % Found (fun (x7:((in Xx) A)) (Xy:fofType) (x8:((in Xy) A)) (x9:((in ((kpair Xx) Xy)) R))=> x9) as proof of (forall (Xy:fofType), (((in Xy) A)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) A0)))) % Found (fun (Xx:fofType) (x7:((in Xx) A)) (Xy:fofType) (x8:((in Xy) A)) (x9:((in ((kpair Xx) Xy)) R))=> x9) as proof of (((in Xx) A)->(forall (Xy:fofType), (((in Xy) A)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) A0))))) % Found (fun (Xx:fofType) (x7:((in Xx) A)) (Xy:fofType) (x8:((in Xy) A)) (x9:((in ((kpair Xx) Xy)) R))=> x9) as proof of (forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) A)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) A0)))))) % Found (((x0000 x4) x4) (fun (Xx:fofType) (x7:((in Xx) A)) (Xy:fofType) (x8:((in Xy) A)) (x9:((in ((kpair Xx) Xy)) R))=> x9)) as proof of ((subset R) A0) % Found ((((x000 A) x4) x4) (fun (Xx:fofType) (x7:((in Xx) A)) (Xy:fofType) (x8:((in Xy) A)) (x9:((in ((kpair Xx) Xy)) R))=> x9)) as proof of ((subset R) A0) % Found (((((fun (A1:fofType) (x7:((breln1 A1) R))=> (((x00 A1) x7) A0)) A) x4) x4) (fun (Xx:fofType) (x7:((in Xx) A)) (Xy:fofType) (x8:((in Xy) A)) (x9:((in ((kpair Xx) Xy)) R))=> x9)) as proof of ((subset R) A0) % Found (((((fun (A1:fofType) (x7:((breln1 A1) R))=> ((((fun (A1:fofType)=> ((x0 A1) R)) A1) x7) A0)) A) x4) x4) (fun (Xx:fofType) (x7:((in Xx) A)) (Xy:fofType) (x8:((in Xy) A)) (x9:((in ((kpair Xx) Xy)) R))=> x9)) as proof of ((subset R) A0) % Found (((((fun (A1:fofType) (x7:((breln1 A1) R))=> ((((fun (A1:fofType)=> ((x0 A1) R)) A1) x7) A0)) A) x4) x4) (fun (Xx:fofType) (x7:((in Xx) A)) (Xy:fofType) (x8:((in Xy) A)) (x9:((in ((kpair Xx) Xy)) R))=> x9)) as proof of ((subset R) A0) % Found x1000:=(x100 x4):((breln1 A) ((breln1invset A) R)) % Found (x100 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x1000:=(x100 x4):((breln1 A) ((breln1invset A) R)) % Found (x100 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found eq_ref00:=(eq_ref0 ((breln1invset A) ((breln1invset A) R))):(((eq fofType) ((breln1invset A) ((breln1invset A) R))) ((breln1invset A) ((breln1invset A) R))) % Found (eq_ref0 ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found eq_ref00:=(eq_ref0 ((breln1invset A) ((breln1invset A) R))):(((eq fofType) ((breln1invset A) ((breln1invset A) R))) ((breln1invset A) ((breln1invset A) R))) % Found (eq_ref0 ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found eq_ref00:=(eq_ref0 ((breln1invset A) ((breln1invset A) R))):(((eq fofType) ((breln1invset A) ((breln1invset A) R))) ((breln1invset A) ((breln1invset A) R))) % Found (eq_ref0 ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found eq_ref00:=(eq_ref0 ((breln1invset A) ((breln1invset A) R))):(((eq fofType) ((breln1invset A) ((breln1invset A) R))) ((breln1invset A) ((breln1invset A) R))) % Found (eq_ref0 ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found eq_ref00:=(eq_ref0 ((breln1invset A) ((breln1invset A) R))):(((eq fofType) ((breln1invset A) ((breln1invset A) R))) ((breln1invset A) ((breln1invset A) R))) % Found (eq_ref0 ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found eq_ref00:=(eq_ref0 ((breln1invset A) ((breln1invset A) R))):(((eq fofType) ((breln1invset A) ((breln1invset A) R))) ((breln1invset A) ((breln1invset A) R))) % Found (eq_ref0 ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % 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 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 R):(((eq fofType) R) R) % Found (eq_ref0 R) as proof of (((eq fofType) R) b0) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b0) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b0) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b0) % Found eq_ref00:=(eq_ref0 b0):(((eq fofType) b0) b0) % Found (eq_ref0 b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found eq_ref00:=(eq_ref0 R):(((eq fofType) R) R) % Found (eq_ref0 R) as proof of (((eq fofType) R) b0) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b0) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b0) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b0) % Found eq_ref00:=(eq_ref0 b0):(((eq fofType) b0) b0) % Found (eq_ref0 b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b0) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b0) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x50:(P b) % Found (fun (x50:(P b))=> x50) as proof of (P b) % Found (fun (x50:(P b))=> x50) as proof of (P0 b) % Found x50:(P b) % Found (fun (x50:(P b))=> x50) as proof of (P b) % Found (fun (x50:(P b))=> x50) as proof of (P0 b) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x5:(P b) % Found x5 as proof of (P0 R) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found eq_ref00:=(eq_ref0 R):(((eq fofType) R) R) % Found (eq_ref0 R) as proof of (((eq fofType) R) b0) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b0) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b0) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b0) % Found eq_ref00:=(eq_ref0 b0):(((eq fofType) b0) b0) % Found (eq_ref0 b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found x5:(P1 ((breln1invset A) ((breln1invset A) R))) % Instantiate: A0:=((breln1invset A) ((breln1invset A) R)):fofType % Found x5 as proof of (P2 A0) % Found x5:(P1 ((breln1invset A) ((breln1invset A) R))) % Instantiate: A0:=((breln1invset A) ((breln1invset A) R)):fofType % Found x5 as proof of (P2 A0) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x5:(P b) % Instantiate: b0:=b:fofType % Found x5 as proof of (P0 b0) % Found eq_ref00:=(eq_ref0 ((breln1invset A) ((breln1invset A) R))):(((eq fofType) ((breln1invset A) ((breln1invset A) R))) ((breln1invset A) ((breln1invset A) R))) % Found (eq_ref0 ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b0) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b0) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b0) % Found ((eq_ref fofType) ((breln1invset A) ((breln1invset A) R))) as proof of (((eq fofType) ((breln1invset A) ((breln1invset A) R))) b0) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x1000:=(x100 x4):((breln1 A) ((breln1invset A) R)) % Found (x100 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found x1000:=(x100 x4):((breln1 A) ((breln1invset A) R)) % Found (x100 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found x1000:=(x100 x4):((breln1 A) ((breln1invset A) R)) % Found (x100 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found x1000:=(x100 x4):((breln1 A) ((breln1invset A) R)) % Found (x100 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found x1000:=(x100 x4):((breln1 A) ((breln1invset A) R)) % Found (x100 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found x60:(P1 ((breln1invset A) ((breln1invset A) R))) % Found (fun (x60:(P1 ((breln1invset A) ((breln1invset A) R))))=> x60) as proof of (P1 ((breln1invset A) ((breln1invset A) R))) % Found (fun (x60:(P1 ((breln1invset A) ((breln1invset A) R))))=> x60) as proof of (P2 ((breln1invset A) ((breln1invset A) R))) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x1000:=(x100 x4):((breln1 A) ((breln1invset A) R)) % Found (x100 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found x1000:=(x100 x4):((breln1 A) ((breln1invset A) R)) % Found (x100 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found x5:(P ((breln1invset A) ((breln1invset A) R))) % Instantiate: b:=((breln1invset A) ((breln1invset A) R)):fofType % Found x5 as proof of (P0 b) % Found eq_ref00:=(eq_ref0 R):(((eq fofType) R) R) % Found (eq_ref0 R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x1010:=(x101 x4):((breln1 A) ((breln1invset A) R)) % Found (x101 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (x100 ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found ((x10 ((breln1invset A) R)) ((x10 R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4)) as proof of ((breln1 A) ((breln1invset A) ((breln1invset A) R))) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found eq_ref00:=(eq_ref0 R):(((eq fofType) R) R) % Found (eq_ref0 R) as proof of (((eq fofType) R) b0) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b0) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b0) % Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b0) % Found eq_ref00:=(eq_ref0 b0):(((eq fofType) b0) b0) % Found (eq_ref0 b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) ((breln1invset A) ((breln1invset A) R))) % Found x70:(P1 ((breln1invset A) ((breln1invset A) R))) % Found (fun (x70:(P1 ((breln1invset A) ((breln1invset A) R))))=> x70) as proof of (P1 ((breln1invset A) ((breln1invset A) R))) % Found (fun (x70:(P1 ((breln1invset A) ((breln1invset A) R))))=> x70) as proof of (P2 ((breln1invset A) ((breln1invset A) R))) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) R) % Found x4:((breln1 A) R) % Found x4 as proof of ((breln1 A) b) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x201000000:=(x20100000 x8):((in ((kpair Xy) Xx)) ((breln1invset A) R)) % Found (x20100000 x8) as proof of ((in ((kpair Xy) Xx)) ((breln1invset A) R)) % Found ((x2010000 x7) x8) as proof of ((in ((kpair Xy) Xx)) ((breln1invset A) R)) % Found (((x201000 Xy) x7) x8) as proof of ((in ((kpair Xy) Xx)) ((breln1invset A) R)) % Found ((((x20100 x6) Xy) x7) x8) as proof of ((in ((kpair Xy) Xx)) ((breln1invset A) R)) % Found (((((x2010 Xx) x6) Xy) x7) x8) as proof of ((in ((kpair Xy) Xx)) ((breln1invset A) R)) % Found ((((((x201 x4) Xx) x6) Xy) x7) x8) as proof of ((in ((kpair Xy) Xx)) ((breln1invset A) R)) % Found (((((((x20 R) x4) Xx) x6) Xy) x7) x8) as proof of ((in ((kpair Xy) Xx)) ((breln1invset A) R)) % Found (((((((x20 R) x4) Xx) x6) Xy) x7) x8) as proof of ((in ((kpair Xy) Xx)) ((breln1invset A) R)) % Found ((((x20000 (((x1 A) R) x4)) x7) x6) (((((((x20 R) x4) Xx) x6) Xy) x7) x8)) as proof of ((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))) % Found (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> (((x2000 x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) (((((((x20 R) x4) Xx) x6) Xy) x7) x8)) as proof of ((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))) % Found (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((x200 x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) (((((((x20 R) x4) Xx) x6) Xy) x7) x8)) as proof of ((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))) % Found (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> (((x20 ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) (((((((x20 R) x4) Xx) x6) Xy) x7) x8)) as proof of ((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))) % Found (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((((x2 A) ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) ((((((((x2 A) R) x4) Xx) x6) Xy) x7) x8)) as proof of ((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))) % Found (fun (x8:((in ((kpair Xx) Xy)) R))=> (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((((x2 A) ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) ((((((((x2 A) R) x4) Xx) x6) Xy) x7) x8))) as proof of ((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))) % Found (fun (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) R))=> (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((((x2 A) ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) ((((((((x2 A) R) x4) Xx) x6) Xy) x7) x8))) as proof of (((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R)))) % Found (fun (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) R))=> (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((((x2 A) ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) ((((((((x2 A) R) x4) Xx) x6) Xy) x7) x8))) as proof of (((in Xy) A)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))) % Found (fun (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) R))=> (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((((x2 A) ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) ((((((((x2 A) R) x4) Xx) x6) Xy) x7) x8))) as proof of (forall (Xy:fofType), (((in Xy) A)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R)))))) % Found (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) R))=> (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((((x2 A) ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) ((((((((x2 A) R) x4) Xx) x6) Xy) x7) x8))) as proof of (((in Xx) A)->(forall (Xy:fofType), (((in Xy) A)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))))) % Found (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) R))=> (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((((x2 A) ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) ((((((((x2 A) R) x4) Xx) x6) Xy) x7) x8))) as proof of (forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) A)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R)))))))) % Found (((x0000 x4) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) R))=> (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((((x2 A) ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) ((((((((x2 A) R) x4) Xx) x6) Xy) x7) x8)))) as proof of ((subset R) ((breln1invset A) ((breln1invset A) R))) % Found ((((x000 A) x4) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) R))=> (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((((x2 A) ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) ((((((((x2 A) R) x4) Xx) x6) Xy) x7) x8)))) as proof of ((subset R) ((breln1invset A) ((breln1invset A) R))) % Found (((((fun (A0:fofType) (x6:((breln1 A0) R))=> (((x00 A0) x6) ((breln1invset A) ((breln1invset A) R)))) A) x4) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) R))=> (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((((x2 A) ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) ((((((((x2 A) R) x4) Xx) x6) Xy) x7) x8)))) as proof of ((subset R) ((breln1invset A) ((breln1invset A) R))) % Found (((((fun (A0:fofType) (x6:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x0 A0) R)) A0) x6) ((breln1invset A) ((breln1invset A) R)))) A) x4) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) R))=> (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((((x2 A) ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) ((((((((x2 A) R) x4) Xx) x6) Xy) x7) x8)))) as proof of ((subset R) ((breln1invset A) ((breln1invset A) R))) % Found (((((fun (A0:fofType) (x6:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x0 A0) R)) A0) x6) ((breln1invset A) ((breln1invset A) R)))) A) x4) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) R))=> (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((((x2 A) ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) ((((((((x2 A) R) x4) Xx) x6) Xy) x7) x8)))) as proof of ((subset R) ((breln1invset A) ((breln1invset A) R))) % Found x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))) % Found x8 as proof of ((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))) % Found x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))) % Found x8 as proof of ((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))) % Found x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))) % Found x8 as proof of ((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))) % Found x8 as proof of ((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x7:((in Xy) A) % Found x7 as proof of ((in Xy) A) % Found x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))) % Found x8 as proof of ((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))) % Found x1000:=(x100 x4):((breln1 A) ((breln1invset A) R)) % Found (x100 x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((x10 R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found (((x1 A) R) x4) as proof of ((breln1 A) ((breln1invset A) R)) % Found ((((x31000 (((x1 A) R) x4)) x7) x6) x8) as proof of ((in ((kpair Xy) Xx)) ((breln1invset A) R)) % Found (((((x3100 A) (((x1 A) R) x4)) x7) x6) x8) as proof of ((in ((kpair Xy) Xx)) ((breln1invset A) R)) % Found ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> ((((x310 A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8) as proof of ((in ((kpair Xy) Xx)) ((breln1invset A) R)) % Found ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> (((x31 A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8) as proof of ((in ((kpair Xy) Xx)) ((breln1invset A) R)) % Found ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8) as proof of ((in ((kpair Xy) Xx)) ((breln1invset A) R)) % Found ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8) as proof of ((in ((kpair Xy) Xx)) ((breln1invset A) R)) % Found ((((x30000 x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8)) as proof of ((in ((kpair Xx) Xy)) R) % Found (((((x3000 A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8)) as proof of ((in ((kpair Xx) Xy)) R) % Found ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> ((((x300 A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8)) as proof of ((in ((kpair Xx) Xy)) R) % Found ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> (((x30 A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8)) as proof of ((in ((kpair Xx) Xy)) R) % Found ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x3 A0) R)) A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8)) as proof of ((in ((kpair Xx) Xy)) R) % Found (fun (x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))=> ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x3 A0) R)) A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8))) as proof of ((in ((kpair Xx) Xy)) R) % Found (fun (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))=> ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x3 A0) R)) A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8))) as proof of (((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R)))->((in ((kpair Xx) Xy)) R)) % Found (fun (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))=> ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x3 A0) R)) A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8))) as proof of (((in Xy) A)->(((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R)))->((in ((kpair Xx) Xy)) R))) % Found (fun (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))=> ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x3 A0) R)) A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8))) as proof of (forall (Xy:fofType), (((in Xy) A)->(((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R)))->((in ((kpair Xx) Xy)) R)))) % Found (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))=> ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x3 A0) R)) A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8))) as proof of (((in Xx) A)->(forall (Xy:fofType), (((in Xy) A)->(((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R)))->((in ((kpair Xx) Xy)) R))))) % Found (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))=> ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x3 A0) R)) A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8))) as proof of (forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) A)->(((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R)))->((in ((kpair Xx) Xy)) R)))))) % Found (((x0000 (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) x4) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))=> ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x3 A0) R)) A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8)))) as proof of ((subset ((breln1invset A) ((breln1invset A) R))) R) % Found ((((x000 A) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) x4) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))=> ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x3 A0) R)) A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8)))) as proof of ((subset ((breln1invset A) ((breln1invset A) R))) R) % Found (((((fun (A0:fofType) (x6:((breln1 A0) ((breln1invset A) ((breln1invset A) R))))=> (((x00 A0) x6) R)) A) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) x4) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))=> ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x3 A0) R)) A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8)))) as proof of ((subset ((breln1invset A) ((breln1invset A) R))) R) % Found (((((fun (A0:fofType) (x6:((breln1 A0) ((breln1invset A) ((breln1invset A) R))))=> ((((fun (A0:fofType)=> ((x0 A0) ((breln1invset A) ((breln1invset A) R)))) A0) x6) R)) A) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) x4) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))=> ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x3 A0) R)) A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8)))) as proof of ((subset ((breln1invset A) ((breln1invset A) R))) R) % Found (((((fun (A0:fofType) (x6:((breln1 A0) ((breln1invset A) ((breln1invset A) R))))=> ((((fun (A0:fofType)=> ((x0 A0) ((breln1invset A) ((breln1invset A) R)))) A0) x6) R)) A) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) x4) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))=> ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x3 A0) R)) A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8)))) as proof of ((subset ((breln1invset A) ((breln1invset A) R))) R) % Found ((x50 (((((fun (A0:fofType) (x6:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x0 A0) R)) A0) x6) ((breln1invset A) ((breln1invset A) R)))) A) x4) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) R))=> (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((((x2 A) ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) ((((((((x2 A) R) x4) Xx) x6) Xy) x7) x8))))) (((((fun (A0:fofType) (x6:((breln1 A0) ((breln1invset A) ((breln1invset A) R))))=> ((((fun (A0:fofType)=> ((x0 A0) ((breln1invset A) ((breln1invset A) R)))) A0) x6) R)) A) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) x4) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))=> ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x3 A0) R)) A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8))))) as proof of (((eq fofType) R) ((breln1invset A) ((breln1invset A) R))) % Found (((x5 ((breln1invset A) ((breln1invset A) R))) (((((fun (A0:fofType) (x6:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x0 A0) R)) A0) x6) ((breln1invset A) ((breln1invset A) R)))) A) x4) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) R))=> (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((((x2 A) ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) ((((((((x2 A) R) x4) Xx) x6) Xy) x7) x8))))) (((((fun (A0:fofType) (x6:((breln1 A0) ((breln1invset A) ((breln1invset A) R))))=> ((((fun (A0:fofType)=> ((x0 A0) ((breln1invset A) ((breln1invset A) R)))) A0) x6) R)) A) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) x4) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))=> ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x3 A0) R)) A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8))))) as proof of (((eq fofType) R) ((breln1invset A) ((breln1invset A) R))) % Found ((((x R) ((breln1invset A) ((breln1invset A) R))) (((((fun (A0:fofType) (x6:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x0 A0) R)) A0) x6) ((breln1invset A) ((breln1invset A) R)))) A) x4) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) R))=> (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((((x2 A) ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) ((((((((x2 A) R) x4) Xx) x6) Xy) x7) x8))))) (((((fun (A0:fofType) (x6:((breln1 A0) ((breln1invset A) ((breln1invset A) R))))=> ((((fun (A0:fofType)=> ((x0 A0) ((breln1invset A) ((breln1invset A) R)))) A0) x6) R)) A) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) x4) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))=> ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x3 A0) R)) A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8))))) as proof of (((eq fofType) R) ((breln1invset A) ((breln1invset A) R))) % Found (fun (x4:((breln1 A) R))=> ((((x R) ((breln1invset A) ((breln1invset A) R))) (((((fun (A0:fofType) (x6:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x0 A0) R)) A0) x6) ((breln1invset A) ((breln1invset A) R)))) A) x4) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) R))=> (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((((x2 A) ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) ((((((((x2 A) R) x4) Xx) x6) Xy) x7) x8))))) (((((fun (A0:fofType) (x6:((breln1 A0) ((breln1invset A) ((breln1invset A) R))))=> ((((fun (A0:fofType)=> ((x0 A0) ((breln1invset A) ((breln1invset A) R)))) A0) x6) R)) A) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) x4) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))=> ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x3 A0) R)) A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8)))))) as proof of (((eq fofType) R) ((breln1invset A) ((breln1invset A) R))) % Found (fun (R:fofType) (x4:((breln1 A) R))=> ((((x R) ((breln1invset A) ((breln1invset A) R))) (((((fun (A0:fofType) (x6:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x0 A0) R)) A0) x6) ((breln1invset A) ((breln1invset A) R)))) A) x4) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) R))=> (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((((x2 A) ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) ((((((((x2 A) R) x4) Xx) x6) Xy) x7) x8))))) (((((fun (A0:fofType) (x6:((breln1 A0) ((breln1invset A) ((breln1invset A) R))))=> ((((fun (A0:fofType)=> ((x0 A0) ((breln1invset A) ((breln1invset A) R)))) A0) x6) R)) A) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) x4) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))=> ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x3 A0) R)) A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8)))))) as proof of (((breln1 A) R)->(((eq fofType) R) ((breln1invset A) ((breln1invset A) R)))) % Found (fun (A:fofType) (R:fofType) (x4:((breln1 A) R))=> ((((x R) ((breln1invset A) ((breln1invset A) R))) (((((fun (A0:fofType) (x6:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x0 A0) R)) A0) x6) ((breln1invset A) ((breln1invset A) R)))) A) x4) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) R))=> (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((((x2 A) ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) ((((((((x2 A) R) x4) Xx) x6) Xy) x7) x8))))) (((((fun (A0:fofType) (x6:((breln1 A0) ((breln1invset A) ((breln1invset A) R))))=> ((((fun (A0:fofType)=> ((x0 A0) ((breln1invset A) ((breln1invset A) R)))) A0) x6) R)) A) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) x4) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))=> ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x3 A0) R)) A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8)))))) as proof of (forall (R:fofType), (((breln1 A) R)->(((eq fofType) R) ((breln1invset A) ((breln1invset A) R))))) % Found (fun (x3:breln1invE) (A:fofType) (R:fofType) (x4:((breln1 A) R))=> ((((x R) ((breln1invset A) ((breln1invset A) R))) (((((fun (A0:fofType) (x6:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x0 A0) R)) A0) x6) ((breln1invset A) ((breln1invset A) R)))) A) x4) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) R))=> (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((((x2 A) ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) ((((((((x2 A) R) x4) Xx) x6) Xy) x7) x8))))) (((((fun (A0:fofType) (x6:((breln1 A0) ((breln1invset A) ((breln1invset A) R))))=> ((((fun (A0:fofType)=> ((x0 A0) ((breln1invset A) ((breln1invset A) R)))) A0) x6) R)) A) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) x4) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))=> ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x3 A0) R)) A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8)))))) as proof of (forall (A:fofType) (R:fofType), (((breln1 A) R)->(((eq fofType) R) ((breln1invset A) ((breln1invset A) R))))) % Found (fun (x2:breln1invI) (x3:breln1invE) (A:fofType) (R:fofType) (x4:((breln1 A) R))=> ((((x R) ((breln1invset A) ((breln1invset A) R))) (((((fun (A0:fofType) (x6:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x0 A0) R)) A0) x6) ((breln1invset A) ((breln1invset A) R)))) A) x4) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) R))=> (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((((x2 A) ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) ((((((((x2 A) R) x4) Xx) x6) Xy) x7) x8))))) (((((fun (A0:fofType) (x6:((breln1 A0) ((breln1invset A) ((breln1invset A) R))))=> ((((fun (A0:fofType)=> ((x0 A0) ((breln1invset A) ((breln1invset A) R)))) A0) x6) R)) A) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) x4) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))=> ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x3 A0) R)) A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8)))))) as proof of (breln1invE->(forall (A:fofType) (R:fofType), (((breln1 A) R)->(((eq fofType) R) ((breln1invset A) ((breln1invset A) R)))))) % Found (fun (x1:breln1invprop) (x2:breln1invI) (x3:breln1invE) (A:fofType) (R:fofType) (x4:((breln1 A) R))=> ((((x R) ((breln1invset A) ((breln1invset A) R))) (((((fun (A0:fofType) (x6:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x0 A0) R)) A0) x6) ((breln1invset A) ((breln1invset A) R)))) A) x4) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) R))=> (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((((x2 A) ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) ((((((((x2 A) R) x4) Xx) x6) Xy) x7) x8))))) (((((fun (A0:fofType) (x6:((breln1 A0) ((breln1invset A) ((breln1invset A) R))))=> ((((fun (A0:fofType)=> ((x0 A0) ((breln1invset A) ((breln1invset A) R)))) A0) x6) R)) A) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) x4) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))=> ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x3 A0) R)) A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8)))))) as proof of (breln1invI->(breln1invE->(forall (A:fofType) (R:fofType), (((breln1 A) R)->(((eq fofType) R) ((breln1invset A) ((breln1invset A) R))))))) % Found (fun (x0:subbreln1) (x1:breln1invprop) (x2:breln1invI) (x3:breln1invE) (A:fofType) (R:fofType) (x4:((breln1 A) R))=> ((((x R) ((breln1invset A) ((breln1invset A) R))) (((((fun (A0:fofType) (x6:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x0 A0) R)) A0) x6) ((breln1invset A) ((breln1invset A) R)))) A) x4) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) R))=> (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((((x2 A) ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) ((((((((x2 A) R) x4) Xx) x6) Xy) x7) x8))))) (((((fun (A0:fofType) (x6:((breln1 A0) ((breln1invset A) ((breln1invset A) R))))=> ((((fun (A0:fofType)=> ((x0 A0) ((breln1invset A) ((breln1invset A) R)))) A0) x6) R)) A) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) x4) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))=> ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x3 A0) R)) A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8)))))) as proof of (breln1invprop->(breln1invI->(breln1invE->(forall (A:fofType) (R:fofType), (((breln1 A) R)->(((eq fofType) R) ((breln1invset A) ((breln1invset A) R)))))))) % Found (fun (x:setextsub) (x0:subbreln1) (x1:breln1invprop) (x2:breln1invI) (x3:breln1invE) (A:fofType) (R:fofType) (x4:((breln1 A) R))=> ((((x R) ((breln1invset A) ((breln1invset A) R))) (((((fun (A0:fofType) (x6:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x0 A0) R)) A0) x6) ((breln1invset A) ((breln1invset A) R)))) A) x4) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) R))=> (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((((x2 A) ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) ((((((((x2 A) R) x4) Xx) x6) Xy) x7) x8))))) (((((fun (A0:fofType) (x6:((breln1 A0) ((breln1invset A) ((breln1invset A) R))))=> ((((fun (A0:fofType)=> ((x0 A0) ((breln1invset A) ((breln1invset A) R)))) A0) x6) R)) A) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) x4) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))=> ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x3 A0) R)) A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8)))))) as proof of (subbreln1->(breln1invprop->(breln1invI->(breln1invE->(forall (A:fofType) (R:fofType), (((breln1 A) R)->(((eq fofType) R) ((breln1invset A) ((breln1invset A) R))))))))) % Found (fun (x:setextsub) (x0:subbreln1) (x1:breln1invprop) (x2:breln1invI) (x3:breln1invE) (A:fofType) (R:fofType) (x4:((breln1 A) R))=> ((((x R) ((breln1invset A) ((breln1invset A) R))) (((((fun (A0:fofType) (x6:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x0 A0) R)) A0) x6) ((breln1invset A) ((breln1invset A) R)))) A) x4) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) R))=> (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((((x2 A) ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) ((((((((x2 A) R) x4) Xx) x6) Xy) x7) x8))))) (((((fun (A0:fofType) (x6:((breln1 A0) ((breln1invset A) ((breln1invset A) R))))=> ((((fun (A0:fofType)=> ((x0 A0) ((breln1invset A) ((breln1invset A) R)))) A0) x6) R)) A) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) x4) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))=> ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x3 A0) R)) A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8)))))) as proof of (setextsub->(subbreln1->(breln1invprop->(breln1invI->(breln1invE->(forall (A:fofType) (R:fofType), (((breln1 A) R)->(((eq fofType) R) ((breln1invset A) ((breln1invset A) R)))))))))) % Got proof (fun (x:setextsub) (x0:subbreln1) (x1:breln1invprop) (x2:breln1invI) (x3:breln1invE) (A:fofType) (R:fofType) (x4:((breln1 A) R))=> ((((x R) ((breln1invset A) ((breln1invset A) R))) (((((fun (A0:fofType) (x6:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x0 A0) R)) A0) x6) ((breln1invset A) ((breln1invset A) R)))) A) x4) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) R))=> (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((((x2 A) ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) ((((((((x2 A) R) x4) Xx) x6) Xy) x7) x8))))) (((((fun (A0:fofType) (x6:((breln1 A0) ((breln1invset A) ((breln1invset A) R))))=> ((((fun (A0:fofType)=> ((x0 A0) ((breln1invset A) ((breln1invset A) R)))) A0) x6) R)) A) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) x4) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))=> ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x3 A0) R)) A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8)))))) % Time elapsed = 114.338272s % node=18361 cost=2245.000000 depth=37 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % (fun (x:setextsub) (x0:subbreln1) (x1:breln1invprop) (x2:breln1invI) (x3:breln1invE) (A:fofType) (R:fofType) (x4:((breln1 A) R))=> ((((x R) ((breln1invset A) ((breln1invset A) R))) (((((fun (A0:fofType) (x6:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x0 A0) R)) A0) x6) ((breln1invset A) ((breln1invset A) R)))) A) x4) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) R))=> (((((fun (x9:((breln1 A) ((breln1invset A) R))) (x10:((in Xy) A))=> ((((fun (x9:((breln1 A) ((breln1invset A) R)))=> ((((x2 A) ((breln1invset A) R)) x9) Xy)) x9) x10) Xx)) (((x1 A) R) x4)) x7) x6) ((((((((x2 A) R) x4) Xx) x6) Xy) x7) x8))))) (((((fun (A0:fofType) (x6:((breln1 A0) ((breln1invset A) ((breln1invset A) R))))=> ((((fun (A0:fofType)=> ((x0 A0) ((breln1invset A) ((breln1invset A) R)))) A0) x6) R)) A) (((x1 A) ((breln1invset A) R)) (((x1 A) R) x4))) x4) (fun (Xx:fofType) (x6:((in Xx) A)) (Xy:fofType) (x7:((in Xy) A)) (x8:((in ((kpair Xx) Xy)) ((breln1invset A) ((breln1invset A) R))))=> ((((((fun (A0:fofType) (x9:((breln1 A0) R)) (x10:((in Xx) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) R))=> ((((fun (A0:fofType)=> ((x3 A0) R)) A0) x9) Xx)) A0) x9) x10) Xy)) A) x4) x6) x7) ((((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R))) (x10:((in Xy) A0))=> (((((fun (A0:fofType) (x9:((breln1 A0) ((breln1invset A) R)))=> ((((fun (A0:fofType)=> ((x3 A0) ((breln1invset A) R))) A0) x9) Xy)) A0) x9) x10) Xx)) A) (((x1 A) R) x4)) x7) x6) x8)))))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------