%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEU826^1 : TPTP v6.1.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n111.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:15 EDT 2014 % Result : Theorem 31.28s % Output : Proof 31.28s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SEU826^1 : TPTP v6.1.0. Released v3.7.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n111.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:35:26 CDT 2014 % % CPUTime : 31.28 % Python 2.7.5 % Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % FOF formula (<kernel.Constant object at 0x1c5d638>, <kernel.DependentProduct object at 0x1c5d3f8>) of role type named seteq_type % Using role type % Declaring seteq:((fofType->Prop)->((fofType->Prop)->Prop)) % FOF formula (((eq ((fofType->Prop)->((fofType->Prop)->Prop))) seteq) (fun (X:(fofType->Prop)) (Y:(fofType->Prop))=> (forall (U:fofType), ((iff (X U)) (Y U))))) of role definition named seteq % A new definition: (((eq ((fofType->Prop)->((fofType->Prop)->Prop))) seteq) (fun (X:(fofType->Prop)) (Y:(fofType->Prop))=> (forall (U:fofType), ((iff (X U)) (Y U))))) % Defined: seteq:=(fun (X:(fofType->Prop)) (Y:(fofType->Prop))=> (forall (U:fofType), ((iff (X U)) (Y U)))) % FOF formula (<kernel.Constant object at 0x1b3c4d0>, <kernel.DependentProduct object at 0x1c5db48>) of role type named u_type % Using role type % Declaring u:((fofType->Prop)->((fofType->Prop)->(fofType->Prop))) % FOF formula (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) u) (fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((or (X U)) (Y U)))) of role definition named u % A new definition: (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) u) (fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((or (X U)) (Y U)))) % Defined: u:=(fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((or (X U)) (Y U))) % FOF formula (<kernel.Constant object at 0x1c5db48>, <kernel.DependentProduct object at 0x1c5d560>) of role type named n_type % Using role type % Declaring n:((fofType->Prop)->((fofType->Prop)->(fofType->Prop))) % FOF formula (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) n) (fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((and (X U)) (Y U)))) of role definition named n % A new definition: (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) n) (fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((and (X U)) (Y U)))) % Defined: n:=(fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((and (X U)) (Y U))) % FOF formula (<kernel.Constant object at 0x1c5d560>, <kernel.DependentProduct object at 0x1c5d518>) of role type named a_type % Using role type % Declaring a:(fofType->Prop) % FOF formula (<kernel.Constant object at 0x1c5d638>, <kernel.DependentProduct object at 0x1c5dcb0>) of role type named b_type % Using role type % Declaring b:(fofType->Prop) % FOF formula (<kernel.Constant object at 0x1c5db48>, <kernel.DependentProduct object at 0x1c5dab8>) of role type named c_type % Using role type % Declaring c:(fofType->Prop) % FOF formula ((seteq ((u a) ((n b) c))) ((n ((u a) b)) ((u a) c))) of role conjecture named conj % Conjecture to prove = ((seteq ((u a) ((n b) c))) ((n ((u a) b)) ((u a) c))):Prop % Parameter fofType_DUMMY:fofType. % We need to prove ['((seteq ((u a) ((n b) c))) ((n ((u a) b)) ((u a) c)))'] % Parameter fofType:Type. % Definition seteq:=(fun (X:(fofType->Prop)) (Y:(fofType->Prop))=> (forall (U:fofType), ((iff (X U)) (Y U)))):((fofType->Prop)->((fofType->Prop)->Prop)). % Definition u:=(fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((or (X U)) (Y U))):((fofType->Prop)->((fofType->Prop)->(fofType->Prop))). % Definition n:=(fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((and (X U)) (Y U))):((fofType->Prop)->((fofType->Prop)->(fofType->Prop))). % Parameter a:(fofType->Prop). % Parameter b:(fofType->Prop). % Parameter c:(fofType->Prop). % Trying to prove ((seteq ((u a) ((n b) c))) ((n ((u a) b)) ((u a) c))) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_introl000:=(or_introl00 (((n b) c) U)):((or (a U)) (((n b) c) U)) % Found (or_introl00 (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found ((fun (B:Prop)=> ((or_introl0 B) x2)) (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U))) as proof of (((u a) ((n b) c)) U) % Found (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U))) as proof of ((a U)->(((u a) ((n b) c)) U)) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_introl000:=(or_introl00 (((n b) c) U)):((or (a U)) (((n b) c) U)) % Found (or_introl00 (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found ((fun (B:Prop)=> ((or_introl0 B) x2)) (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U))) as proof of (((u a) ((n b) c)) U) % Found (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U))) as proof of ((a U)->(((u a) ((n b) c)) U)) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found x2:(a U) % Found (fun (x2:(a U))=> x2) as proof of (a U) % Found (fun (x2:(a U))=> x2) as proof of ((a U)->(a U)) % Found x2:(a U) % Found (fun (x2:(a U))=> x2) as proof of (a U) % Found (fun (x2:(a U))=> x2) as proof of ((a U)->(a U)) % Found x2:(a U) % Found (fun (x2:(a U))=> x2) as proof of (a U) % Found (fun (x2:(a U))=> x2) as proof of ((a U)->(a U)) % Found x2:(a U) % Found (fun (x2:(a U))=> x2) as proof of (a U) % Found (fun (x2:(a U))=> x2) as proof of ((a U)->(a U)) % Found x2:(a U) % Found (fun (x2:(a U))=> x2) as proof of (a U) % Found (fun (x2:(a U))=> x2) as proof of ((a U)->(a U)) % Found x2:(a U) % Found (fun (x2:(a U))=> x2) as proof of (a U) % Found (fun (x2:(a U))=> x2) as proof of ((a U)->(a U)) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_introl000:=(or_introl00 (((n b) c) U)):((or (a U)) (((n b) c) U)) % Found (or_introl00 (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found ((fun (B:Prop)=> ((or_introl0 B) x3)) (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U))) as proof of (((u a) ((n b) c)) U) % Found (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U))) as proof of ((a U)->(((u a) ((n b) c)) U)) % Found or_introl000:=(or_introl00 (((n b) c) U)):((or (a U)) (((n b) c) U)) % Found (or_introl00 (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found ((fun (B:Prop)=> ((or_introl0 B) x3)) (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U))) as proof of (((u a) ((n b) c)) U) % Found (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U))) as proof of ((a U)->(((u a) ((n b) c)) U)) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found x2:(a U) % Found (fun (x2:(a U))=> x2) as proof of (a U) % Found (fun (x2:(a U))=> x2) as proof of ((a U)->(a U)) % Found x2:(a U) % Found (fun (x2:(a U))=> x2) as proof of (a U) % Found (fun (x2:(a U))=> x2) as proof of ((a U)->(a U)) % Found x2:(a U) % Found (fun (x2:(a U))=> x2) as proof of (a U) % Found (fun (x2:(a U))=> x2) as proof of ((a U)->(a U)) % Found x2:(a U) % Found (fun (x2:(a U))=> x2) as proof of (a U) % Found (fun (x2:(a U))=> x2) as proof of ((a U)->(a U)) % Found x2:(a U) % Found (fun (x2:(a U))=> x2) as proof of (a U) % Found (fun (x2:(a U))=> x2) as proof of ((a U)->(a U)) % Found x2:(a U) % Found (fun (x2:(a U))=> x2) as proof of (a U) % Found (fun (x2:(a U))=> x2) as proof of ((a U)->(a U)) % Found x2:(a U) % Found (fun (x2:(a U))=> x2) as proof of (a U) % Found (fun (x2:(a U))=> x2) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x2:(a U) % Found (fun (x2:(a U))=> x2) as proof of (a U) % Found (fun (x2:(a U))=> x2) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found x3:(a U) % Found (fun (x3:(a U))=> x3) as proof of (a U) % Found (fun (x3:(a U))=> x3) as proof of ((a U)->(a U)) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_introl00:=(or_introl0 (b U)):((a U)->((or (a U)) (b U))) % Found (or_introl0 (b U)) as proof of ((a U)->((or (a U)) (b U))) % Found ((or_introl (a U)) (b U)) as proof of ((a U)->((or (a U)) (b U))) % Found ((or_introl (a U)) (b U)) as proof of ((a U)->((or (a U)) (b U))) % Found or_introl00:=(or_introl0 (c U)):((a U)->((or (a U)) (c U))) % Found (or_introl0 (c U)) as proof of ((a U)->((or (a U)) (c U))) % Found ((or_introl (a U)) (c U)) as proof of ((a U)->((or (a U)) (c U))) % Found ((or_introl (a U)) (c U)) as proof of ((a U)->((or (a U)) (c U))) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_introl000:=(or_introl00 (((n b) c) U)):((or (a U)) (((n b) c) U)) % Found (or_introl00 (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found ((fun (B:Prop)=> ((or_introl0 B) x2)) (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U))) as proof of (((u a) ((n b) c)) U) % Found (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U))) as proof of ((a U)->(((u a) ((n b) c)) U)) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_introl000:=(or_introl00 (((n b) c) U)):((or (a U)) (((n b) c) U)) % Found (or_introl00 (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found ((fun (B:Prop)=> ((or_introl0 B) x2)) (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U))) as proof of (((u a) ((n b) c)) U) % Found (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U))) as proof of ((a U)->(((u a) ((n b) c)) U)) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found x2:(a U) % Found (fun (x2:(a U))=> x2) as proof of (a U) % Found (fun (x2:(a U))=> x2) as proof of ((a U)->(a U)) % Found x2:(a U) % Found (fun (x2:(a U))=> x2) as proof of (a U) % Found (fun (x2:(a U))=> x2) as proof of ((a U)->(a U)) % Found x2:(a U) % Found (fun (x2:(a U))=> x2) as proof of (a U) % Found (fun (x2:(a U))=> x2) as proof of ((a U)->(a U)) % Found x2:(a U) % Found (fun (x2:(a U))=> x2) as proof of (a U) % Found (fun (x2:(a U))=> x2) as proof of ((a U)->(a U)) % Found x2:(a U) % Found (fun (x2:(a U))=> x2) as proof of (a U) % Found (fun (x2:(a U))=> x2) as proof of ((a U)->(a U)) % Found x2:(a U) % Found (fun (x2:(a U))=> x2) as proof of (a U) % Found (fun (x2:(a U))=> x2) as proof of ((a U)->(a U)) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_introl000:=(or_introl00 (((n b) c) U)):((or (a U)) (((n b) c) U)) % Found (or_introl00 (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found ((fun (B:Prop)=> ((or_introl0 B) x2)) (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U))) as proof of (((u a) ((n b) c)) U) % Found (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U))) as proof of ((a U)->(((u a) ((n b) c)) U)) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_intror00:=(or_intror0 (a U)):((a U)->((or (((n b) c) U)) (a U))) % Found (or_intror0 (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found ((or_intror (((n b) c) U)) (a U)) as proof of ((a U)->((or (((n b) c) U)) (a U))) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_introl000:=(or_introl00 (((n b) c) U)):((or (a U)) (((n b) c) U)) % Found (or_introl00 (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found ((fun (B:Prop)=> ((or_introl0 B) x2)) (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)) as proof of ((or (a U)) (((n b) c) U)) % Found (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U))) as proof of (((u a) ((n b) c)) U) % Found (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U))) as proof of ((a U)->(((u a) ((n b) c)) U)) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_introl00:=(or_introl0 (((n b) c) U)):((a U)->((or (a U)) (((n b) c) U))) % Found (or_introl0 (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found ((or_introl (a U)) (((n b) c) U)) as proof of ((a U)->((or (a U)) (((n b) c) U))) % Found or_introl000:=(or_introl00 (b U)):((or (a U)) (b U)) % Found (or_introl00 (b U)) as proof of ((or (a U)) (b U)) % Found ((fun (B:Prop)=> ((or_introl0 B) x0)) (b U)) as proof of ((or (a U)) (b U)) % Found ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (b U)) as proof of ((or (a U)) (b U)) % Found ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (b U)) as proof of ((or (a U)) (b U)) % Found ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (b U)) as proof of (((u a) b) U) % Found or_introl000:=(or_introl00 (c U)):((or (a U)) (c U)) % Found (or_introl00 (c U)) as proof of ((or (a U)) (c U)) % Found ((fun (B:Prop)=> ((or_introl0 B) x0)) (c U)) as proof of ((or (a U)) (c U)) % Found ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (c U)) as proof of ((or (a U)) (c U)) % Found ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (c U)) as proof of ((or (a U)) (c U)) % Found ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (c U)) as proof of (((u a) c) U) % Found ((conj10 ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (b U))) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (c U))) as proof of ((and (((u a) b) U)) (((u a) c) U)) % Found (((conj1 (((u a) c) U)) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (b U))) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (c U))) as proof of ((and (((u a) b) U)) (((u a) c) U)) % Found ((((conj (((u a) b) U)) (((u a) c) U)) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (b U))) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (c U))) as proof of ((and (((u a) b) U)) (((u a) c) U)) % Found (fun (x0:(a U))=> ((((conj (((u a) b) U)) (((u a) c) U)) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (b U))) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (c U)))) as proof of ((and (((u a) b) U)) (((u a) c) U)) % Found (fun (x0:(a U))=> ((((conj (((u a) b) U)) (((u a) c) U)) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (b U))) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (c U)))) as proof of ((a U)->((and (((u a) b) U)) (((u a) c) U))) % Found or_intror00:=(or_intror0 (c U)):((c U)->((or (a U)) (c U))) % Found (or_intror0 (c U)) as proof of ((c U)->((or (a U)) (c U))) % Found ((or_intror (a U)) (c U)) as proof of ((c U)->((or (a U)) (c U))) % Found (fun (x1:(b U))=> ((or_intror (a U)) (c U))) as proof of ((c U)->((or (a U)) (c U))) % Found (fun (x1:(b U))=> ((or_intror (a U)) (c U))) as proof of ((b U)->((c U)->((or (a U)) (c U)))) % Found (and_rect00 (fun (x1:(b U))=> ((or_intror (a U)) (c U)))) as proof of ((or (a U)) (c U)) % Found ((and_rect0 ((or (a U)) (c U))) (fun (x1:(b U))=> ((or_intror (a U)) (c U)))) as proof of ((or (a U)) (c U)) % Found (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) ((or (a U)) (c U))) (fun (x1:(b U))=> ((or_intror (a U)) (c U)))) as proof of ((or (a U)) (c U)) % Found (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) ((or (a U)) (c U))) (fun (x1:(b U))=> ((or_intror (a U)) (c U)))) as proof of ((or (a U)) (c U)) % Found (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) ((or (a U)) (c U))) (fun (x1:(b U))=> ((or_intror (a U)) (c U)))) as proof of (((u a) c) U) % Found or_intror000:=(or_intror00 x1):((or (a U)) (b U)) % Found (or_intror00 x1) as proof of ((or (a U)) (b U)) % Found ((or_intror0 (b U)) x1) as proof of ((or (a U)) (b U)) % Found (((or_intror (a U)) (b U)) x1) as proof of ((or (a U)) (b U)) % Found (((or_intror (a U)) (b U)) x1) as proof of ((or (a U)) (b U)) % Found (fun (x2:(c U))=> (((or_intror (a U)) (b U)) x1)) as proof of (((u a) b) U) % Found (fun (x1:(b U)) (x2:(c U))=> (((or_intror (a U)) (b U)) x1)) as proof of ((c U)->(((u a) b) U)) % Found (fun (x1:(b U)) (x2:(c U))=> (((or_intror (a U)) (b U)) x1)) as proof of ((b U)->((c U)->(((u a) b) U))) % Found (and_rect00 (fun (x1:(b U)) (x2:(c U))=> (((or_intror (a U)) (b U)) x1))) as proof of (((u a) b) U) % Found ((and_rect0 (((u a) b) U)) (fun (x1:(b U)) (x2:(c U))=> (((or_intror (a U)) (b U)) x1))) as proof of (((u a) b) U) % Found (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) (((u a) b) U)) (fun (x1:(b U)) (x2:(c U))=> (((or_intror (a U)) (b U)) x1))) as proof of (((u a) b) U) % Found (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) (((u a) b) U)) (fun (x1:(b U)) (x2:(c U))=> (((or_intror (a U)) (b U)) x1))) as proof of (((u a) b) U) % Found ((conj10 (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) (((u a) b) U)) (fun (x1:(b U)) (x2:(c U))=> (((or_intror (a U)) (b U)) x1)))) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) ((or (a U)) (c U))) (fun (x1:(b U))=> ((or_intror (a U)) (c U))))) as proof of ((and (((u a) b) U)) (((u a) c) U)) % Found (((conj1 (((u a) c) U)) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) (((u a) b) U)) (fun (x1:(b U)) (x2:(c U))=> (((or_intror (a U)) (b U)) x1)))) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) ((or (a U)) (c U))) (fun (x1:(b U))=> ((or_intror (a U)) (c U))))) as proof of ((and (((u a) b) U)) (((u a) c) U)) % Found ((((conj (((u a) b) U)) (((u a) c) U)) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) (((u a) b) U)) (fun (x1:(b U)) (x2:(c U))=> (((or_intror (a U)) (b U)) x1)))) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) ((or (a U)) (c U))) (fun (x1:(b U))=> ((or_intror (a U)) (c U))))) as proof of ((and (((u a) b) U)) (((u a) c) U)) % Found (fun (x0:(((n b) c) U))=> ((((conj (((u a) b) U)) (((u a) c) U)) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) (((u a) b) U)) (fun (x1:(b U)) (x2:(c U))=> (((or_intror (a U)) (b U)) x1)))) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) ((or (a U)) (c U))) (fun (x1:(b U))=> ((or_intror (a U)) (c U)))))) as proof of ((and (((u a) b) U)) (((u a) c) U)) % Found (fun (x0:(((n b) c) U))=> ((((conj (((u a) b) U)) (((u a) c) U)) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) (((u a) b) U)) (fun (x1:(b U)) (x2:(c U))=> (((or_intror (a U)) (b U)) x1)))) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) ((or (a U)) (c U))) (fun (x1:(b U))=> ((or_intror (a U)) (c U)))))) as proof of ((((n b) c) U)->((and (((u a) b) U)) (((u a) c) U))) % Found ((or_ind00 (fun (x0:(a U))=> ((((conj (((u a) b) U)) (((u a) c) U)) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (b U))) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (c U))))) (fun (x0:(((n b) c) U))=> ((((conj (((u a) b) U)) (((u a) c) U)) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) (((u a) b) U)) (fun (x1:(b U)) (x2:(c U))=> (((or_intror (a U)) (b U)) x1)))) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) ((or (a U)) (c U))) (fun (x1:(b U))=> ((or_intror (a U)) (c U))))))) as proof of ((and (((u a) b) U)) (((u a) c) U)) % Found (((or_ind0 ((and (((u a) b) U)) (((u a) c) U))) (fun (x0:(a U))=> ((((conj (((u a) b) U)) (((u a) c) U)) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (b U))) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (c U))))) (fun (x0:(((n b) c) U))=> ((((conj (((u a) b) U)) (((u a) c) U)) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) (((u a) b) U)) (fun (x1:(b U)) (x2:(c U))=> (((or_intror (a U)) (b U)) x1)))) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) ((or (a U)) (c U))) (fun (x1:(b U))=> ((or_intror (a U)) (c U))))))) as proof of ((and (((u a) b) U)) (((u a) c) U)) % Found ((((fun (P:Prop) (x0:((a U)->P)) (x1:((((n b) c) U)->P))=> ((((((or_ind (a U)) (((n b) c) U)) P) x0) x1) x)) ((and (((u a) b) U)) (((u a) c) U))) (fun (x0:(a U))=> ((((conj (((u a) b) U)) (((u a) c) U)) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (b U))) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (c U))))) (fun (x0:(((n b) c) U))=> ((((conj (((u a) b) U)) (((u a) c) U)) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) (((u a) b) U)) (fun (x1:(b U)) (x2:(c U))=> (((or_intror (a U)) (b U)) x1)))) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) ((or (a U)) (c U))) (fun (x1:(b U))=> ((or_intror (a U)) (c U))))))) as proof of ((and (((u a) b) U)) (((u a) c) U)) % Found ((((fun (P:Prop) (x0:((a U)->P)) (x1:((((n b) c) U)->P))=> ((((((or_ind (a U)) (((n b) c) U)) P) x0) x1) x)) ((and (((u a) b) U)) (((u a) c) U))) (fun (x0:(a U))=> ((((conj (((u a) b) U)) (((u a) c) U)) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (b U))) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (c U))))) (fun (x0:(((n b) c) U))=> ((((conj (((u a) b) U)) (((u a) c) U)) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) (((u a) b) U)) (fun (x1:(b U)) (x2:(c U))=> (((or_intror (a U)) (b U)) x1)))) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) ((or (a U)) (c U))) (fun (x1:(b U))=> ((or_intror (a U)) (c U))))))) as proof of ((and (((u a) b) U)) (((u a) c) U)) % Found (fun (x:(((u a) ((n b) c)) U))=> ((((fun (P:Prop) (x0:((a U)->P)) (x1:((((n b) c) U)->P))=> ((((((or_ind (a U)) (((n b) c) U)) P) x0) x1) x)) ((and (((u a) b) U)) (((u a) c) U))) (fun (x0:(a U))=> ((((conj (((u a) b) U)) (((u a) c) U)) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (b U))) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (c U))))) (fun (x0:(((n b) c) U))=> ((((conj (((u a) b) U)) (((u a) c) U)) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) (((u a) b) U)) (fun (x1:(b U)) (x2:(c U))=> (((or_intror (a U)) (b U)) x1)))) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) ((or (a U)) (c U))) (fun (x1:(b U))=> ((or_intror (a U)) (c U)))))))) as proof of (((n ((u a) b)) ((u a) c)) U) % Found (fun (x:(((u a) ((n b) c)) U))=> ((((fun (P:Prop) (x0:((a U)->P)) (x1:((((n b) c) U)->P))=> ((((((or_ind (a U)) (((n b) c) U)) P) x0) x1) x)) ((and (((u a) b) U)) (((u a) c) U))) (fun (x0:(a U))=> ((((conj (((u a) b) U)) (((u a) c) U)) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (b U))) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (c U))))) (fun (x0:(((n b) c) U))=> ((((conj (((u a) b) U)) (((u a) c) U)) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) (((u a) b) U)) (fun (x1:(b U)) (x2:(c U))=> (((or_intror (a U)) (b U)) x1)))) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) ((or (a U)) (c U))) (fun (x1:(b U))=> ((or_intror (a U)) (c U)))))))) as proof of ((((u a) ((n b) c)) U)->(((n ((u a) b)) ((u a) c)) U)) % Found x2:(c U) % Found x2 as proof of (c U) % Found x2:(b U) % Found x2 as proof of (b U) % Found x2:(c U) % Found x2 as proof of (c U) % Found x2:(c U) % Found x2 as proof of (c U) % Found x2:(b U) % Found x2 as proof of (b U) % Found x2:(b U) % Found x2 as proof of (b U) % Found conj1000:=(conj100 x3):((and (b U)) (c U)) % Found (conj100 x3) as proof of ((and (b U)) (c U)) % Found ((conj10 (c U)) x3) as proof of ((and (b U)) (c U)) % Found (((fun (B:Prop)=> ((conj1 B) x2)) (c U)) x3) as proof of ((and (b U)) (c U)) % Found (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3) as proof of ((and (b U)) (c U)) % Found (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3) as proof of ((and (b U)) (c U)) % Found (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3) as proof of (((n b) c) U) % Found (or_intror00 (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3)) as proof of ((or (a U)) (((n b) c) U)) % Found ((or_intror0 (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3)) as proof of ((or (a U)) (((n b) c) U)) % Found (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3)) as proof of ((or (a U)) (((n b) c) U)) % Found (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3)) as proof of ((or (a U)) (((n b) c) U)) % Found (fun (x3:(c U))=> (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3))) as proof of (((u a) ((n b) c)) U) % Found (fun (x3:(c U))=> (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3))) as proof of ((c U)->(((u a) ((n b) c)) U)) % Found ((or_ind10 (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)))) (fun (x3:(c U))=> (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3)))) as proof of (((u a) ((n b) c)) U) % Found (((or_ind1 (((u a) ((n b) c)) U)) (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)))) (fun (x3:(c U))=> (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3)))) as proof of (((u a) ((n b) c)) U) % Found ((((fun (P:Prop) (x3:((a U)->P)) (x4:((c U)->P))=> ((((((or_ind (a U)) (c U)) P) x3) x4) x1)) (((u a) ((n b) c)) U)) (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)))) (fun (x3:(c U))=> (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3)))) as proof of (((u a) ((n b) c)) U) % Found (fun (x2:(b U))=> ((((fun (P:Prop) (x3:((a U)->P)) (x4:((c U)->P))=> ((((((or_ind (a U)) (c U)) P) x3) x4) x1)) (((u a) ((n b) c)) U)) (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)))) (fun (x3:(c U))=> (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3))))) as proof of (((u a) ((n b) c)) U) % Found (fun (x2:(b U))=> ((((fun (P:Prop) (x3:((a U)->P)) (x4:((c U)->P))=> ((((((or_ind (a U)) (c U)) P) x3) x4) x1)) (((u a) ((n b) c)) U)) (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)))) (fun (x3:(c U))=> (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3))))) as proof of ((b U)->(((u a) ((n b) c)) U)) % Found ((or_ind00 (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)))) (fun (x2:(b U))=> ((((fun (P:Prop) (x3:((a U)->P)) (x4:((c U)->P))=> ((((((or_ind (a U)) (c U)) P) x3) x4) x1)) (((u a) ((n b) c)) U)) (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)))) (fun (x3:(c U))=> (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3)))))) as proof of (((u a) ((n b) c)) U) % Found (((or_ind0 (((u a) ((n b) c)) U)) (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)))) (fun (x2:(b U))=> ((((fun (P:Prop) (x3:((a U)->P)) (x4:((c U)->P))=> ((((((or_ind (a U)) (c U)) P) x3) x4) x1)) (((u a) ((n b) c)) U)) (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)))) (fun (x3:(c U))=> (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3)))))) as proof of (((u a) ((n b) c)) U) % Found ((((fun (P:Prop) (x2:((a U)->P)) (x3:((b U)->P))=> ((((((or_ind (a U)) (b U)) P) x2) x3) x0)) (((u a) ((n b) c)) U)) (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)))) (fun (x2:(b U))=> ((((fun (P:Prop) (x3:((a U)->P)) (x4:((c U)->P))=> ((((((or_ind (a U)) (c U)) P) x3) x4) x1)) (((u a) ((n b) c)) U)) (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)))) (fun (x3:(c U))=> (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3)))))) as proof of (((u a) ((n b) c)) U) % Found (fun (x1:(((u a) c) U))=> ((((fun (P:Prop) (x2:((a U)->P)) (x3:((b U)->P))=> ((((((or_ind (a U)) (b U)) P) x2) x3) x0)) (((u a) ((n b) c)) U)) (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)))) (fun (x2:(b U))=> ((((fun (P:Prop) (x3:((a U)->P)) (x4:((c U)->P))=> ((((((or_ind (a U)) (c U)) P) x3) x4) x1)) (((u a) ((n b) c)) U)) (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)))) (fun (x3:(c U))=> (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3))))))) as proof of (((u a) ((n b) c)) U) % Found (fun (x0:(((u a) b) U)) (x1:(((u a) c) U))=> ((((fun (P:Prop) (x2:((a U)->P)) (x3:((b U)->P))=> ((((((or_ind (a U)) (b U)) P) x2) x3) x0)) (((u a) ((n b) c)) U)) (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)))) (fun (x2:(b U))=> ((((fun (P:Prop) (x3:((a U)->P)) (x4:((c U)->P))=> ((((((or_ind (a U)) (c U)) P) x3) x4) x1)) (((u a) ((n b) c)) U)) (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)))) (fun (x3:(c U))=> (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3))))))) as proof of ((((u a) c) U)->(((u a) ((n b) c)) U)) % Found (fun (x0:(((u a) b) U)) (x1:(((u a) c) U))=> ((((fun (P:Prop) (x2:((a U)->P)) (x3:((b U)->P))=> ((((((or_ind (a U)) (b U)) P) x2) x3) x0)) (((u a) ((n b) c)) U)) (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)))) (fun (x2:(b U))=> ((((fun (P:Prop) (x3:((a U)->P)) (x4:((c U)->P))=> ((((((or_ind (a U)) (c U)) P) x3) x4) x1)) (((u a) ((n b) c)) U)) (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)))) (fun (x3:(c U))=> (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3))))))) as proof of ((((u a) b) U)->((((u a) c) U)->(((u a) ((n b) c)) U))) % Found (and_rect00 (fun (x0:(((u a) b) U)) (x1:(((u a) c) U))=> ((((fun (P:Prop) (x2:((a U)->P)) (x3:((b U)->P))=> ((((((or_ind (a U)) (b U)) P) x2) x3) x0)) (((u a) ((n b) c)) U)) (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)))) (fun (x2:(b U))=> ((((fun (P:Prop) (x3:((a U)->P)) (x4:((c U)->P))=> ((((((or_ind (a U)) (c U)) P) x3) x4) x1)) (((u a) ((n b) c)) U)) (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)))) (fun (x3:(c U))=> (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3)))))))) as proof of (((u a) ((n b) c)) U) % Found ((and_rect0 (((u a) ((n b) c)) U)) (fun (x0:(((u a) b) U)) (x1:(((u a) c) U))=> ((((fun (P:Prop) (x2:((a U)->P)) (x3:((b U)->P))=> ((((((or_ind (a U)) (b U)) P) x2) x3) x0)) (((u a) ((n b) c)) U)) (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)))) (fun (x2:(b U))=> ((((fun (P:Prop) (x3:((a U)->P)) (x4:((c U)->P))=> ((((((or_ind (a U)) (c U)) P) x3) x4) x1)) (((u a) ((n b) c)) U)) (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)))) (fun (x3:(c U))=> (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3)))))))) as proof of (((u a) ((n b) c)) U) % Found (((fun (P:Type) (x0:((((u a) b) U)->((((u a) c) U)->P)))=> (((((and_rect (((u a) b) U)) (((u a) c) U)) P) x0) x)) (((u a) ((n b) c)) U)) (fun (x0:(((u a) b) U)) (x1:(((u a) c) U))=> ((((fun (P:Prop) (x2:((a U)->P)) (x3:((b U)->P))=> ((((((or_ind (a U)) (b U)) P) x2) x3) x0)) (((u a) ((n b) c)) U)) (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)))) (fun (x2:(b U))=> ((((fun (P:Prop) (x3:((a U)->P)) (x4:((c U)->P))=> ((((((or_ind (a U)) (c U)) P) x3) x4) x1)) (((u a) ((n b) c)) U)) (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)))) (fun (x3:(c U))=> (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3)))))))) as proof of (((u a) ((n b) c)) U) % Found (fun (x:(((n ((u a) b)) ((u a) c)) U))=> (((fun (P:Type) (x0:((((u a) b) U)->((((u a) c) U)->P)))=> (((((and_rect (((u a) b) U)) (((u a) c) U)) P) x0) x)) (((u a) ((n b) c)) U)) (fun (x0:(((u a) b) U)) (x1:(((u a) c) U))=> ((((fun (P:Prop) (x2:((a U)->P)) (x3:((b U)->P))=> ((((((or_ind (a U)) (b U)) P) x2) x3) x0)) (((u a) ((n b) c)) U)) (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)))) (fun (x2:(b U))=> ((((fun (P:Prop) (x3:((a U)->P)) (x4:((c U)->P))=> ((((((or_ind (a U)) (c U)) P) x3) x4) x1)) (((u a) ((n b) c)) U)) (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)))) (fun (x3:(c U))=> (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3))))))))) as proof of (((u a) ((n b) c)) U) % Found (fun (x:(((n ((u a) b)) ((u a) c)) U))=> (((fun (P:Type) (x0:((((u a) b) U)->((((u a) c) U)->P)))=> (((((and_rect (((u a) b) U)) (((u a) c) U)) P) x0) x)) (((u a) ((n b) c)) U)) (fun (x0:(((u a) b) U)) (x1:(((u a) c) U))=> ((((fun (P:Prop) (x2:((a U)->P)) (x3:((b U)->P))=> ((((((or_ind (a U)) (b U)) P) x2) x3) x0)) (((u a) ((n b) c)) U)) (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)))) (fun (x2:(b U))=> ((((fun (P:Prop) (x3:((a U)->P)) (x4:((c U)->P))=> ((((((or_ind (a U)) (c U)) P) x3) x4) x1)) (((u a) ((n b) c)) U)) (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)))) (fun (x3:(c U))=> (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3))))))))) as proof of ((((n ((u a) b)) ((u a) c)) U)->(((u a) ((n b) c)) U)) % Found ((conj00 (fun (x:(((u a) ((n b) c)) U))=> ((((fun (P:Prop) (x0:((a U)->P)) (x1:((((n b) c) U)->P))=> ((((((or_ind (a U)) (((n b) c) U)) P) x0) x1) x)) ((and (((u a) b) U)) (((u a) c) U))) (fun (x0:(a U))=> ((((conj (((u a) b) U)) (((u a) c) U)) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (b U))) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (c U))))) (fun (x0:(((n b) c) U))=> ((((conj (((u a) b) U)) (((u a) c) U)) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) (((u a) b) U)) (fun (x1:(b U)) (x2:(c U))=> (((or_intror (a U)) (b U)) x1)))) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) ((or (a U)) (c U))) (fun (x1:(b U))=> ((or_intror (a U)) (c U))))))))) (fun (x:(((n ((u a) b)) ((u a) c)) U))=> (((fun (P:Type) (x0:((((u a) b) U)->((((u a) c) U)->P)))=> (((((and_rect (((u a) b) U)) (((u a) c) U)) P) x0) x)) (((u a) ((n b) c)) U)) (fun (x0:(((u a) b) U)) (x1:(((u a) c) U))=> ((((fun (P:Prop) (x2:((a U)->P)) (x3:((b U)->P))=> ((((((or_ind (a U)) (b U)) P) x2) x3) x0)) (((u a) ((n b) c)) U)) (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)))) (fun (x2:(b U))=> ((((fun (P:Prop) (x3:((a U)->P)) (x4:((c U)->P))=> ((((((or_ind (a U)) (c U)) P) x3) x4) x1)) (((u a) ((n b) c)) U)) (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)))) (fun (x3:(c U))=> (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3)))))))))) as proof of ((and ((((u a) ((n b) c)) U)->(((n ((u a) b)) ((u a) c)) U))) ((((n ((u a) b)) ((u a) c)) U)->(((u a) ((n b) c)) U))) % Found (((conj0 ((((n ((u a) b)) ((u a) c)) U)->(((u a) ((n b) c)) U))) (fun (x:(((u a) ((n b) c)) U))=> ((((fun (P:Prop) (x0:((a U)->P)) (x1:((((n b) c) U)->P))=> ((((((or_ind (a U)) (((n b) c) U)) P) x0) x1) x)) ((and (((u a) b) U)) (((u a) c) U))) (fun (x0:(a U))=> ((((conj (((u a) b) U)) (((u a) c) U)) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (b U))) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (c U))))) (fun (x0:(((n b) c) U))=> ((((conj (((u a) b) U)) (((u a) c) U)) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) (((u a) b) U)) (fun (x1:(b U)) (x2:(c U))=> (((or_intror (a U)) (b U)) x1)))) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) ((or (a U)) (c U))) (fun (x1:(b U))=> ((or_intror (a U)) (c U))))))))) (fun (x:(((n ((u a) b)) ((u a) c)) U))=> (((fun (P:Type) (x0:((((u a) b) U)->((((u a) c) U)->P)))=> (((((and_rect (((u a) b) U)) (((u a) c) U)) P) x0) x)) (((u a) ((n b) c)) U)) (fun (x0:(((u a) b) U)) (x1:(((u a) c) U))=> ((((fun (P:Prop) (x2:((a U)->P)) (x3:((b U)->P))=> ((((((or_ind (a U)) (b U)) P) x2) x3) x0)) (((u a) ((n b) c)) U)) (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)))) (fun (x2:(b U))=> ((((fun (P:Prop) (x3:((a U)->P)) (x4:((c U)->P))=> ((((((or_ind (a U)) (c U)) P) x3) x4) x1)) (((u a) ((n b) c)) U)) (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)))) (fun (x3:(c U))=> (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3)))))))))) as proof of ((and ((((u a) ((n b) c)) U)->(((n ((u a) b)) ((u a) c)) U))) ((((n ((u a) b)) ((u a) c)) U)->(((u a) ((n b) c)) U))) % Found ((((conj ((((u a) ((n b) c)) U)->(((n ((u a) b)) ((u a) c)) U))) ((((n ((u a) b)) ((u a) c)) U)->(((u a) ((n b) c)) U))) (fun (x:(((u a) ((n b) c)) U))=> ((((fun (P:Prop) (x0:((a U)->P)) (x1:((((n b) c) U)->P))=> ((((((or_ind (a U)) (((n b) c) U)) P) x0) x1) x)) ((and (((u a) b) U)) (((u a) c) U))) (fun (x0:(a U))=> ((((conj (((u a) b) U)) (((u a) c) U)) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (b U))) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (c U))))) (fun (x0:(((n b) c) U))=> ((((conj (((u a) b) U)) (((u a) c) U)) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) (((u a) b) U)) (fun (x1:(b U)) (x2:(c U))=> (((or_intror (a U)) (b U)) x1)))) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) ((or (a U)) (c U))) (fun (x1:(b U))=> ((or_intror (a U)) (c U))))))))) (fun (x:(((n ((u a) b)) ((u a) c)) U))=> (((fun (P:Type) (x0:((((u a) b) U)->((((u a) c) U)->P)))=> (((((and_rect (((u a) b) U)) (((u a) c) U)) P) x0) x)) (((u a) ((n b) c)) U)) (fun (x0:(((u a) b) U)) (x1:(((u a) c) U))=> ((((fun (P:Prop) (x2:((a U)->P)) (x3:((b U)->P))=> ((((((or_ind (a U)) (b U)) P) x2) x3) x0)) (((u a) ((n b) c)) U)) (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)))) (fun (x2:(b U))=> ((((fun (P:Prop) (x3:((a U)->P)) (x4:((c U)->P))=> ((((((or_ind (a U)) (c U)) P) x3) x4) x1)) (((u a) ((n b) c)) U)) (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)))) (fun (x3:(c U))=> (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3)))))))))) as proof of ((and ((((u a) ((n b) c)) U)->(((n ((u a) b)) ((u a) c)) U))) ((((n ((u a) b)) ((u a) c)) U)->(((u a) ((n b) c)) U))) % Found ((((conj ((((u a) ((n b) c)) U)->(((n ((u a) b)) ((u a) c)) U))) ((((n ((u a) b)) ((u a) c)) U)->(((u a) ((n b) c)) U))) (fun (x:(((u a) ((n b) c)) U))=> ((((fun (P:Prop) (x0:((a U)->P)) (x1:((((n b) c) U)->P))=> ((((((or_ind (a U)) (((n b) c) U)) P) x0) x1) x)) ((and (((u a) b) U)) (((u a) c) U))) (fun (x0:(a U))=> ((((conj (((u a) b) U)) (((u a) c) U)) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (b U))) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (c U))))) (fun (x0:(((n b) c) U))=> ((((conj (((u a) b) U)) (((u a) c) U)) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) (((u a) b) U)) (fun (x1:(b U)) (x2:(c U))=> (((or_intror (a U)) (b U)) x1)))) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) ((or (a U)) (c U))) (fun (x1:(b U))=> ((or_intror (a U)) (c U))))))))) (fun (x:(((n ((u a) b)) ((u a) c)) U))=> (((fun (P:Type) (x0:((((u a) b) U)->((((u a) c) U)->P)))=> (((((and_rect (((u a) b) U)) (((u a) c) U)) P) x0) x)) (((u a) ((n b) c)) U)) (fun (x0:(((u a) b) U)) (x1:(((u a) c) U))=> ((((fun (P:Prop) (x2:((a U)->P)) (x3:((b U)->P))=> ((((((or_ind (a U)) (b U)) P) x2) x3) x0)) (((u a) ((n b) c)) U)) (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)))) (fun (x2:(b U))=> ((((fun (P:Prop) (x3:((a U)->P)) (x4:((c U)->P))=> ((((((or_ind (a U)) (c U)) P) x3) x4) x1)) (((u a) ((n b) c)) U)) (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)))) (fun (x3:(c U))=> (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3)))))))))) as proof of ((and ((((u a) ((n b) c)) U)->(((n ((u a) b)) ((u a) c)) U))) ((((n ((u a) b)) ((u a) c)) U)->(((u a) ((n b) c)) U))) % Found (fun (U:fofType)=> ((((conj ((((u a) ((n b) c)) U)->(((n ((u a) b)) ((u a) c)) U))) ((((n ((u a) b)) ((u a) c)) U)->(((u a) ((n b) c)) U))) (fun (x:(((u a) ((n b) c)) U))=> ((((fun (P:Prop) (x0:((a U)->P)) (x1:((((n b) c) U)->P))=> ((((((or_ind (a U)) (((n b) c) U)) P) x0) x1) x)) ((and (((u a) b) U)) (((u a) c) U))) (fun (x0:(a U))=> ((((conj (((u a) b) U)) (((u a) c) U)) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (b U))) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (c U))))) (fun (x0:(((n b) c) U))=> ((((conj (((u a) b) U)) (((u a) c) U)) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) (((u a) b) U)) (fun (x1:(b U)) (x2:(c U))=> (((or_intror (a U)) (b U)) x1)))) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) ((or (a U)) (c U))) (fun (x1:(b U))=> ((or_intror (a U)) (c U))))))))) (fun (x:(((n ((u a) b)) ((u a) c)) U))=> (((fun (P:Type) (x0:((((u a) b) U)->((((u a) c) U)->P)))=> (((((and_rect (((u a) b) U)) (((u a) c) U)) P) x0) x)) (((u a) ((n b) c)) U)) (fun (x0:(((u a) b) U)) (x1:(((u a) c) U))=> ((((fun (P:Prop) (x2:((a U)->P)) (x3:((b U)->P))=> ((((((or_ind (a U)) (b U)) P) x2) x3) x0)) (((u a) ((n b) c)) U)) (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)))) (fun (x2:(b U))=> ((((fun (P:Prop) (x3:((a U)->P)) (x4:((c U)->P))=> ((((((or_ind (a U)) (c U)) P) x3) x4) x1)) (((u a) ((n b) c)) U)) (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)))) (fun (x3:(c U))=> (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3))))))))))) as proof of ((iff (((u a) ((n b) c)) U)) (((n ((u a) b)) ((u a) c)) U)) % Found (fun (U:fofType)=> ((((conj ((((u a) ((n b) c)) U)->(((n ((u a) b)) ((u a) c)) U))) ((((n ((u a) b)) ((u a) c)) U)->(((u a) ((n b) c)) U))) (fun (x:(((u a) ((n b) c)) U))=> ((((fun (P:Prop) (x0:((a U)->P)) (x1:((((n b) c) U)->P))=> ((((((or_ind (a U)) (((n b) c) U)) P) x0) x1) x)) ((and (((u a) b) U)) (((u a) c) U))) (fun (x0:(a U))=> ((((conj (((u a) b) U)) (((u a) c) U)) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (b U))) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (c U))))) (fun (x0:(((n b) c) U))=> ((((conj (((u a) b) U)) (((u a) c) U)) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) (((u a) b) U)) (fun (x1:(b U)) (x2:(c U))=> (((or_intror (a U)) (b U)) x1)))) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) ((or (a U)) (c U))) (fun (x1:(b U))=> ((or_intror (a U)) (c U))))))))) (fun (x:(((n ((u a) b)) ((u a) c)) U))=> (((fun (P:Type) (x0:((((u a) b) U)->((((u a) c) U)->P)))=> (((((and_rect (((u a) b) U)) (((u a) c) U)) P) x0) x)) (((u a) ((n b) c)) U)) (fun (x0:(((u a) b) U)) (x1:(((u a) c) U))=> ((((fun (P:Prop) (x2:((a U)->P)) (x3:((b U)->P))=> ((((((or_ind (a U)) (b U)) P) x2) x3) x0)) (((u a) ((n b) c)) U)) (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)))) (fun (x2:(b U))=> ((((fun (P:Prop) (x3:((a U)->P)) (x4:((c U)->P))=> ((((((or_ind (a U)) (c U)) P) x3) x4) x1)) (((u a) ((n b) c)) U)) (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)))) (fun (x3:(c U))=> (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3))))))))))) as proof of ((seteq ((u a) ((n b) c))) ((n ((u a) b)) ((u a) c))) % Got proof (fun (U:fofType)=> ((((conj ((((u a) ((n b) c)) U)->(((n ((u a) b)) ((u a) c)) U))) ((((n ((u a) b)) ((u a) c)) U)->(((u a) ((n b) c)) U))) (fun (x:(((u a) ((n b) c)) U))=> ((((fun (P:Prop) (x0:((a U)->P)) (x1:((((n b) c) U)->P))=> ((((((or_ind (a U)) (((n b) c) U)) P) x0) x1) x)) ((and (((u a) b) U)) (((u a) c) U))) (fun (x0:(a U))=> ((((conj (((u a) b) U)) (((u a) c) U)) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (b U))) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (c U))))) (fun (x0:(((n b) c) U))=> ((((conj (((u a) b) U)) (((u a) c) U)) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) (((u a) b) U)) (fun (x1:(b U)) (x2:(c U))=> (((or_intror (a U)) (b U)) x1)))) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) ((or (a U)) (c U))) (fun (x1:(b U))=> ((or_intror (a U)) (c U))))))))) (fun (x:(((n ((u a) b)) ((u a) c)) U))=> (((fun (P:Type) (x0:((((u a) b) U)->((((u a) c) U)->P)))=> (((((and_rect (((u a) b) U)) (((u a) c) U)) P) x0) x)) (((u a) ((n b) c)) U)) (fun (x0:(((u a) b) U)) (x1:(((u a) c) U))=> ((((fun (P:Prop) (x2:((a U)->P)) (x3:((b U)->P))=> ((((((or_ind (a U)) (b U)) P) x2) x3) x0)) (((u a) ((n b) c)) U)) (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)))) (fun (x2:(b U))=> ((((fun (P:Prop) (x3:((a U)->P)) (x4:((c U)->P))=> ((((((or_ind (a U)) (c U)) P) x3) x4) x1)) (((u a) ((n b) c)) U)) (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)))) (fun (x3:(c U))=> (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3))))))))))) % Time elapsed = 30.557922s % node=4903 cost=4904.000000 depth=33 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % (fun (U:fofType)=> ((((conj ((((u a) ((n b) c)) U)->(((n ((u a) b)) ((u a) c)) U))) ((((n ((u a) b)) ((u a) c)) U)->(((u a) ((n b) c)) U))) (fun (x:(((u a) ((n b) c)) U))=> ((((fun (P:Prop) (x0:((a U)->P)) (x1:((((n b) c) U)->P))=> ((((((or_ind (a U)) (((n b) c) U)) P) x0) x1) x)) ((and (((u a) b) U)) (((u a) c) U))) (fun (x0:(a U))=> ((((conj (((u a) b) U)) (((u a) c) U)) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (b U))) ((fun (B:Prop)=> (((or_introl (a U)) B) x0)) (c U))))) (fun (x0:(((n b) c) U))=> ((((conj (((u a) b) U)) (((u a) c) U)) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) (((u a) b) U)) (fun (x1:(b U)) (x2:(c U))=> (((or_intror (a U)) (b U)) x1)))) (((fun (P:Type) (x1:((b U)->((c U)->P)))=> (((((and_rect (b U)) (c U)) P) x1) x0)) ((or (a U)) (c U))) (fun (x1:(b U))=> ((or_intror (a U)) (c U))))))))) (fun (x:(((n ((u a) b)) ((u a) c)) U))=> (((fun (P:Type) (x0:((((u a) b) U)->((((u a) c) U)->P)))=> (((((and_rect (((u a) b) U)) (((u a) c) U)) P) x0) x)) (((u a) ((n b) c)) U)) (fun (x0:(((u a) b) U)) (x1:(((u a) c) U))=> ((((fun (P:Prop) (x2:((a U)->P)) (x3:((b U)->P))=> ((((((or_ind (a U)) (b U)) P) x2) x3) x0)) (((u a) ((n b) c)) U)) (fun (x2:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x2)) (((n b) c) U)))) (fun (x2:(b U))=> ((((fun (P:Prop) (x3:((a U)->P)) (x4:((c U)->P))=> ((((((or_ind (a U)) (c U)) P) x3) x4) x1)) (((u a) ((n b) c)) U)) (fun (x3:(a U))=> ((fun (B:Prop)=> (((or_introl (a U)) B) x3)) (((n b) c) U)))) (fun (x3:(c U))=> (((or_intror (a U)) (((n b) c) U)) (((fun (B:Prop)=> (((conj (b U)) B) x2)) (c U)) x3))))))))))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------