%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SYO326^5 : TPTP v7.5.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n019.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 0s % DateTime : Tue Mar 29 00:51:10 EDT 2022 % Result : Theorem 1.07s 1.31s % Output : Proof 1.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SYO326^5 : TPTP v7.5.0. Released v4.0.0. % 0.11/0.12 % Command : python CASC.py /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.12/0.32 % Computer : n019.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPUModel : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % RAMPerCPU : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % DateTime : Sat Mar 12 03:53:12 EST 2022 % 0.17/0.33 % CPUTime : % 0.17/0.33 ModuleCmd_Load.c(213):ERROR:105: Unable to locate a modulefile for 'python/python27' % 0.17/0.34 Python 2.7.5 % 0.71/0.88 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox2/benchmark/', '/export/starexec/sandbox2/benchmark/'] % 0.71/0.88 FOF formula (<kernel.Constant object at 0x14afd40>, <kernel.DependentProduct object at 0x2b7829d45d88>) of role type named cC % 0.71/0.88 Using role type % 0.71/0.88 Declaring cC:(fofType->Prop) % 0.71/0.88 FOF formula (<kernel.Constant object at 0x14afd40>, <kernel.DependentProduct object at 0x2b7829d456c8>) of role type named f % 0.71/0.88 Using role type % 0.71/0.88 Declaring f:(fofType->fofType) % 0.71/0.88 FOF formula (<kernel.Constant object at 0x14abc20>, <kernel.DependentProduct object at 0x2b7829d45440>) of role type named cB % 0.71/0.88 Using role type % 0.71/0.88 Declaring cB:(fofType->(fofType->Prop)) % 0.71/0.88 FOF formula (<kernel.Constant object at 0x14abc20>, <kernel.DependentProduct object at 0x2b7829d458c0>) of role type named cA % 0.71/0.88 Using role type % 0.71/0.88 Declaring cA:(fofType->Prop) % 0.71/0.88 FOF formula ((ex (fofType->(fofType->Prop))) (fun (Xu:(fofType->(fofType->Prop)))=> ((and ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xu (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xu Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), (((Xu Xx) Xy)->((Xv Xx) Xy)))))))) of role conjecture named cSV8 % 0.71/0.88 Conjecture to prove = ((ex (fofType->(fofType->Prop))) (fun (Xu:(fofType->(fofType->Prop)))=> ((and ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xu (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xu Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), (((Xu Xx) Xy)->((Xv Xx) Xy)))))))):Prop % 0.71/0.88 Parameter fofType_DUMMY:fofType. % 0.71/0.88 We need to prove ['((ex (fofType->(fofType->Prop))) (fun (Xu:(fofType->(fofType->Prop)))=> ((and ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xu (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xu Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), (((Xu Xx) Xy)->((Xv Xx) Xy))))))))'] % 0.71/0.88 Parameter fofType:Type. % 0.71/0.88 Parameter cC:(fofType->Prop). % 0.71/0.88 Parameter f:(fofType->fofType). % 0.71/0.88 Parameter cB:(fofType->(fofType->Prop)). % 0.71/0.88 Parameter cA:(fofType->Prop). % 0.71/0.88 Trying to prove ((ex (fofType->(fofType->Prop))) (fun (Xu:(fofType->(fofType->Prop)))=> ((and ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xu (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xu Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), (((Xu Xx) Xy)->((Xv Xx) Xy)))))))) % 0.71/0.88 Found x00:((x Xx) Xy) % 0.71/0.88 Instantiate: x:=Xv:(fofType->(fofType->Prop)) % 0.71/0.88 Found x00 as proof of ((Xv Xx) Xy) % 0.71/0.88 Found (fun (x00:((x Xx) Xy))=> x00) as proof of ((Xv Xx) Xy) % 0.71/0.88 Found (fun (Xy:fofType) (x00:((x Xx) Xy))=> x00) as proof of (((x Xx) Xy)->((Xv Xx) Xy)) % 0.71/0.88 Found (fun (Xx:fofType) (Xy:fofType) (x00:((x Xx) Xy))=> x00) as proof of (forall (Xy:fofType), (((x Xx) Xy)->((Xv Xx) Xy))) % 0.71/0.88 Found (fun (x0:((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))) (Xx:fofType) (Xy:fofType) (x00:((x Xx) Xy))=> x00) as proof of (forall (Xx:fofType) (Xy:fofType), (((x Xx) Xy)->((Xv Xx) Xy))) % 0.71/0.88 Found x0000:=(x000 x0):((Xv Xx) Xy) % 0.71/0.88 Found (x000 x0) as proof of ((Xv Xx) Xy) % 0.71/0.88 Found ((x00 Xv) x0) as proof of ((Xv Xx) Xy) % 0.71/0.88 Found ((x00 Xv) x0) as proof of ((Xv Xx) Xy) % 0.71/0.88 Found (fun (x00:((x Xx) Xy))=> ((x00 Xv) x0)) as proof of ((Xv Xx) Xy) % 0.71/0.88 Found (fun (Xy:fofType) (x00:((x Xx) Xy))=> ((x00 Xv) x0)) as proof of (((x Xx) Xy)->((Xv Xx) Xy)) % 0.71/0.88 Found (fun (Xx:fofType) (Xy:fofType) (x00:((x Xx) Xy))=> ((x00 Xv) x0)) as proof of (forall (Xy:fofType), (((x Xx) Xy)->((Xv Xx) Xy))) % 1.07/1.25 Found (fun (x0:((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))) (Xx:fofType) (Xy:fofType) (x00:((x Xx) Xy))=> ((x00 Xv) x0)) as proof of (forall (Xx:fofType) (Xy:fofType), (((x Xx) Xy)->((Xv Xx) Xy))) % 1.07/1.25 Found (fun (Xv:(fofType->(fofType->Prop))) (x0:((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))) (Xx:fofType) (Xy:fofType) (x00:((x Xx) Xy))=> ((x00 Xv) x0)) as proof of (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), (((x Xx) Xy)->((Xv Xx) Xy)))) % 1.07/1.25 Found (fun (Xv:(fofType->(fofType->Prop))) (x0:((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))) (Xx:fofType) (Xy:fofType) (x00:((x Xx) Xy))=> ((x00 Xv) x0)) as proof of (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), (((x Xx) Xy)->((Xv Xx) Xy))))) % 1.07/1.25 Found x200:=(x20 x0):((Xv Xz) Xz) % 1.07/1.25 Found (x20 x0) as proof of ((Xv Xz) Xz) % 1.07/1.25 Found ((x2 Xz) x0) as proof of ((Xv Xz) Xz) % 1.07/1.25 Found (fun (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> ((x2 Xz) x0)) as proof of ((Xv Xz) Xz) % 1.07/1.25 Found (fun (x1:(forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> ((x2 Xz) x0)) as proof of ((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->((Xv Xz) Xz)) % 1.07/1.25 Found (fun (x1:(forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> ((x2 Xz) x0)) as proof of ((forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->((Xv Xz) Xz))) % 1.07/1.25 Found (and_rect00 (fun (x1:(forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> ((x2 Xz) x0))) as proof of ((Xv Xz) Xz) % 1.07/1.25 Found ((and_rect0 ((Xv Xz) Xz)) (fun (x1:(forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> ((x2 Xz) x0))) as proof of ((Xv Xz) Xz) % 1.07/1.25 Found (((fun (P:Type) (x1:((forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv Xz) Xz)) (fun (x1:(forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> ((x2 Xz) x0))) as proof of ((Xv Xz) Xz) % 1.07/1.25 Found (fun (x00:((and (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv Xz) Xz)) (fun (x1:(forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> ((x2 Xz) x0)))) as proof of ((Xv Xz) Xz) % 1.07/1.25 Found (fun (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv Xz) Xz)) (fun (x1:(forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> ((x2 Xz) x0)))) as proof of (((and (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))->((Xv Xz) Xz)) % 1.07/1.27 Found (fun (x0:(cC Xz)) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv Xz) Xz)) (fun (x1:(forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> ((x2 Xz) x0)))) as proof of ((x Xz) Xz) % 1.07/1.27 Found (fun (Xz:fofType) (x0:(cC Xz)) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv Xz) Xz)) (fun (x1:(forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> ((x2 Xz) x0)))) as proof of ((cC Xz)->((x Xz) Xz)) % 1.07/1.27 Found (fun (Xz:fofType) (x0:(cC Xz)) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv Xz) Xz)) (fun (x1:(forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> ((x2 Xz) x0)))) as proof of (forall (Xz:fofType), ((cC Xz)->((x Xz) Xz))) % 1.07/1.27 Found x1000:=(x100 x0):((Xv (f Xw)) Xz) % 1.07/1.27 Found (x100 x0) as proof of ((Xv (f Xw)) Xz) % 1.07/1.27 Found ((x10 Xz) x0) as proof of ((Xv (f Xw)) Xz) % 1.07/1.27 Found (((x1 Xw) Xz) x0) as proof of ((Xv (f Xw)) Xz) % 1.07/1.27 Found (fun (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0)) as proof of ((Xv (f Xw)) Xz) % 1.07/1.27 Found (fun (x1:(forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0)) as proof of ((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->((Xv (f Xw)) Xz)) % 1.07/1.27 Found (fun (x1:(forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0)) as proof of ((forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->((Xv (f Xw)) Xz))) % 1.07/1.27 Found (and_rect00 (fun (x1:(forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0))) as proof of ((Xv (f Xw)) Xz) % 1.07/1.27 Found ((and_rect0 ((Xv (f Xw)) Xz)) (fun (x1:(forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0))) as proof of ((Xv (f Xw)) Xz) % 1.07/1.27 Found (((fun (P:Type) (x1:((forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv (f Xw)) Xz)) (fun (x1:(forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0))) as proof of ((Xv (f Xw)) Xz) % 1.07/1.27 Found (fun (x00:((and (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv (f Xw)) Xz)) (fun (x1:(forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0)))) as proof of ((Xv (f Xw)) Xz) % 1.07/1.27 Found (fun (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv (f Xw)) Xz)) (fun (x1:(forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0)))) as proof of (((and (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))->((Xv (f Xw)) Xz)) % 1.07/1.27 Found (fun (x0:((and (cA Xw)) ((cB Xz) Xw))) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv (f Xw)) Xz)) (fun (x1:(forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0)))) as proof of ((x (f Xw)) Xz) % 1.07/1.27 Found (fun (Xz:fofType) (x0:((and (cA Xw)) ((cB Xz) Xw))) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv (f Xw)) Xz)) (fun (x1:(forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0)))) as proof of (((and (cA Xw)) ((cB Xz) Xw))->((x (f Xw)) Xz)) % 1.07/1.27 Found (fun (Xw:fofType) (Xz:fofType) (x0:((and (cA Xw)) ((cB Xz) Xw))) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv (f Xw)) Xz)) (fun (x1:(forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0)))) as proof of (forall (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((x (f Xw)) Xz))) % 1.07/1.27 Found (fun (Xw:fofType) (Xz:fofType) (x0:((and (cA Xw)) ((cB Xz) Xw))) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv (f Xw)) Xz)) (fun (x1:(forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0)))) as proof of (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((x (f Xw)) Xz))) % 1.07/1.27 Found ((conj10 (fun (Xw:fofType) (Xz:fofType) (x0:((and (cA Xw)) ((cB Xz) Xw))) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv (f Xw)) Xz)) (fun (x1:(forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0))))) (fun (Xz:fofType) (x0:(cC Xz)) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv Xz) Xz)) (fun (x1:(forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> ((x2 Xz) x0))))) as proof of ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((x (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((x Xz) Xz)))) % 1.07/1.27 Found (((conj1 (forall (Xz:fofType), ((cC Xz)->((x Xz) Xz)))) (fun (Xw:fofType) (Xz:fofType) (x0:((and (cA Xw)) ((cB Xz) Xw))) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv (f Xw)) Xz)) (fun (x1:(forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0))))) (fun (Xz:fofType) (x0:(cC Xz)) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv Xz) Xz)) (fun (x1:(forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> ((x2 Xz) x0))))) as proof of ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((x (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((x Xz) Xz)))) % 1.07/1.28 Found ((((conj (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((x (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((x Xz) Xz)))) (fun (Xw:fofType) (Xz:fofType) (x0:((and (cA Xw)) ((cB Xz) Xw))) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv (f Xw)) Xz)) (fun (x1:(forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0))))) (fun (Xz:fofType) (x0:(cC Xz)) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv Xz) Xz)) (fun (x1:(forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> ((x2 Xz) x0))))) as proof of ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((x (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((x Xz) Xz)))) % 1.07/1.28 Found ((((conj (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((x (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((x Xz) Xz)))) (fun (Xw:fofType) (Xz:fofType) (x0:((and (cA Xw)) ((cB Xz) Xw))) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv (f Xw)) Xz)) (fun (x1:(forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0))))) (fun (Xz:fofType) (x0:(cC Xz)) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv Xz) Xz)) (fun (x1:(forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> ((x2 Xz) x0))))) as proof of ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((x (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((x Xz) Xz)))) % 1.07/1.28 Found ((conj00 ((((conj (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((x (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((x Xz) Xz)))) (fun (Xw:fofType) (Xz:fofType) (x0:((and (cA Xw)) ((cB Xz) Xw))) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv (f Xw)) Xz)) (fun (x1:(forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0))))) (fun (Xz:fofType) (x0:(cC Xz)) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv Xz) Xz)) (fun (x1:(forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> ((x2 Xz) x0)))))) (fun (Xv:(fofType->(fofType->Prop))) (x0:((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))) (Xx:fofType) (Xy:fofType) (x00:((x Xx) Xy))=> ((x00 Xv) x0))) as proof of ((and ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((x (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((x Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), (((x Xx) Xy)->((Xv Xx) Xy)))))) % 1.07/1.28 Found (((conj0 (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), (((x Xx) Xy)->((Xv Xx) Xy)))))) ((((conj (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((x (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((x Xz) Xz)))) (fun (Xw:fofType) (Xz:fofType) (x0:((and (cA Xw)) ((cB Xz) Xw))) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv (f Xw)) Xz)) (fun (x1:(forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0))))) (fun (Xz:fofType) (x0:(cC Xz)) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv Xz) Xz)) (fun (x1:(forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> ((x2 Xz) x0)))))) (fun (Xv:(fofType->(fofType->Prop))) (x0:((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))) (Xx:fofType) (Xy:fofType) (x00:((x Xx) Xy))=> ((x00 Xv) x0))) as proof of ((and ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((x (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((x Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), (((x Xx) Xy)->((Xv Xx) Xy)))))) % 1.07/1.28 Found ((((conj ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((x (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((x Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), (((x Xx) Xy)->((Xv Xx) Xy)))))) ((((conj (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((x (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((x Xz) Xz)))) (fun (Xw:fofType) (Xz:fofType) (x0:((and (cA Xw)) ((cB Xz) Xw))) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv (f Xw)) Xz)) (fun (x1:(forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0))))) (fun (Xz:fofType) (x0:(cC Xz)) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv Xz) Xz)) (fun (x1:(forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> ((x2 Xz) x0)))))) (fun (Xv:(fofType->(fofType->Prop))) (x0:((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))) (Xx:fofType) (Xy:fofType) (x00:((x Xx) Xy))=> ((x00 Xv) x0))) as proof of ((and ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((x (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((x Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), (((x Xx) Xy)->((Xv Xx) Xy)))))) % 1.07/1.29 Found ((((conj ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((x (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((x Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), (((x Xx) Xy)->((Xv Xx) Xy)))))) ((((conj (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((x (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((x Xz) Xz)))) (fun (Xw:fofType) (Xz:fofType) (x0:((and (cA Xw)) ((cB Xz) Xw))) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv (f Xw)) Xz)) (fun (x1:(forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0))))) (fun (Xz:fofType) (x0:(cC Xz)) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv Xz) Xz)) (fun (x1:(forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> ((x2 Xz) x0)))))) (fun (Xv:(fofType->(fofType->Prop))) (x0:((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))) (Xx:fofType) (Xy:fofType) (x00:((x Xx) Xy))=> ((x00 Xv) x0))) as proof of ((and ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((x (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((x Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), (((x Xx) Xy)->((Xv Xx) Xy)))))) % 1.07/1.29 Found (ex_intro000 ((((conj ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((x (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((x Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), (((x Xx) Xy)->((Xv Xx) Xy)))))) ((((conj (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((x (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((x Xz) Xz)))) (fun (Xw:fofType) (Xz:fofType) (x0:((and (cA Xw)) ((cB Xz) Xw))) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv (f Xw)) Xz)) (fun (x1:(forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0))))) (fun (Xz:fofType) (x0:(cC Xz)) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv Xz) Xz)) (fun (x1:(forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> ((x2 Xz) x0)))))) (fun (Xv:(fofType->(fofType->Prop))) (x0:((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))) (Xx:fofType) (Xy:fofType) (x00:((x Xx) Xy))=> ((x00 Xv) x0)))) as proof of ((ex (fofType->(fofType->Prop))) (fun (Xu:(fofType->(fofType->Prop)))=> ((and ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xu (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xu Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), (((Xu Xx) Xy)->((Xv Xx) Xy)))))))) % 1.07/1.29 Found ((ex_intro00 (fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1))))) ((((conj ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), ((((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) Xx) Xy)->((Xv Xx) Xy)))))) ((((conj (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) Xz) Xz)))) (fun (Xw:fofType) (Xz:fofType) (x0:((and (cA Xw)) ((cB Xz) Xw))) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv (f Xw)) Xz)) (fun (x1:(forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0))))) (fun (Xz:fofType) (x0:(cC Xz)) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv Xz) Xz)) (fun (x1:(forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> ((x2 Xz) x0)))))) (fun (Xv:(fofType->(fofType->Prop))) (x0:((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))) (Xx:fofType) (Xy:fofType) (x00:(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) Xx) Xy))=> ((x00 Xv) x0)))) as proof of ((ex (fofType->(fofType->Prop))) (fun (Xu:(fofType->(fofType->Prop)))=> ((and ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xu (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xu Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), (((Xu Xx) Xy)->((Xv Xx) Xy)))))))) % 1.07/1.29 Found (((ex_intro0 (fun (Xu:(fofType->(fofType->Prop)))=> ((and ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xu (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xu Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), (((Xu Xx) Xy)->((Xv Xx) Xy)))))))) (fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1))))) ((((conj ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), ((((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) Xx) Xy)->((Xv Xx) Xy)))))) ((((conj (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) Xz) Xz)))) (fun (Xw:fofType) (Xz:fofType) (x0:((and (cA Xw)) ((cB Xz) Xw))) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv (f Xw)) Xz)) (fun (x1:(forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0))))) (fun (Xz:fofType) (x0:(cC Xz)) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv Xz) Xz)) (fun (x1:(forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> ((x2 Xz) x0)))))) (fun (Xv:(fofType->(fofType->Prop))) (x0:((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))) (Xx:fofType) (Xy:fofType) (x00:(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) Xx) Xy))=> ((x00 Xv) x0)))) as proof of ((ex (fofType->(fofType->Prop))) (fun (Xu:(fofType->(fofType->Prop)))=> ((and ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xu (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xu Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), (((Xu Xx) Xy)->((Xv Xx) Xy)))))))) % 1.07/1.30 Found ((((ex_intro (fofType->(fofType->Prop))) (fun (Xu:(fofType->(fofType->Prop)))=> ((and ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xu (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xu Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), (((Xu Xx) Xy)->((Xv Xx) Xy)))))))) (fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1))))) ((((conj ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), ((((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) Xx) Xy)->((Xv Xx) Xy)))))) ((((conj (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) Xz) Xz)))) (fun (Xw:fofType) (Xz:fofType) (x0:((and (cA Xw)) ((cB Xz) Xw))) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv (f Xw)) Xz)) (fun (x1:(forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0))))) (fun (Xz:fofType) (x0:(cC Xz)) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv Xz) Xz)) (fun (x1:(forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> ((x2 Xz) x0)))))) (fun (Xv:(fofType->(fofType->Prop))) (x0:((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))) (Xx:fofType) (Xy:fofType) (x00:(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) Xx) Xy))=> ((x00 Xv) x0)))) as proof of ((ex (fofType->(fofType->Prop))) (fun (Xu:(fofType->(fofType->Prop)))=> ((and ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xu (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xu Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), (((Xu Xx) Xy)->((Xv Xx) Xy)))))))) % 1.07/1.30 Found ((((ex_intro (fofType->(fofType->Prop))) (fun (Xu:(fofType->(fofType->Prop)))=> ((and ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xu (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xu Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), (((Xu Xx) Xy)->((Xv Xx) Xy)))))))) (fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1))))) ((((conj ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), ((((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) Xx) Xy)->((Xv Xx) Xy)))))) ((((conj (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) Xz) Xz)))) (fun (Xw:fofType) (Xz:fofType) (x0:((and (cA Xw)) ((cB Xz) Xw))) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv (f Xw)) Xz)) (fun (x1:(forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0))))) (fun (Xz:fofType) (x0:(cC Xz)) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv Xz) Xz)) (fun (x1:(forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> ((x2 Xz) x0)))))) (fun (Xv:(fofType->(fofType->Prop))) (x0:((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))) (Xx:fofType) (Xy:fofType) (x00:(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) Xx) Xy))=> ((x00 Xv) x0)))) as proof of ((ex (fofType->(fofType->Prop))) (fun (Xu:(fofType->(fofType->Prop)))=> ((and ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xu (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xu Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), (((Xu Xx) Xy)->((Xv Xx) Xy)))))))) % 1.07/1.30 Got proof ((((ex_intro (fofType->(fofType->Prop))) (fun (Xu:(fofType->(fofType->Prop)))=> ((and ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xu (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xu Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), (((Xu Xx) Xy)->((Xv Xx) Xy)))))))) (fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1))))) ((((conj ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), ((((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) Xx) Xy)->((Xv Xx) Xy)))))) ((((conj (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) Xz) Xz)))) (fun (Xw:fofType) (Xz:fofType) (x0:((and (cA Xw)) ((cB Xz) Xw))) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv (f Xw)) Xz)) (fun (x1:(forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0))))) (fun (Xz:fofType) (x0:(cC Xz)) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv Xz) Xz)) (fun (x1:(forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> ((x2 Xz) x0)))))) (fun (Xv:(fofType->(fofType->Prop))) (x0:((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))) (Xx:fofType) (Xy:fofType) (x00:(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) Xx) Xy))=> ((x00 Xv) x0)))) % 1.07/1.31 Time elapsed = 0.684992s % 1.07/1.31 node=97 cost=850.000000 depth=27 % 1.07/1.31 :::::::::::::::::::::: % 1.07/1.31 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.07/1.31 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.07/1.31 ((((ex_intro (fofType->(fofType->Prop))) (fun (Xu:(fofType->(fofType->Prop)))=> ((and ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xu (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xu Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), (((Xu Xx) Xy)->((Xv Xx) Xy)))))))) (fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1))))) ((((conj ((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) Xz) Xz))))) (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->(forall (Xx:fofType) (Xy:fofType), ((((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) Xx) Xy)->((Xv Xx) Xy)))))) ((((conj (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) Xz) Xz)))) (fun (Xw:fofType) (Xz:fofType) (x0:((and (cA Xw)) ((cB Xz) Xw))) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv (f Xw)) Xz)) (fun (x1:(forall (Xw0:fofType) (Xz0:fofType), (((and (cA Xw0)) ((cB Xz0) Xw0))->((Xv (f Xw0)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> (((x1 Xw) Xz) x0))))) (fun (Xz:fofType) (x0:(cC Xz)) (Xv:(fofType->(fofType->Prop))) (x00:((and (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))))=> (((fun (P:Type) (x1:((forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))->((forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))->P)))=> (((((and_rect (forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0)))) P) x1) x00)) ((Xv Xz) Xz)) (fun (x1:(forall (Xw:fofType) (Xz0:fofType), (((and (cA Xw)) ((cB Xz0) Xw))->((Xv (f Xw)) Xz0)))) (x2:(forall (Xz0:fofType), ((cC Xz0)->((Xv Xz0) Xz0))))=> ((x2 Xz) x0)))))) (fun (Xv:(fofType->(fofType->Prop))) (x0:((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))) (Xx:fofType) (Xy:fofType) (x00:(((fun (a0:fofType) (a1:fofType)=> (forall (Xv:(fofType->(fofType->Prop))), (((and (forall (Xw:fofType) (Xz:fofType), (((and (cA Xw)) ((cB Xz) Xw))->((Xv (f Xw)) Xz)))) (forall (Xz:fofType), ((cC Xz)->((Xv Xz) Xz))))->((Xv a0) a1)))) Xx) Xy))=> ((x00 Xv) x0)))) % 1.16/1.31 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------