Can you please invent a name for the term defined by " In Empty."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => x1)."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => x0)."?
Can you please invent a name for the term defined by " binunion omega (Repl omega minus_CSNo)."?
Can you please invent a name for the term defined by " (fun x0 : prop => If_i x0 1 0)."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => ap x1 0)."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => ap x1 3)."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => ap x1 4)."?
Can you please invent a name for the term defined by " pack_b_b_r_e_e real add_SNo mul_SNo SNoLe 0 1."?
Can you please invent a name for the term defined by " (fun x0 : set => forall x1, nIn x1 x0)."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => UPair (UPair x0 x1) (Sing x0))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => UPair (Sing x0) (UPair x0 x1))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => UPair (Sing x0) (UPair x1 x0))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => UPair (UPair x1 x0) (Sing x0))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => UPair (UPair x1 x0) (Sing x1))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => UPair (Sing x1) (UPair x1 x0))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => UPair (Sing x1) (UPair x0 x1))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => UPair (UPair x0 x1) (Sing x1))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => decode_b (ap x1 2))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => decode_b (ap x1 1))."?
Can you please invent a name for the term defined by " (fun x0 : set => lam omega (fun x1 : set => ap x0 (ordsucc x1)))."?
Can you please invent a name for the term defined by " (fun x0 : set -> set => fun x1 : set => x0 (x0 x1))."?
Can you please invent a name for the term defined by " (fun x0 : set -> set => fun x1 : set => x0 (x0 (x0 (x0 x1))))."?
Can you please invent a name for the term defined by " (fun x0 : set => and (struct_u x0) (unpack_u_o x0 (fun x1 : set => inj x1 x1)))."?
Can you please invent a name for the term defined by " (fun x0 : set => and (struct_u x0) (unpack_u_o x0 (fun x1 : set => bij x1 x1)))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (MagmaHom x0 x1 x2) (MagmaHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (MagmaHom x0 x1 x2) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (MagmaHom x0 x1 x2) (BinRelnHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (PtdSetHom x0 x1 x2) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => lam omega (nat_primrec x0 (fun x2 x3 : set => ap x1 x2)))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (BinRelnHom x0 x1 x2) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (MagmaHom x0 x1 x2) (UnaryFuncHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (BinRelnHom x0 x1 x2) (BinRelnHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (MagmaHom x0 x1 x2) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (UnaryFuncHom x0 x1 x2) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (UnaryPredHom x0 x1 x2) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (BinRelnHom x0 x1 x2) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (UnaryFuncHom x0 x1 x2) (BinRelnHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 : set => or (x1 :e x3) (and (x1 = x3) (x0 :e x2)))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 : set => or (x0 :e x2) (and (x0 = x2) (x1 :e x3)))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (PreContinuousHom x0 x1 x2) (MagmaHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (UnaryPredHom x0 x1 x2) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (UnaryFuncHom x0 x1 x2) (UnaryFuncHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (UnaryFuncHom x0 x1 x2) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (PreContinuousHom x0 x1 x2) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (PreContinuousHom x0 x1 x2) (BinRelnHom x0 x1 x2))."?
Can you please invent a name for the term defined by " In_rec_i (fun x0 : set => fun x1 : set -> set => famunion x0 (fun x2 : set => Power (x1 x2)))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (PreContinuousHom x0 x1 x2) (UnaryFuncHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (PreContinuousHom x0 x1 x2) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " Eps_i (fun x0 : set => and (forall x1, x1 :e x0 -> SNo x1) (explicit_Reals x0 0 1 add_SNo mul_SNo SNoLe))."?
Can you please invent a name for the term defined by " (fun x0 : set => not (missingname_acdba35036356b6f3f5277943f93a3d5f62a97e30846e785cd1f436a46fe2472 x0))."?
Can you please invent a name for the term defined by " (fun x0 : set => not (missingname_5adfc97f877949e850303ccf97106d86d5b789a2ef2cf28e8d614e0a469ac80b x0))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => and (and (x1 :e x0) (SNo x1)) (forall x2, x2 :e x0 -> SNo x2 -> SNoLe x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => and (and (x1 :e x0) (SNo x1)) (forall x2, x2 :e x0 -> SNo x2 -> SNoLe x2 x1))."?
Can you please invent a name for the term defined by " (fun x0 : set => forall x1 : set -> set -> prop, x1 x0 (lam omega (ap x0)) -> x1 (lam omega (ap x0)) x0)."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (MagmaHom x0 x1 x2) (MagmaHom x0 x1 x2)) (MagmaHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (MagmaHom x0 x1 x2) (MagmaHom x0 x1 x2)) (BinRelnHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : set => x9)."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : set => x8)."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : set => x7)."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : set => x6)."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : set => x5)."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : set => x4)."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : set => x3)."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : set => x2)."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : set => x1)."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : set => x0)."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (MagmaHom x0 x1 x2) (BinRelnHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 : set => Sep (missingname_7864bcf70cc3cdb856575a33e936cf0af667634490f6123fa1f736ddfe565bcf x0) ordinal)."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (MagmaHom x0 x1 x2) (MagmaHom x0 x1 x2)) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (MagmaHom x0 x1 x2) (MagmaHom x0 x1 x2)) (UnaryFuncHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (BinRelnHom x0 x1 x2) (BinRelnHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (MagmaHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (MagmaHom x0 x1 x2) (UnaryPredHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (MagmaHom x0 x1 x2) (BinRelnHom x0 x1 x2)) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (MagmaHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (BinRelnHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (UnaryFuncHom x0 x1 x2) (BinRelnHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (BinRelnHom x0 x1 x2) (UnaryPredHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 : set => and (RealsStruct_leq x1 x2 x3) (x2 = x3 -> (forall x4 : prop, x4)))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (MagmaHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (BinRelnHom x0 x1 x2) (BinRelnHom x0 x1 x2)) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (UnaryFuncHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (UnaryFuncHom x0 x1 x2) (UnaryPredHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (UnaryPredHom x0 x1 x2) (UnaryPredHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (PreContinuousHom x0 x1 x2) (MagmaHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (UnaryFuncHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (BinRelnHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (PreContinuousHom x0 x1 x2) (MagmaHom x0 x1 x2)) (BinRelnHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (UnaryFuncHom x0 x1 x2) (BinRelnHom x0 x1 x2)) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (PreContinuousHom x0 x1 x2) (BinRelnHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (UnaryFuncHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (PreContinuousHom x0 x1 x2) (MagmaHom x0 x1 x2)) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (PreContinuousHom x0 x1 x2) (MagmaHom x0 x1 x2)) (UnaryFuncHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (PreContinuousHom x0 x1 x2) (UnaryPredHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (PreContinuousHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (PreContinuousHom x0 x1 x2) (BinRelnHom x0 x1 x2)) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (PreContinuousHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (BinRelnHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 : (set -> set) -> set -> set => fun x1 : set -> set => x0 (x0 x1))."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set => x0 0 u1 u2 u3 u4 u5)."?
Can you please invent a name for the term defined by " (fun x0 x1 : set -> set -> set => fun x2 x3 : set => x0 x3 (x1 x2 x3))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set -> set -> set => fun x2 x3 : set => x0 (x1 x2 x3) x3)."?
Can you please invent a name for the term defined by " (fun x0 x1 : set -> set -> set => fun x2 x3 : set => x0 x2 (x1 x2 x3))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (PreContinuousHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => div_SNo (nat_factorial x0) (mul_SNo (nat_factorial (add_SNo x0 (minus_SNo x1))) (nat_factorial x1)))."?
Can you please invent a name for the term defined by " (fun x0 : set => forall x1, x1 :e x0 -> missingname_7864bcf70cc3cdb856575a33e936cf0af667634490f6123fa1f736ddfe565bcf x1 :e x0)."?
Can you please invent a name for the term defined by " (fun x0 : (set -> set) -> set -> set => fun x1 : set -> set => x0 (x0 (x0 x1)))."?
Can you please invent a name for the term defined by " (fun x0 : set => forall x1, x1 :e x0 -> (forall x2 : set -> set, (forall x3, x3 :e x1 -> x2 x3 :e x0) -> famunion x1 x2 :e x0))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set -> set -> set => fun x2 x3 : set => x0 (x1 x3 x2) (x1 x2 x3))."?
Can you please invent a name for the term defined by " (fun x0 : (set -> set) -> set -> set => fun x1 : set -> set => x0 (x0 (x0 (x0 x1))))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (MagmaHom x0 x1 x2) (MagmaHom x0 x1 x2)) (MagmaHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 : set => and (struct_u x0) (unpack_u_o x0 (fun x1 : set => fun x2 : set -> set => forall x3, x3 :e x1 -> x2 (x2 x3) = x2 x3)))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (MagmaHom x0 x1 x2) (MagmaHom x0 x1 x2)) (MagmaHom x0 x1 x2)) (BinRelnHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (MagmaHom x0 x1 x2) (MagmaHom x0 x1 x2)) (BinRelnHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 : (set -> set) -> set -> set => fun x1 : set -> set => x0 (x0 (x0 (x0 (x0 x1)))))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (MagmaHom x0 x1 x2) (MagmaHom x0 x1 x2)) (MagmaHom x0 x1 x2)) (UnaryFuncHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (MagmaHom x0 x1 x2) (MagmaHom x0 x1 x2)) (BinRelnHom x0 x1 x2)) (BinRelnHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (MagmaHom x0 x1 x2) (MagmaHom x0 x1 x2)) (MagmaHom x0 x1 x2)) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (MagmaHom x0 x1 x2) (BinRelnHom x0 x1 x2)) (PtdSetHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (MagmaHom x0 x1 x2) (MagmaHom x0 x1 x2)) (UnaryFuncHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (MagmaHom x0 x1 x2) (MagmaHom x0 x1 x2)) (UnaryPredHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (BinRelnHom x0 x1 x2) (BinRelnHom x0 x1 x2)) (PtdSetHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (MagmaHom x0 x1 x2) (MagmaHom x0 x1 x2)) (UnaryFuncHom x0 x1 x2)) (BinRelnHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (MagmaHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (PtdSetHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (MagmaHom x0 x1 x2) (MagmaHom x0 x1 x2)) (BinRelnHom x0 x1 x2)) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (MagmaHom x0 x1 x2) (UnaryPredHom x0 x1 x2)) (PtdSetHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (MagmaHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (BinRelnHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (MagmaHom x0 x1 x2) (BinRelnHom x0 x1 x2)) (UnaryPredHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (MagmaHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (BinRelnHom x0 x1 x2)) (BinRelnHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (MagmaHom x0 x1 x2) (MagmaHom x0 x1 x2)) (UnaryPredHom x0 x1 x2)) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (MagmaHom x0 x1 x2) (MagmaHom x0 x1 x2)) (UnaryFuncHom x0 x1 x2)) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (MagmaHom x0 x1 x2) (MagmaHom x0 x1 x2)) (UnaryFuncHom x0 x1 x2)) (UnaryFuncHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (UnaryFuncHom x0 x1 x2) (BinRelnHom x0 x1 x2)) (PtdSetHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (BinRelnHom x0 x1 x2) (UnaryPredHom x0 x1 x2)) (PtdSetHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 : (set -> set) -> set -> set => fun x1 : set -> set => x0 (x0 (x0 (x0 (x0 (x0 x1))))))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (MagmaHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (UnaryPredHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (BinRelnHom x0 x1 x2) (BinRelnHom x0 x1 x2)) (UnaryPredHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (UnaryPredHom x0 x1 x2) (UnaryPredHom x0 x1 x2)) (PtdSetHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (MagmaHom x0 x1 x2) (BinRelnHom x0 x1 x2)) (UnaryPredHom x0 x1 x2)) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (UnaryFuncHom x0 x1 x2) (UnaryPredHom x0 x1 x2)) (PtdSetHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (PreContinuousHom x0 x1 x2) (MagmaHom x0 x1 x2)) (PtdSetHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (UnaryFuncHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (PtdSetHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (MagmaHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (BinRelnHom x0 x1 x2)) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (PreContinuousHom x0 x1 x2) (MagmaHom x0 x1 x2)) (BinRelnHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (UnaryFuncHom x0 x1 x2) (BinRelnHom x0 x1 x2)) (UnaryPredHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (UnaryFuncHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (BinRelnHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (UnaryFuncHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (BinRelnHom x0 x1 x2)) (BinRelnHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (PreContinuousHom x0 x1 x2) (BinRelnHom x0 x1 x2)) (PtdSetHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (PreContinuousHom x0 x1 x2) (MagmaHom x0 x1 x2)) (BinRelnHom x0 x1 x2)) (BinRelnHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (BinRelnHom x0 x1 x2) (BinRelnHom x0 x1 x2)) (UnaryPredHom x0 x1 x2)) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (MagmaHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (UnaryPredHom x0 x1 x2)) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (PreContinuousHom x0 x1 x2) (MagmaHom x0 x1 x2)) (UnaryFuncHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (PreContinuousHom x0 x1 x2) (MagmaHom x0 x1 x2)) (UnaryPredHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (UnaryFuncHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (UnaryPredHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 : (set -> set) -> set -> set => fun x1 : set -> set => x0 (x0 (x0 (x0 (x0 (x0 (x0 x1)))))))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (PreContinuousHom x0 x1 x2) (UnaryPredHom x0 x1 x2)) (PtdSetHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (PreContinuousHom x0 x1 x2) (MagmaHom x0 x1 x2)) (UnaryFuncHom x0 x1 x2)) (BinRelnHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (PreContinuousHom x0 x1 x2) (MagmaHom x0 x1 x2)) (BinRelnHom x0 x1 x2)) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (UnaryFuncHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (BinRelnHom x0 x1 x2)) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (PreContinuousHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (PtdSetHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (UnaryFuncHom x0 x1 x2) (BinRelnHom x0 x1 x2)) (UnaryPredHom x0 x1 x2)) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (PreContinuousHom x0 x1 x2) (BinRelnHom x0 x1 x2)) (UnaryPredHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (PreContinuousHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (BinRelnHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (PreContinuousHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (BinRelnHom x0 x1 x2)) (BinRelnHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (UnaryFuncHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (UnaryPredHom x0 x1 x2)) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (PreContinuousHom x0 x1 x2) (MagmaHom x0 x1 x2)) (UnaryPredHom x0 x1 x2)) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (PreContinuousHom x0 x1 x2) (MagmaHom x0 x1 x2)) (UnaryFuncHom x0 x1 x2)) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (PreContinuousHom x0 x1 x2) (MagmaHom x0 x1 x2)) (UnaryFuncHom x0 x1 x2)) (UnaryFuncHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (PreContinuousHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (UnaryPredHom x0 x1 x2)) (PtdSetHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 : set => and (struct_b x0) (unpack_b_o x0 (fun x1 : set => fun x2 : set -> set -> set => and (explicit_Group x1 x2) (explicit_abelian x1 x2))))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (PreContinuousHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (BinRelnHom x0 x1 x2)) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (PreContinuousHom x0 x1 x2) (BinRelnHom x0 x1 x2)) (UnaryPredHom x0 x1 x2)) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 : (set -> set) -> set -> set => fun x1 : set -> set => x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1))))))))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (PreContinuousHom x0 x1 x2) (UnaryFuncHom x0 x1 x2)) (UnaryPredHom x0 x1 x2)) (UnaryPredHom x0 x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 : (set -> set) -> set -> set => fun x2 : set -> set => x0 (x1 x2))."?
Can you please invent a name for the term defined by " (fun x0 : set => and (struct_p x0) (unpack_p_o x0 (fun x1 : set => fun x2 : set -> prop => forall x3 : prop, (forall x4, and (x4 :e x1) (x2 x4) -> x3) -> x3)))."?
Can you please invent a name for the term defined by " (fun x0 : set => forall x1 : prop, (forall x2, and (x2 :e omega) (missingname_83e7e1dec223e576ffbd3a4af6d06d926c88390b6b4bbe5f6d4db16b20975198 x0 x2) -> x1) -> x1)."?
Can you please invent a name for the term defined by " ReplSep2 missingname_4daffb669546d65312481b5f945330815f8f5c460c7278516e497b08a82751e5 (fun x0 : set => omega) (fun x0 x1 : set => x1 = 0 -> (forall x2 : prop, x2)) div_CSNo."?
Can you please invent a name for the term defined by " (fun x0 : set => and (Field x0) (forall x1, x1 :e omega -> nat_primrec (field4 x0) (fun x3 : set => field1b x0 (field4 x0)) x1 = field3 x0 -> (forall x2 : prop, x2)))."?
Can you please invent a name for the term defined by " (fun x0 : set => fun x1 : set -> set -> prop => fun x2 : set => Sep x0 (fun x3 : set => and (x2 = x3 -> (forall x4 : prop, x4)) (x1 x2 x3)))."?
Can you please invent a name for the term defined by " (fun x0 x1 : (set -> set) -> set -> set => fun x2 : set -> set => fun x3 : set => x0 x2 (x1 x2 x3))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => fun x2 : set -> set => fun x3 : set => explicit_Nats_primrec x0 x1 x2 x3 (fun x4 : set => explicit_Nats_one_plus x0 x1 x2 x3))."?
Can you please invent a name for the term defined by " (fun x0 : set => ap (nat_primrec (lam omega (fun x1 : set => If_i (x1 = 0) 1 0)) (fun x1 x2 : set => lam omega (fun x3 : set => If_i (x3 = 0) 1 (add_nat (ap x2 (Union x3)) (ap x2 x3)))) x0))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 : set => unpack_b_i x0 (fun x4 : set => pack_b (Sep x4 (fun x5 : set => forall x6 : set -> set -> prop, x6 (ap x2 x5) (ap x3 x5) -> x6 (ap x3 x5) (ap x2 x5)))))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 : set => unpack_r_i x0 (fun x4 : set => pack_r (Sep x4 (fun x5 : set => forall x6 : set -> set -> prop, x6 (ap x2 x5) (ap x3 x5) -> x6 (ap x3 x5) (ap x2 x5)))))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 : set => unpack_p_i x0 (fun x4 : set => pack_p (Sep x4 (fun x5 : set => forall x6 : set -> set -> prop, x6 (ap x2 x5) (ap x3 x5) -> x6 (ap x3 x5) (ap x2 x5)))))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 : set => unpack_u_i x0 (fun x4 : set => pack_u (Sep x4 (fun x5 : set => forall x6 : set -> set -> prop, x6 (ap x2 x5) (ap x3 x5) -> x6 (ap x3 x5) (ap x2 x5)))))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => forall x2 : prop, (forall x3, and (x3 :e RealsStruct_Z x0) (forall x4 : prop, (forall x5, and (x5 :e RealsStruct_Npos x0) (field2b x0 x5 x1 = x3) -> x4) -> x4) -> x2) -> x2)."?
Can you please invent a name for the term defined by " (fun x0 : set => missingname_eb5db5f738ad7aa7a16e5fd9f1201ca51305373920f987771a6afffbc5cda3de (permargs_i_3_2_1_0_4_5 (missingname_d45c1fe6a3dff7795ce0a3b891aea8946efc8dceebae3c8b8977b41878b0e841 x0)))."?
Can you please invent a name for the term defined by " (fun x0 : set => missingname_eb5db5f738ad7aa7a16e5fd9f1201ca51305373920f987771a6afffbc5cda3de (permargs_i_1_0_3_2_4_5 (missingname_d45c1fe6a3dff7795ce0a3b891aea8946efc8dceebae3c8b8977b41878b0e841 x0)))."?
Can you please invent a name for the term defined by " (fun x0 : set => missingname_eb5db5f738ad7aa7a16e5fd9f1201ca51305373920f987771a6afffbc5cda3de (permargs_i_2_3_0_1_4_5 (missingname_d45c1fe6a3dff7795ce0a3b891aea8946efc8dceebae3c8b8977b41878b0e841 x0)))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => fun x2 : set -> set => fun x3 : set => and (x3 :e x0) (forall x4, x4 :e x0 -> x3 = explicit_Nats_one_plus x0 x1 x2 (x2 x1) x4 -> (forall x5 : prop, x5)))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 x4 x5 x6 : set => ap (lam 6 (fun x7 : set => If_i (x7 = 0) x1 (If_i (x7 = 1) x2 (If_i (x7 = 2) x3 (If_i (x7 = 3) x4 (If_i (x7 = 4) x5 x6)))))) x0)."?
Can you please invent a name for the term defined by " ReplSep2 missingname_5c3986ee4332ef315b83ef53491e4d2cb38a7ed52b7a33b70161ca6a48b17c87 (fun x0 : set => missingname_5c3986ee4332ef315b83ef53491e4d2cb38a7ed52b7a33b70161ca6a48b17c87) (fun x0 x1 : set => True) SNo_pair."?
Can you please invent a name for the term defined by " (fun x0 : set => and (struct_b x0) (unpack_b_o x0 (fun x1 : set => fun x2 : set -> set -> set => forall x3, x3 :e x1 -> (forall x4, x4 :e x1 -> (forall x5, x5 :e x1 -> x2 (x2 x3 x4) x5 = x2 x3 (x2 x4 x5))))))."?
Can you please invent a name for the term defined by " (fun x0 : set => and (struct_b x0) (unpack_b_o x0 (fun x1 : set => fun x2 : set -> set -> set => and (forall x3, x3 :e x1 -> bij x1 x1 (x2 x3)) (forall x3, x3 :e x1 -> bij x1 x1 (fun x4 : set => x2 x4 x3)))))."?
Can you please invent a name for the term defined by " (fun x0 : set => fun x1 : set -> set => Sep (UnivOf (UPair x0 (famunion x0 (fun x2 : set => Sing (x1 x2))))) (missingname_2cc59ad7dda106b509dcb1f32df804c6d8211b768f557e6c1c51cc2df6180396 x0 x1))."?
Can you please invent a name for the term defined by " (fun x0 : set => Eps_i (fun x1 : set => and (x1 :e omega) (missingname_83e7e1dec223e576ffbd3a4af6d06d926c88390b6b4bbe5f6d4db16b20975198 x1 (Sep (ordsucc x0) (fun x2 : set => and (0 :e x2) (coprime_nat x2 x0))))))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => unpack_p_i x0 (fun x2 : set => fun x3 : set -> prop => unpack_p_i x1 (fun x4 : set => fun x5 : set -> prop => pack_p (setprod x2 x4) (fun x6 : set => and (x3 (ap x6 0)) (x5 (ap x6 1))))))."?
Can you please invent a name for the term defined by " (fun x0 : set => forall x1 : prop, (forall x2, and (x2 :e omega) (forall x3 : prop, (forall x4, and (x4 :e omega) (or (x0 = mul_SNo (eps_ x2) x4) (x0 = minus_SNo (mul_SNo (eps_ x2) x4))) -> x3) -> x3) -> x1) -> x1)."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => fun x2 : set -> set => fun x3 : set => and (x3 :e x0) (forall x4 : prop, (forall x5, and (x5 :e x0) (x3 = explicit_Nats_one_plus x0 x1 x2 (x2 x1) x5) -> x4) -> x4))."?
Can you please invent a name for the term defined by " (fun x0 : set => and (struct_r x0) (unpack_r_o x0 (fun x1 : set => fun x2 : set -> set -> prop => and (forall x3, x3 :e x1 -> not (x2 x3 x3)) (forall x3, x3 :e x1 -> (forall x4, x4 :e x1 -> x2 x3 x4 -> x2 x4 x3)))))."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set => or (x0 = missingname_75223c9f1caec771c751fb18f88418ef8450382ea4c75fd75e31fa2d4abf6881) (x0 = missingname_104bd1d639021d5c073bd32d58e48d5ceaa0c50be10f8aec78c9dae680ad10f5))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => unpack_p_i x0 (fun x2 : set => fun x3 : set -> prop => unpack_p_i x1 (fun x4 : set => fun x5 : set -> prop => pack_p (setexp x4 x2) (fun x6 : set => forall x7, x7 :e x2 -> x3 x7 -> x5 (ap x6 x7)))))."?
Can you please invent a name for the term defined by " (fun x0 : set => and (struct_b_b_e x0) (unpack_b_b_e_o x0 (fun x1 : set => fun x2 x3 : set -> set -> set => fun x4 : set => and (explicit_Ring x1 x4 x2 x3) (forall x5, x5 :e x1 -> (forall x6, x6 :e x1 -> x3 x5 x6 = x3 x6 x5)))))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => nat_primrec (missingname_465e1310c12c30fb65fd32e20d8fb211226903bf56f52b3231cab506526842c0 x0 x0) (fun x2 : set => missingname_7794c6a9f406b8dbb6d24b313affee5bf84fde129928299a1527e8a4696fce2a x0 x0 x1))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => fun x2 : set -> set => fun x3 x4 : set => and (and (x3 :e x0) (x4 :e x0)) (forall x5 : prop, (forall x6, and (x6 :e x0) (explicit_Nats_one_plus x0 x1 x2 x6 x3 = x4) -> x5) -> x5))."?
Can you please invent a name for the term defined by " (fun x0 : set -> (set -> set) -> set => fun x1 x2 : set => forall x3 : set -> set -> prop, (forall x4, forall x5 : set -> set, (forall x6, x6 :e x4 -> x3 x6 (x5 x6)) -> x3 x4 (x0 x4 x5)) -> x3 x1 x2)."?
Can you please invent a name for the term defined by " (fun x0 : set => forall x1 : prop, (forall x2, and (x2 :e omega) (forall x3 : prop, (forall x4, and (x4 :e missingname_4daffb669546d65312481b5f945330815f8f5c460c7278516e497b08a82751e5) (x0 = mul_SNo (eps_ x2) x4) -> x3) -> x3) -> x1) -> x1)."?
Can you please invent a name for the term defined by " (fun x0 : set => fun x1 : set -> set => fun x2 : set -> set -> set -> set => fun x3 : set => Eps_i (missingname_35b91d0b9edf3632a83c30e8f2dcb5e03ee6431724e480c91fa5ef9ae88d0d2f x0 x1 x2 x3))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => unpack_u_i x0 (fun x2 : set => fun x3 : set -> set => unpack_u_i x1 (fun x4 : set => fun x5 : set -> set => pack_u (setprod x2 x4) (fun x6 : set => lam 2 (fun x7 : set => If_i (x7 = 0) (x3 (ap x6 0)) (x5 (ap x6 1)))))))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => fun x2 : set -> set => fun x3 : set => and (x3 :e x0) (forall x4, x4 :e x0 -> missingname_ae6692f2c312f52669ea03eee6399b5eff601066438fd7aea92ceae6ae4a8cb7 x0 x1 x2 x4 x3 -> or (x4 = x1) (x4 = x3)))."?
Can you please invent a name for the term defined by " (fun x0 : set -> set => fun x1 : set -> (set -> set) -> set -> set => In_rec_ii (fun x2 : set => fun x3 : set -> set -> set => If_ii (Union x2 :e x2) (x1 (Union x2) (x3 (Union x2))) x0))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => unpack_r_i x0 (fun x2 : set => fun x3 : set -> set -> prop => unpack_r_i x1 (fun x4 : set => fun x5 : set -> set -> prop => pack_r (setprod x2 x4) (fun x6 x7 : set => and (x3 (ap x6 0) (ap x7 0)) (x5 (ap x6 1) (ap x7 1))))))."?
Can you please invent a name for the term defined by " (fun x0 : set => and (struct_r x0) (unpack_r_o x0 (fun x1 : set => fun x2 : set -> set -> prop => and (forall x3, x3 :e x1 -> not (x2 x3 x3)) (forall x3, x3 :e x1 -> (forall x4, x4 :e x1 -> (forall x5, x5 :e x1 -> x2 x3 x4 -> x2 x4 x5 -> x2 x3 x5))))))."?
Can you please invent a name for the term defined by " (fun x0 : set => missingname_21bb26399802c128b4a27a6184c81e80a2bb391015d712920b939216289ef0b6 (missingname_92bfd592d4bd138d697c881a8067ba190f25e0712f3d0158ce87745d82ec6c69 (missingname_02709d69b879f00cff710051a82db11b456805f2bfe835c5d14f8c542276ac60 x0)))."?
Can you please invent a name for the term defined by " (fun x0 : set => and (x0 c= SNoS_ omega) (forall x1, x1 :e x0 -> (forall x2 : prop, (forall x3, and (x3 :e omega) (forall x4, x4 :e SNoS_ omega -> SNoLt (add_SNo x1 (minus_SNo (eps_ x3))) x4 -> SNoLt x4 (add_SNo x1 (eps_ x3)) -> x4 :e x0) -> x2) -> x2)))."?
Can you please invent a name for the term defined by " (fun x0 : set => fun x1 : set -> set => fun x2 : set => forall x3, SNo x3 -> SNoLt 0 x3 -> (forall x4 : prop, (forall x5, and (x5 :e x0) (forall x6, x6 :e setminus x0 x5 -> SNoLt (abs_SNo (add_SNo (x1 x6) (minus_SNo x2))) x3) -> x4) -> x4))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => unpack_p_i x0 (fun x2 : set => fun x3 : set -> prop => unpack_p_i x1 (fun x4 : set => fun x5 : set -> prop => pack_p (setsum x2 x4) (fun x6 : set => or (and (x6 = Inj0 (Unj x6)) (x3 (Unj x6))) (and (x6 = Inj1 (Unj x6)) (x5 (Unj x6)))))))."?
Can you please invent a name for the term defined by " (fun x0 : set => fun x1 : set -> set => fun x2 : set => forall x3 : set -> prop, (forall x4, x4 :e x0 -> (forall x5, tuple_p (x1 x4) x5 -> (forall x6, x6 :e x1 x4 -> x3 (ap x5 x6)) -> x3 (lam 2 (fun x6 : set => If_i (x6 = 0) x4 x5)))) -> x3 x2)."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 x4 : set => forall x5 : set -> set -> prop, (forall x6, x6 :e x0 -> x5 (ap x1 x6) (ap x2 x6)) -> (forall x6, x5 x6 x6) -> (forall x6 x7, x5 x6 x7 -> x5 x7 x6) -> (forall x6 x7 x8, x5 x6 x7 -> x5 x7 x8 -> x5 x6 x8) -> x5 x3 x4)."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => forall x3 : prop, (forall x4, (forall x5 : prop, (forall x6, and (and (missingname_83bc597c2b0b94d91380ef182323b516f1956d2ac61f7b8a1c7e5f05b39b6051 x0 x4 x1 x2) (subfield x4 x6)) (radical_field_extension x0 x6) -> x5) -> x5) -> x3) -> x3)."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => fun x2 : set -> set => explicit_Nats_primrec x0 x1 x2 x1 (fun x3 x4 : set => If_i (and (x3 = x1 -> (forall x5 : prop, x5)) (missingname_7013937fd1e27f993ba2728905ecd5979ca8f2e29610c3fe92c0d59ade3a19e0 x0 x1 x2 x3 x3)) (x2 x4) x4))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => unpack_r_i x0 (fun x2 : set => fun x3 : set -> set -> prop => unpack_r_i x1 (fun x4 : set => fun x5 : set -> set -> prop => pack_r (setexp x4 x2) (fun x6 x7 : set => forall x8, x8 :e x2 -> (forall x9, x9 :e x2 -> x3 x8 x9 -> x5 (ap x6 x8) (ap x7 x9))))))."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set => forall x1 : (set -> set -> set) -> (set -> set -> set) -> prop, x1 x0 missingname_104bd1d639021d5c073bd32d58e48d5ceaa0c50be10f8aec78c9dae680ad10f5 -> x1 missingname_104bd1d639021d5c073bd32d58e48d5ceaa0c50be10f8aec78c9dae680ad10f5 x0)."?
Can you please invent a name for the term defined by " (fun x0 : set => fun x1 : set -> set => forall x2, SNo x2 -> SNoLt 0 x2 -> (forall x3 : prop, (forall x4, and (x4 :e x0) (forall x5, x5 :e setminus x0 x4 -> (forall x6, x6 :e setminus x0 x4 -> SNoLt (abs_SNo (add_SNo (x1 x5) (minus_SNo (x1 x6)))) x2)) -> x3) -> x3))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => unpack_b_i x0 (fun x2 : set => fun x3 : set -> set -> set => unpack_b_i x1 (fun x4 : set => fun x5 : set -> set -> set => pack_b (setprod x2 x4) (fun x6 x7 : set => lam 2 (fun x8 : set => If_i (x8 = 0) (x3 (ap x6 0) (ap x7 0)) (x5 (ap x6 1) (ap x7 1)))))))."?
Can you please invent a name for the term defined by " (fun x0 : set => and (struct_r x0) (unpack_r_o x0 (fun x1 : set => fun x2 : set -> set -> prop => and (forall x3, x3 :e x1 -> (forall x4, x4 :e x1 -> x2 x3 x4 -> x2 x4 x3)) (forall x3, x3 :e x1 -> (forall x4, x4 :e x1 -> (forall x5, x5 :e x1 -> x2 x3 x4 -> x2 x4 x5 -> x2 x3 x5))))))."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> prop => fun x1 x2 : set => forall x3 : set -> set -> prop, (forall x4 x5, x0 x4 x5 -> x3 x4 x5) -> (forall x4, x3 x4 x4) -> (forall x4 x5, x3 x4 x5 -> x3 x5 x4) -> (forall x4 x5 x6, x3 x4 x5 -> x3 x5 x6 -> x3 x4 x6) -> x3 x1 x2)."?
Can you please invent a name for the term defined by " (fun x0 : (set -> set) -> set -> set => forall x1 : ((set -> set) -> set -> set) -> prop, x1 (fun x2 : set -> set => fun x3 : set => x3) -> (forall x2 : (set -> set) -> set -> set, x1 x2 -> x1 (fun x3 : set -> set => fun x4 : set => x3 (x2 x3 x4))) -> x1 x0)."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (x0 :e omega) (x1 :e omega)) (x2 :e omega)) (or (forall x3 : prop, (forall x4, and (x4 :e omega) (add_nat x0 (mul_nat x4 x2) = x1) -> x3) -> x3) (forall x3 : prop, (forall x4, and (x4 :e omega) (add_nat x1 (mul_nat x4 x2) = x0) -> x3) -> x3)))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => fun x2 : set -> set => fun x3 : set => fun x4 : set -> set -> set => fun x5 x6 : set => forall x7 : set -> set -> prop, x7 x1 x3 -> (forall x8, x8 :e x0 -> (forall x9, x7 x8 x9 -> x7 (x2 x8) (x4 x8 x9))) -> x7 x5 x6)."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (x0 :e omega) (x1 :e omega)) (x2 :e setminus omega 1)) (or (forall x3 : prop, (forall x4, and (x4 :e omega) (add_SNo x0 (mul_SNo x4 x2) = x1) -> x3) -> x3) (forall x3 : prop, (forall x4, and (x4 :e omega) (add_SNo x1 (mul_SNo x4 x2) = x0) -> x3) -> x3)))."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set => fun x1 : set -> (set -> set -> set) -> set -> set -> set => In_rec_iii (fun x2 : set => fun x3 : set -> set -> set -> set => If_iii (Union x2 :e x2) (x1 (Union x2) (x3 (Union x2))) x0))."?
Can you please invent a name for the term defined by " (fun x0 : (set -> set -> set) -> (set -> set -> set) -> set -> set -> set => x0 missingname_75223c9f1caec771c751fb18f88418ef8450382ea4c75fd75e31fa2d4abf6881 missingname_75223c9f1caec771c751fb18f88418ef8450382ea4c75fd75e31fa2d4abf6881)."?
Can you please invent a name for the term defined by " (fun x0 : (set -> set -> set) -> (set -> set -> set) -> set -> set -> set => x0 missingname_75223c9f1caec771c751fb18f88418ef8450382ea4c75fd75e31fa2d4abf6881 missingname_104bd1d639021d5c073bd32d58e48d5ceaa0c50be10f8aec78c9dae680ad10f5)."?
Can you please invent a name for the term defined by " (fun x0 : (set -> set -> set) -> (set -> set -> set) -> set -> set -> set => x0 missingname_104bd1d639021d5c073bd32d58e48d5ceaa0c50be10f8aec78c9dae680ad10f5 missingname_75223c9f1caec771c751fb18f88418ef8450382ea4c75fd75e31fa2d4abf6881)."?
Can you please invent a name for the term defined by " (fun x0 : (set -> set -> set) -> (set -> set -> set) -> set -> set -> set => x0 missingname_104bd1d639021d5c073bd32d58e48d5ceaa0c50be10f8aec78c9dae680ad10f5 missingname_104bd1d639021d5c073bd32d58e48d5ceaa0c50be10f8aec78c9dae680ad10f5)."?
Can you please invent a name for the term defined by " (fun x0 : set -> (set -> set -> set) -> set -> set => fun x1 : set => fun x2 : set -> set => forall x3 : set -> (set -> set) -> prop, (forall x4, forall x5 : set -> set -> set, (forall x6, x6 :e x4 -> x3 x6 (x5 x6)) -> x3 x4 (x0 x4 x5)) -> x3 x1 x2)."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : set => lam 10 (fun x10 : set => If_i (x10 = 0) x0 (If_i (x10 = 1) x1 (If_i (x10 = 2) x2 (If_i (x10 = 3) x3 (If_i (x10 = 4) x4 (If_i (x10 = 5) x5 (If_i (x10 = 6) x6 (If_i (x10 = 7) x7 (If_i (x10 = 8) x8 x9))))))))))."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => x0 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16)."?
Can you please invent a name for the term defined by " (fun x0 : set -> (set -> set -> prop) -> set -> prop => fun x1 : set => fun x2 : set -> prop => forall x3 : set -> (set -> prop) -> prop, (forall x4, forall x5 : set -> set -> prop, (forall x6, x6 :e x4 -> x3 x6 (x5 x6)) -> x3 x4 (x0 x4 x5)) -> x3 x1 x2)."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => x0 :e u17 -> x1 :e u17 -> missingname_ab34eea44c60018e5f975d4318c2d3e52e1a34eb29f14ca15ff8cefeb958c494 (missingname_be1a105c5bdfe1032a5c5adf14a475736a779a8c52e730ee3d06de1b111cbec9 x0) (missingname_be1a105c5bdfe1032a5c5adf14a475736a779a8c52e730ee3d06de1b111cbec9 x1) = (fun x3 x4 : set => x3))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => x0 :e u17 -> x1 :e u17 -> missingname_5b5f35da4b263dbee945b2ffcce9feabfa586bd96c2f75eb4e868d902a221323 (missingname_02709d69b879f00cff710051a82db11b456805f2bfe835c5d14f8c542276ac60 x0) (missingname_02709d69b879f00cff710051a82db11b456805f2bfe835c5d14f8c542276ac60 x1) = (fun x3 x4 : set => x3))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => x0 :e u17 -> x1 :e u17 -> missingname_ab34eea44c60018e5f975d4318c2d3e52e1a34eb29f14ca15ff8cefeb958c494 (missingname_02709d69b879f00cff710051a82db11b456805f2bfe835c5d14f8c542276ac60 x0) (missingname_02709d69b879f00cff710051a82db11b456805f2bfe835c5d14f8c542276ac60 x1) = (fun x3 x4 : set => x3))."?
Can you please invent a name for the term defined by " (fun x0 : set => and (struct_r x0) (unpack_r_o x0 (fun x1 : set => fun x2 : set -> set -> prop => and (and (forall x3, x3 :e x1 -> x2 x3 x3) (forall x3, x3 :e x1 -> (forall x4, x4 :e x1 -> x2 x3 x4 -> x2 x4 x3))) (forall x3, x3 :e x1 -> (forall x4, x4 :e x1 -> (forall x5, x5 :e x1 -> x2 x3 x4 -> x2 x4 x5 -> x2 x3 x5))))))."?
Can you please invent a name for the term defined by " (fun x0 : set => and (struct_r x0) (unpack_r_o x0 (fun x1 : set => fun x2 : set -> set -> prop => and (and (forall x3, x3 :e x1 -> not (x2 x3 x3)) (forall x3, x3 :e x1 -> (forall x4, x4 :e x1 -> or (x2 x3 x4) (x2 x4 x3)))) (forall x3, x3 :e x1 -> (forall x4, x4 :e x1 -> (forall x5, x5 :e x1 -> x2 x3 x4 -> x2 x4 x5 -> x2 x3 x5))))))."?
Can you please invent a name for the term defined by " Sep (SNoS_ (ordsucc omega)) (fun x0 : set => and (and (and (SNoL_omega x0 = 0 -> (forall x1 : prop, x1)) (SNoR_omega x0 = 0 -> (forall x1 : prop, x1))) (missingname_16a206dc52b4bb55b4a6c92782a08f06f95014669558c00b452a0ba01b887b1c (SNoL_omega x0))) (missingname_16a206dc52b4bb55b4a6c92782a08f06f95014669558c00b452a0ba01b887b1c (SNoR_omega x0)))."?
Can you please invent a name for the term defined by " (fun x0 : set => and (struct_b x0) (unpack_b_o x0 (fun x1 : set => fun x2 : set -> set -> set => and (and (forall x3 : prop, (forall x4, and (x4 :e x1) (forall x5, x5 :e x1 -> and (x2 x5 x4 = x5) (x2 x4 x5 = x5)) -> x3) -> x3) (forall x3, x3 :e x1 -> bij x1 x1 (x2 x3))) (forall x3, x3 :e x1 -> bij x1 x1 (fun x4 : set => x2 x4 x3)))))."?
Can you please invent a name for the term defined by " (fun x0 : set => and (struct_b x0) (unpack_b_o x0 (fun x1 : set => fun x2 : set -> set -> set => and (forall x3, x3 :e x1 -> (forall x4, x4 :e x1 -> (forall x5, x5 :e x1 -> x2 (x2 x3 x4) x5 = x2 x3 (x2 x4 x5)))) (forall x3 : prop, (forall x4, and (x4 :e x1) (forall x5, x5 :e x1 -> and (x2 x5 x4 = x5) (x2 x4 x5 = x5)) -> x3) -> x3))))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => missingname_eb5db5f738ad7aa7a16e5fd9f1201ca51305373920f987771a6afffbc5cda3de (missingname_82e8006d227db496db31fec4ec3bd7d6838576829af8850ce4acb380a61f8a32 (missingname_d45c1fe6a3dff7795ce0a3b891aea8946efc8dceebae3c8b8977b41878b0e841 x0) (missingname_d45c1fe6a3dff7795ce0a3b891aea8946efc8dceebae3c8b8977b41878b0e841 x1)))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => missingname_eb5db5f738ad7aa7a16e5fd9f1201ca51305373920f987771a6afffbc5cda3de (missingname_648f8f9b553fd531a0eb9e248d17e0627f860ac0986a02e56f0f803d1a6b76b7 (missingname_d45c1fe6a3dff7795ce0a3b891aea8946efc8dceebae3c8b8977b41878b0e841 x0) (missingname_d45c1fe6a3dff7795ce0a3b891aea8946efc8dceebae3c8b8977b41878b0e841 x1)))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => missingname_eb5db5f738ad7aa7a16e5fd9f1201ca51305373920f987771a6afffbc5cda3de (missingname_c66a68a593f4596a449224889a9d73fa80613c45c60f35804c568447e7d2cec2 (missingname_d45c1fe6a3dff7795ce0a3b891aea8946efc8dceebae3c8b8977b41878b0e841 x0) (missingname_d45c1fe6a3dff7795ce0a3b891aea8946efc8dceebae3c8b8977b41878b0e841 x1)))."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set => forall x1 : (set -> set -> set -> set -> set -> set -> set) -> prop, x1 (fun x2 x3 x4 x5 x6 x7 : set => x2) -> x1 (fun x2 x3 x4 x5 x6 x7 : set => x3) -> x1 (fun x2 x3 x4 x5 x6 x7 : set => x4) -> x1 (fun x2 x3 x4 x5 x6 x7 : set => x5) -> x1 x0)."?
Can you please invent a name for the term defined by " (fun x0 : (set -> set -> set) -> set -> set -> set => missingname_792d152efe262dcaabf368bc6467ac057697a53fc33616f54269226b8862b39f (x0 missingname_75223c9f1caec771c751fb18f88418ef8450382ea4c75fd75e31fa2d4abf6881) (x0 missingname_104bd1d639021d5c073bd32d58e48d5ceaa0c50be10f8aec78c9dae680ad10f5))."?
Can you please invent a name for the term defined by " (fun x0 : (set -> set -> set) -> set -> set -> set => missingname_132c332e15cb143670ab4045b0f1578af13e57d6190aa1c79e16e4c522afaa7f (x0 missingname_75223c9f1caec771c751fb18f88418ef8450382ea4c75fd75e31fa2d4abf6881) (x0 missingname_104bd1d639021d5c073bd32d58e48d5ceaa0c50be10f8aec78c9dae680ad10f5))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => unpack_r_i x0 (fun x2 : set => fun x3 : set -> set -> prop => unpack_r_i x1 (fun x4 : set => fun x5 : set -> set -> prop => pack_r (setsum x2 x4) (fun x6 x7 : set => or (and (and (x6 = Inj0 (Unj x6)) (x7 = Inj0 (Unj x7))) (x3 (Unj x6) (Unj x7))) (and (and (x6 = Inj1 (Unj x6)) (x7 = Inj1 (Unj x7))) (x5 (Unj x6) (Unj x7)))))))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => fun x2 : set -> set => fun x3 x4 : set => and (and (x3 :e x0) (x4 :e x0)) (forall x5, x5 :e x0 -> missingname_ae6692f2c312f52669ea03eee6399b5eff601066438fd7aea92ceae6ae4a8cb7 x0 x1 x2 x5 x3 -> missingname_ae6692f2c312f52669ea03eee6399b5eff601066438fd7aea92ceae6ae4a8cb7 x0 x1 x2 x5 x4 -> x5 = 1))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (x0 :e missingname_4daffb669546d65312481b5f945330815f8f5c460c7278516e497b08a82751e5) (x1 :e missingname_4daffb669546d65312481b5f945330815f8f5c460c7278516e497b08a82751e5)) (x2 :e setminus omega 1)) (missingname_af5f6e65098725dbbf9014383760c67fe7961b5486f9b4fa4d3289ed424f0c1b (add_SNo x0 (minus_SNo x1)) x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => and (and (and (x0 :e missingname_4daffb669546d65312481b5f945330815f8f5c460c7278516e497b08a82751e5) (x1 :e missingname_4daffb669546d65312481b5f945330815f8f5c460c7278516e497b08a82751e5)) (x2 :e setminus omega 1)) (missingname_af5f6e65098725dbbf9014383760c67fe7961b5486f9b4fa4d3289ed424f0c1b x2 (add_SNo x0 (minus_SNo x1))))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => and (and (x0 :e missingname_4daffb669546d65312481b5f945330815f8f5c460c7278516e497b08a82751e5) (x1 :e missingname_4daffb669546d65312481b5f945330815f8f5c460c7278516e497b08a82751e5)) (forall x2 : prop, (forall x3, and (x3 :e missingname_4daffb669546d65312481b5f945330815f8f5c460c7278516e497b08a82751e5) (mul_SNo x0 x3 = x1) -> x2) -> x2))."?
Can you please invent a name for the term defined by " (fun x0 : set -> (set -> set -> set -> set) -> set -> set -> set => fun x1 : set => fun x2 : set -> set -> set => forall x3 : set -> (set -> set -> set) -> prop, (forall x4, forall x5 : set -> set -> set -> set, (forall x6, x6 :e x4 -> x3 x6 (x5 x6)) -> x3 x4 (x0 x4 x5)) -> x3 x1 x2)."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => missingname_d1414bfc0f85adb94cf9bc0deea76f0706a3d64c0b7b545e95c4d02856529e60 (fun x3 : set => x2) (fun x3 : set => fun x4 : set -> set => fun x5 : set => missingname_002c672b3a8841197b02ffaca6fc5977adb99d45947bb283d29e68e638319d3c (ap x5 0) (x4 (missingname_81c5357434137d8c13616b7f69dc50f3e29ee132ced82e17536c4dc24aaa37b9 x5))) x0 x1)."?
Can you please invent a name for the term defined by " (fun x0 : set -> (set -> set -> set -> prop) -> set -> set -> prop => fun x1 : set => fun x2 : set -> set -> prop => forall x3 : set -> (set -> set -> prop) -> prop, (forall x4, forall x5 : set -> set -> set -> prop, (forall x6, x6 :e x4 -> x3 x6 (x5 x6)) -> x3 x4 (x0 x4 x5)) -> x3 x1 x2)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set => forall x1 : (set -> set -> set -> set -> set -> set -> set) -> prop, x1 (fun x2 x3 x4 x5 x6 x7 : set => x2) -> x1 (fun x2 x3 x4 x5 x6 x7 : set => x3) -> x1 (fun x2 x3 x4 x5 x6 x7 : set => x4) -> x1 (fun x2 x3 x4 x5 x6 x7 : set => x5) -> x1 (fun x2 x3 x4 x5 x6 x7 : set => x6) -> x1 x0)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : set => x0 x8 x9 x10 x11 x12 x13 x1 x2 x3 x4 x5 x6 x7)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : set => x0 x9 x10 x11 x12 x13 x1 x2 x3 x4 x5 x6 x7 x8)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : set => x0 x10 x11 x12 x13 x1 x2 x3 x4 x5 x6 x7 x8 x9)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : set => x0 x11 x12 x13 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : set => x0 x12 x13 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : set => x0 x13 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : set => x0 x7 x8 x9 x10 x11 x12 x13 x1 x2 x3 x4 x5 x6)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : set => x0 x6 x7 x8 x9 x10 x11 x12 x13 x1 x2 x3 x4 x5)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : set => x0 x5 x6 x7 x8 x9 x10 x11 x12 x13 x1 x2 x3 x4)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : set => x0 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x1 x2 x3)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : set => x0 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x1 x2)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : set => x0 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x1)."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => fun x3 x4 : set -> set -> set => fun x5 : set -> set -> prop => fun x6 : set => forall x7 : prop, (forall x8, (forall x9 : prop, (forall x10, and (and (natOfOrderedField_p x0 x1 x2 x3 x4 x5 x8) (natOfOrderedField_p x0 x1 x2 x3 x4 x5 x10)) (x4 x10 x6 = x8) -> x9) -> x9) -> x7) -> x7)."?
Can you please invent a name for the term defined by " (fun x0 : set -> (set -> (set -> prop) -> prop) -> (set -> prop) -> prop => fun x1 : set => fun x2 : (set -> prop) -> prop => forall x3 : set -> ((set -> prop) -> prop) -> prop, (forall x4, forall x5 : set -> (set -> prop) -> prop, (forall x6, x6 :e x4 -> x3 x6 (x5 x6)) -> x3 x4 (x0 x4 x5)) -> x3 x1 x2)."?
Can you please invent a name for the term defined by " (fun x0 : set => forall x1 : prop, (forall x2, and (x2 :e omega) (forall x3 : prop, (forall x4, and (and (and (and (forall x5, x5 :e ordsucc x2 -> Group (ap x4 x5)) (forall x5, x5 :e x2 -> normal_subgroup (ap x4 x5) (ap x4 (ordsucc x5)))) (forall x5, x5 :e x2 -> abelian_Group (quotient_Group (ap x4 (ordsucc x5)) (ap x4 x5)))) (x0 = ap x4 x2)) (trivial_Group_p (ap x4 0)) -> x3) -> x3) -> x1) -> x1)."?
Can you please invent a name for the term defined by " fun Obj : set -> prop => fun Hom : set -> set -> set -> prop => fun Id : set -> set => fun Comp : set -> set -> set -> set -> set -> set => (fun x4 : set => fun x5 : set -> set => and (Obj x4) (forall x6, Obj x6 -> and (Hom x6 x4 (x5 x6)) (forall x7, Hom x6 x4 x7 -> x7 = x5 x6)))."?
Can you please invent a name for the term defined by " fun Obj : set -> prop => fun Hom : set -> set -> set -> prop => fun Id : set -> set => fun Comp : set -> set -> set -> set -> set -> set => (fun x4 : set => fun x5 : set -> set => and (Obj x4) (forall x6, Obj x6 -> and (Hom x4 x6 (x5 x6)) (forall x7, Hom x4 x6 x7 -> x7 = x5 x6)))."?
Can you please invent a name for the term defined by " (fun x0 : set => and (struct_c x0) (unpack_c_o x0 (fun x1 : set => fun x2 : (set -> prop) -> prop => and (and (x2 (fun x3 : set => x3 :e x1)) (forall x3 x4 : set -> prop, x2 x3 -> x2 x4 -> x2 (fun x5 : set => and (x3 x5) (x3 x5)))) (forall x3 : (set -> prop) -> prop, (forall x4 : set -> prop, x3 x4 -> x2 x4) -> x2 (fun x4 : set => forall x5 : prop, (forall x6 : set -> prop, and (x3 x6) (x6 x4) -> x5) -> x5)))))."?
Can you please invent a name for the term defined by " (fun x0 : set => fun x1 : set -> set => fun x2 : set -> set -> set -> set => fun x3 x4 : set => forall x5 : set -> set -> prop, (forall x6, x6 :e x0 -> (forall x7, tuple_p (x1 x6) x7 -> (forall x8 : set -> set, (forall x9, x9 :e x1 x6 -> x5 (ap x7 x9) (x8 x9)) -> x5 (lam 2 (fun x9 : set => If_i (x9 = 0) x6 x7)) (x2 x6 x7 (lam (x1 x6) x8))))) -> x5 x3 x4)."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => and (and (x0 :e missingname_4daffb669546d65312481b5f945330815f8f5c460c7278516e497b08a82751e5) (x1 :e missingname_4daffb669546d65312481b5f945330815f8f5c460c7278516e497b08a82751e5)) (forall x2, x2 :e setminus omega 1 -> missingname_af5f6e65098725dbbf9014383760c67fe7961b5486f9b4fa4d3289ed424f0c1b x2 x0 -> missingname_af5f6e65098725dbbf9014383760c67fe7961b5486f9b4fa4d3289ed424f0c1b x2 x1 -> x2 = 1))."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set => forall x1 : (set -> set -> set -> set -> set -> set -> set) -> prop, x1 (fun x2 x3 x4 x5 x6 x7 : set => x2) -> x1 (fun x2 x3 x4 x5 x6 x7 : set => x3) -> x1 (fun x2 x3 x4 x5 x6 x7 : set => x4) -> x1 (fun x2 x3 x4 x5 x6 x7 : set => x5) -> x1 (fun x2 x3 x4 x5 x6 x7 : set => x6) -> x1 (fun x2 x3 x4 x5 x6 x7 : set => x7) -> x1 x0)."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 : set => nat_primrec (missingname_876af35aacef0322494fa29c19a971887d763f8ea0bb0b0de246393dcd2cfa85 x0 x0) (fun x4 : set => missingname_1e526b1566f90c9bbf5b4d9fbade558d9269b711b0361f6f7eb5ca57cf932e1a x0 x0 (missingname_7794c6a9f406b8dbb6d24b313affee5bf84fde129928299a1527e8a4696fce2a x0 x0 (ap x2 x4) (missingname_64a7c008b0f460a3dc3f283b44546876172641d1f8e6631b78d79db56722febd x0 x3 x4))) x1)."?
Can you please invent a name for the term defined by " missingname_c00acb7edb8b15033e7feb60848c09717a7576ab0712aba330acc825801ac0de (fun x0 x1 : set => 0) (fun x0 : set => fun x1 : set -> set -> set => fun x2 x3 : set => missingname_2060dbcf361a2ac6e3e4a9ef169c82b370e5c575aa25460f8ad77d5bbe76b518 (ap x2 0) (ap x3 0) (x1 (missingname_81c5357434137d8c13616b7f69dc50f3e29ee132ced82e17536c4dc24aaa37b9 x2) (missingname_81c5357434137d8c13616b7f69dc50f3e29ee132ced82e17536c4dc24aaa37b9 x3)))."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 : set => x1 :e u17 -> x2 :e u17 -> missingname_b9d766b3b2821eb2774856c22eff5b82b876eae9318ef86bdebd6c9a619cd481 x0 (x0 x1) (x0 x2) = (fun x4 x5 : set => x4))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => fun x2 : set -> set => fun x3 x4 x5 : set => and (and (and (x3 :e x0) (x4 :e x0)) (x5 :e x0)) (or (or (x3 = x4) (forall x6 : prop, (forall x7, and (x7 :e x0) (explicit_Nats_one_plus x0 x1 x2 x3 (explicit_Nats_one_plus x0 x1 x2 x7 x5) = x4) -> x6) -> x6)) (forall x6 : prop, (forall x7, and (x7 :e x0) (explicit_Nats_one_plus x0 x1 x2 x4 (explicit_Nats_one_plus x0 x1 x2 x7 x5) = x3) -> x6) -> x6)))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 : set => and (missingname_51ff5b8b4eefdfcfdf9232efae9edc27c185d6a9dd776b6f5628bc19e838c2c7 x0 x1 x2 x3) (forall x4, missingname_51ff5b8b4eefdfcfdf9232efae9edc27c185d6a9dd776b6f5628bc19e838c2c7 x0 x4 x2 x3 -> (forall x5 : prop, (forall x6, and (and (Field_Hom x1 x4 x6) (forall x7, x7 :e field0 x0 -> ap x6 x7 = x7)) (forall x7, x7 :e field0 x0 -> (forall x8, x8 :e field0 x0 -> ap x6 x7 = ap x6 x8 -> x7 = x8)) -> x5) -> x5)))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => unpack_b_b_e_o x0 (fun x3 : set => fun x4 x5 : set -> set -> set => fun x6 : set => unpack_b_b_e_o x1 (fun x7 : set => fun x8 x9 : set -> set -> set => fun x10 : set => and (and (and (x2 :e setexp x7 x3) (forall x11, x11 :e x3 -> (forall x12, x12 :e x3 -> ap x2 (x4 x11 x12) = x8 (ap x2 x11) (ap x2 x12)))) (forall x11, x11 :e x3 -> (forall x12, x12 :e x3 -> ap x2 (x5 x11 x12) = x9 (ap x2 x11) (ap x2 x12)))) (ap x2 x6 = x10))))."?
Can you please invent a name for the term defined by " (fun x0 : set => and (struct_r x0) (unpack_r_o x0 (fun x1 : set => fun x2 : set -> set -> prop => and (and (and (forall x3, x3 :e x1 -> not (x2 x3 x3)) (forall x3, x3 :e x1 -> (forall x4, x4 :e x1 -> or (x2 x3 x4) (x2 x4 x3)))) (forall x3, x3 :e x1 -> (forall x4, x4 :e x1 -> (forall x5, x5 :e x1 -> x2 x3 x4 -> x2 x4 x5 -> x2 x3 x5)))) (forall x3 : set -> prop, (forall x4, x4 :e x1 -> (forall x5, x5 :e x1 -> x2 x5 x4 -> x3 x5) -> x3 x4) -> (forall x4, x4 :e x1 -> x3 x4)))))."?
Can you please invent a name for the term defined by " (fun x0 : set -> (set -> ((set -> prop) -> prop) -> prop) -> ((set -> prop) -> prop) -> prop => fun x1 : set => fun x2 : ((set -> prop) -> prop) -> prop => forall x3 : set -> (((set -> prop) -> prop) -> prop) -> prop, (forall x4, forall x5 : set -> ((set -> prop) -> prop) -> prop, (forall x6, x6 :e x4 -> x3 x6 (x5 x6)) -> x3 x4 (x0 x4 x5)) -> x3 x1 x2)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 : set => x0 x2 x4 x1 x3 x6 x8 x5 x7 x11 x9 x12 x10 x14 x15 x16 x13)."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => unpack_b_b_e_e_o x0 (fun x3 : set => fun x4 x5 : set -> set -> set => fun x6 x7 : set => unpack_b_b_e_e_o x1 (fun x8 : set => fun x9 x10 : set -> set -> set => fun x11 x12 : set => and (and (and (and (x2 :e setexp x8 x3) (forall x13, x13 :e x3 -> (forall x14, x14 :e x3 -> ap x2 (x4 x13 x14) = x9 (ap x2 x13) (ap x2 x14)))) (forall x13, x13 :e x3 -> (forall x14, x14 :e x3 -> ap x2 (x5 x13 x14) = x10 (ap x2 x13) (ap x2 x14)))) (ap x2 x6 = x11)) (ap x2 x7 = x12))))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set -> set -> set -> set -> set -> set -> set => fun x2 x3 x4 x5 x6 x7 : set => x0 (permargs_i_3_2_1_0_4_5 x1 x2 x3 x4 x5 x6 x7) (permargs_i_3_2_1_0_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_3_2_1_0_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_3_2_1_0_4_5 x1 x2 x3 x4 x5 x6 x7) (permargs_i_3_2_1_0_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_3_2_1_0_4_5 x1 x2 x3 x4 x5 x6 x7))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set -> set -> set -> set -> set -> set -> set => fun x2 x3 x4 x5 x6 x7 : set => x0 (permargs_i_1_0_3_2_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_1_0_3_2_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_1_0_3_2_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_1_0_3_2_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_1_0_3_2_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_1_0_3_2_4_5 x1 x2 x3 x4 x5 x6 x7))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set -> set -> set -> set -> set -> set -> set => fun x2 x3 x4 x5 x6 x7 : set => x0 (permargs_i_2_3_0_1_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_2_3_0_1_4_5 x1 x2 x3 x4 x5 x6 x7) (permargs_i_2_3_0_1_4_5 x1 x2 x3 x4 x5 x6 x7) (permargs_i_2_3_0_1_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_2_3_0_1_4_5 x1 x2 x3 x4 x5 x6 x7) (permargs_i_2_3_0_1_4_5 x1 x2 x3 x4 x5 x6 x7))."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 : set => x0 x10 x11 x12 x13 x14 x15 x16 x17 x1 x2 x3 x4 x5 x6 x7 x8 x9)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 : set => x0 x9 x10 x11 x12 x13 x14 x15 x16 x17 x1 x2 x3 x4 x5 x6 x7 x8)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 : set => x0 x11 x12 x13 x14 x15 x16 x17 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 : set => x0 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x1 x2 x3 x4 x5 x6 x7)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 : set => x0 x12 x13 x14 x15 x16 x17 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 : set => x0 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x1 x2 x3 x4 x5 x6)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 : set => x0 x13 x14 x15 x16 x17 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 : set => x0 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x1 x2 x3 x4 x5)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 : set => x0 x14 x15 x16 x17 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 : set => x0 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x1 x2 x3 x4)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 : set => x0 x15 x16 x17 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 : set => x0 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x1 x2 x3)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 : set => x0 x16 x17 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 : set => x0 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x1 x2)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 : set => x0 x17 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 : set => x0 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x1)."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => forall x2 x3 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set, missingname_0ecea12529c16388abbd7afd132dcfc71eca000587337d9afd56ea93c40ef1ef x2 -> missingname_0ecea12529c16388abbd7afd132dcfc71eca000587337d9afd56ea93c40ef1ef x3 -> x0 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 -> x1 = x3 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 -> missingname_c56bb54dd1f4c2c13129be6ed51c6ed97d3f990956b0c22589aad20ca952e3f1 x2 x3 = (fun x5 x6 : set => x5))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 : set => x0 :e u6 -> x1 :e u6 -> x2 :e u6 -> x3 :e u6 -> missingname_e73271112c979d5c0e9c9345f7d93a63015c1e7231d69df1ea1f24bf25f50380 (missingname_d45c1fe6a3dff7795ce0a3b891aea8946efc8dceebae3c8b8977b41878b0e841 x0) (missingname_d45c1fe6a3dff7795ce0a3b891aea8946efc8dceebae3c8b8977b41878b0e841 x1) (missingname_d45c1fe6a3dff7795ce0a3b891aea8946efc8dceebae3c8b8977b41878b0e841 x2) (missingname_d45c1fe6a3dff7795ce0a3b891aea8946efc8dceebae3c8b8977b41878b0e841 x3) = (fun x5 x6 : set => x5))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => If_i (and (x1 :e missingname_e31f018a102b5560fa03494c99c4daa3e083577f310f2537bf2b03dd15ac3d47 x0 x0) (x2 :e setminus (missingname_e31f018a102b5560fa03494c99c4daa3e083577f310f2537bf2b03dd15ac3d47 x0 x0) (Sing (missingname_876af35aacef0322494fa29c19a971887d763f8ea0bb0b0de246393dcd2cfa85 x0 x0)))) (Eps_i (fun x3 : set => and (x3 :e missingname_e31f018a102b5560fa03494c99c4daa3e083577f310f2537bf2b03dd15ac3d47 x0 x0) (x1 = missingname_7794c6a9f406b8dbb6d24b313affee5bf84fde129928299a1527e8a4696fce2a x0 x0 x2 x3))) 0)."?
Can you please invent a name for the term defined by " (fun x0 : (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> set -> set -> set => missingname_35679a0f8445869c94133e6427c00b64926e5191b565cad2de5df35770369d95 (fun x1 : set -> set -> set => missingname_35679a0f8445869c94133e6427c00b64926e5191b565cad2de5df35770369d95 (fun x2 : set -> set -> set => x0 (fun x3 : (set -> set -> set) -> (set -> set -> set) -> set -> set -> set => x3 x1 x2))))."?
Can you please invent a name for the term defined by " (fun x0 : (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> set -> set -> set => missingname_91aba9b131a7808e8b8899f5e619d2a78fe76815c7f25b7df01c0b387c9793ec (fun x1 : set -> set -> set => missingname_91aba9b131a7808e8b8899f5e619d2a78fe76815c7f25b7df01c0b387c9793ec (fun x2 : set -> set -> set => x0 (fun x3 : (set -> set -> set) -> (set -> set -> set) -> set -> set -> set => x3 x1 x2))))."?
Can you please invent a name for the term defined by " (fun x0 : set => fun x1 : (set -> set -> set -> set -> set -> set -> set) -> (set -> set -> set -> set -> set -> set -> set) -> set -> set -> set -> set -> set -> set -> set => x1 (missingname_d45c1fe6a3dff7795ce0a3b891aea8946efc8dceebae3c8b8977b41878b0e841 (ap x0 0)) (missingname_d45c1fe6a3dff7795ce0a3b891aea8946efc8dceebae3c8b8977b41878b0e841 (ap x0 u1)))."?
Can you please invent a name for the term defined by " (fun x0 : set -> (set -> (((set -> prop) -> prop) -> prop) -> prop) -> (((set -> prop) -> prop) -> prop) -> prop => fun x1 : set => fun x2 : (((set -> prop) -> prop) -> prop) -> prop => forall x3 : set -> ((((set -> prop) -> prop) -> prop) -> prop) -> prop, (forall x4, forall x5 : set -> (((set -> prop) -> prop) -> prop) -> prop, (forall x6, x6 :e x4 -> x3 x6 (x5 x6)) -> x3 x4 (x0 x4 x5)) -> x3 x1 x2)."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 : set => ap (lam 17 (fun x18 : set => If_i (x18 = 0) x1 (If_i (x18 = 1) x2 (If_i (x18 = 2) x3 (If_i (x18 = 3) x4 (If_i (x18 = 4) x5 (If_i (x18 = 5) x6 (If_i (x18 = 6) x7 (If_i (x18 = 7) x8 (If_i (x18 = 8) x9 (If_i (x18 = 9) x10 (If_i (x18 = 10) x11 (If_i (x18 = 11) x12 (If_i (x18 = 12) x13 (If_i (x18 = 13) x14 (If_i (x18 = 14) x15 (If_i (x18 = 15) x16 x17))))))))))))))))) x0)."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 : set => and (and (subfield x0 x1) (x3 :e setexp (field0 x0) (ordsucc x2))) (forall x4 : prop, (forall x5, and (x5 :e setminus (field0 x0) (Sing (field3 x0))) (and (ap x3 x2 = x5) (forall x6 : prop, (forall x7, and (x7 :e setexp (setexp (field0 x1) 2) x2) (and (forall x8, x8 :e x2 -> ap (ap x7 x8) 1 = field4 x0) (forall x8, x8 :e field0 x1 -> CRing_with_id_eval_poly x1 (ordsucc x2) x3 x8 = nat_primrec x5 (fun x10 x11 : set => field2b x1 x11 (CRing_with_id_eval_poly x1 2 (ap x7 x10) x8)) x2)) -> x6) -> x6)) -> x4) -> x4))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 : set => ap (lam 17 (fun x18 : set => If_i (x18 = 0) x1 (If_i (x18 = 1) x18 (If_i (x18 = 2) x3 (If_i (x18 = 3) x4 (If_i (x18 = 4) x5 (If_i (x18 = 5) x6 (If_i (x18 = 6) x7 (If_i (x18 = 7) x8 (If_i (x18 = 8) x9 (If_i (x18 = 9) x10 (If_i (x18 = 10) x11 (If_i (x18 = 11) x12 (If_i (x18 = 12) x13 (If_i (x18 = 13) x14 (If_i (x18 = 14) x15 (If_i (x18 = 15) x16 x17))))))))))))))))) x0)."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => forall x2 x3 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set, missingname_2a50602e0a09f647d85d3e0968b772706a7501d07652bb47048c29a7df10757a x2 -> missingname_2a50602e0a09f647d85d3e0968b772706a7501d07652bb47048c29a7df10757a x3 -> x0 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 -> x1 = x3 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 -> missingname_b494b403a7bc654ac1ab63d560d5a7782a4857b882ac7cf6d167021892aa5c7e x2 x3 = (fun x5 x6 : set => x5))."?
Can you please invent a name for the term defined by " (fun x0 : (set -> prop) -> prop => fun x1 : (set -> set -> prop) -> prop => fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 : set => fun x12 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x13 x14 : set -> set -> set => fun x15 x16 x17 : set => x14 (x13 (x13 x17 x15) x16) (x13 x15 x16))."?
Can you please invent a name for the term defined by " (fun x0 : set => and (struct_c x0) (unpack_c_o x0 (fun x1 : set => fun x2 : (set -> prop) -> prop => and (and (and (x2 (fun x3 : set => x3 :e x1)) (forall x3 x4 : set -> prop, x2 x3 -> x2 x4 -> x2 (fun x5 : set => and (x3 x5) (x3 x5)))) (forall x3 : (set -> prop) -> prop, (forall x4 : set -> prop, x3 x4 -> x2 x4) -> x2 (fun x4 : set => forall x5 : prop, (forall x6 : set -> prop, and (x3 x6) (x6 x4) -> x5) -> x5))) (forall x3, x3 :e x1 -> (forall x4, x4 :e x1 -> (x3 = x4 -> (forall x5 : prop, x5)) -> (forall x5 : prop, (forall x6 : set -> prop, and (x2 x6) (exactly1of2 (x6 x3) (x6 x4)) -> x5) -> x5))))))."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => and (and (x0 = (fun x2 : (set -> set -> set) -> (set -> set -> set) -> set -> set -> set => x2 (x0 (fun x3 x4 : set -> set -> set => x3)) (x0 (fun x3 x4 : set -> set -> set => x4)))) (missingname_dc35161fb2ec34bf4e293b173ad207112be3b1a971ffff2e3f1eba0f3f0d06db (x0 (fun x1 x2 : set -> set -> set => x1)))) (missingname_dc35161fb2ec34bf4e293b173ad207112be3b1a971ffff2e3f1eba0f3f0d06db (x0 (fun x1 x2 : set -> set -> set => x2))))."?
Can you please invent a name for the term defined by " fun Obj : set -> prop => fun Hom : set -> set -> set -> prop => fun Id : set -> set => fun Comp : set -> set -> set -> set -> set -> set => (fun x4 x5 x6 : set -> set -> set => fun x7 : set -> set -> set -> set -> set -> set => forall x8 x9, Obj x8 -> Obj x9 -> missingname_493d090f589a446965fd7ce072dae5c79961b326d7a828819eb9e8596dd094ce Obj Hom Id Comp x8 x9 (x4 x8 x9) (x5 x8 x9) (x6 x8 x9) (x7 x8 x9))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => forall x2 : prop, (forall x3, and (and (forall x4, x4 :e x0 -> (forall x5 : prop, (forall x6, and (x6 :e x1) (missingname_ed4cdd1284c274c310e985cad4b2fb03e63b825585748249d94045f2fa3c1f70 x4 x6 :e x3) -> x5) -> x5)) (forall x4, x4 :e x1 -> (forall x5 : prop, (forall x6, and (x6 :e x0) (missingname_ed4cdd1284c274c310e985cad4b2fb03e63b825585748249d94045f2fa3c1f70 x6 x4 :e x3) -> x5) -> x5))) (forall x4 x5 x6 x7, missingname_ed4cdd1284c274c310e985cad4b2fb03e63b825585748249d94045f2fa3c1f70 x4 x5 :e x3 -> missingname_ed4cdd1284c274c310e985cad4b2fb03e63b825585748249d94045f2fa3c1f70 x6 x7 :e x3 -> iff (x4 = x6) (x5 = x7)) -> x2) -> x2)."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 : set => unpack_b_b_r_e_e_o x0 (fun x3 : set => fun x4 x5 : set -> set -> set => fun x6 : set -> set -> prop => fun x7 x8 : set => unpack_b_b_r_e_e_o x1 (fun x9 : set => fun x10 x11 : set -> set -> set => fun x12 : set -> set -> prop => fun x13 x14 : set => and (and (and (and (and (x2 :e setexp x9 x3) (forall x15, x15 :e x3 -> (forall x16, x16 :e x3 -> ap x2 (x4 x15 x16) = x10 (ap x2 x15) (ap x2 x16)))) (forall x15, x15 :e x3 -> (forall x16, x16 :e x3 -> ap x2 (x5 x15 x16) = x11 (ap x2 x15) (ap x2 x16)))) (forall x15, x15 :e x3 -> (forall x16, x16 :e x3 -> x6 x15 x16 -> x12 (ap x2 x15) (ap x2 x16)))) (ap x2 x7 = x13)) (ap x2 x8 = x14))))."?
Can you please invent a name for the term defined by " (fun x0 x1 : ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => missingname_792d152efe262dcaabf368bc6467ac057697a53fc33616f54269226b8862b39f (missingname_3f722e3216ed8fcdbdfaa42fe61e6869e0e4fe9464064bd2d51c3b063940b714 (x0 (fun x2 x3 : set -> set -> set => x2)) (x1 (fun x2 x3 : set -> set -> set => x2))) (missingname_3f722e3216ed8fcdbdfaa42fe61e6869e0e4fe9464064bd2d51c3b063940b714 (x0 (fun x2 x3 : set -> set -> set => x3)) (x1 (fun x2 x3 : set -> set -> set => x3))))."?
Can you please invent a name for the term defined by " (fun x0 : (set -> prop) -> prop => fun x1 : (set -> set -> prop) -> prop => fun x2 : set => fun x3 x4 : set -> set -> set => and (and (and (x0 (fun x5 : set => forall x6 : set -> set -> prop, x6 (x3 x5 x2) x5 -> x6 x5 (x3 x5 x2))) (x1 (fun x5 x6 : set => forall x7 : set -> set -> prop, x7 (x3 x5 x6) (x3 x6 x5) -> x7 (x3 x6 x5) (x3 x5 x6)))) (x0 (fun x5 : set => x0 (fun x6 : set => forall x7 : set -> set -> prop, x7 (x3 (x4 x5 x6) x6) x5 -> x7 x5 (x3 (x4 x5 x6) x6))))) (x0 (fun x5 : set => x0 (fun x6 : set => forall x7 : set -> set -> prop, x7 (x4 (x3 x5 x6) x6) x5 -> x7 x5 (x4 (x3 x5 x6) x6)))))."?
Can you please invent a name for the term defined by " (fun x0 : set => and (struct_c x0) (unpack_c_o x0 (fun x1 : set => fun x2 : (set -> prop) -> prop => and (and (and (x2 (fun x3 : set => x3 :e x1)) (forall x3 x4 : set -> prop, x2 x3 -> x2 x4 -> x2 (fun x5 : set => and (x3 x5) (x3 x5)))) (forall x3 : (set -> prop) -> prop, (forall x4 : set -> prop, x3 x4 -> x2 x4) -> x2 (fun x4 : set => forall x5 : prop, (forall x6 : set -> prop, and (x3 x6) (x6 x4) -> x5) -> x5))) (forall x3, x3 :e x1 -> (forall x4, x4 :e x1 -> (x3 = x4 -> (forall x5 : prop, x5)) -> (forall x5 : prop, (forall x6 : set -> prop, (forall x7 : prop, (forall x8 : set -> prop, and (and (and (and (x2 x6) (x2 x8)) (x6 x3)) (x8 x4)) (forall x9, x6 x9 -> not (x8 x9)) -> x7) -> x7) -> x5) -> x5))))))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 : set => x0 (x1 x2 x8 x10 x6 x5 x9 x3 x7 x4 x11) (x1 x3 x2 x4 x5 x11 x8 x7 x10 x9 x6) (x1 x4 x5 x2 x3 x7 x6 x9 x8 x11 x10) (x1 x5 x9 x8 x2 x10 x11 x4 x3 x6 x7) (x1 x6 x10 x9 x11 x2 x7 x8 x4 x3 x5) (x1 x7 x3 x5 x4 x6 x2 x11 x9 x10 x8) (x1 x8 x7 x6 x10 x4 x3 x2 x11 x5 x9) (x1 x9 x6 x11 x7 x3 x5 x10 x2 x8 x4) (x1 x10 x11 x7 x8 x9 x4 x5 x6 x2 x3) (x1 x11 x4 x3 x9 x8 x10 x6 x5 x7 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 : set => x0 (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) (x1 x3 x7 x11 x4 x9 x8 x2 x5 x6 x10) (x1 x4 x11 x3 x7 x8 x10 x5 x6 x2 x9) (x1 x5 x4 x7 x3 x2 x9 x10 x11 x8 x6) (x1 x6 x9 x8 x2 x7 x4 x11 x10 x5 x3) (x1 x7 x8 x10 x9 x4 x6 x3 x2 x11 x5) (x1 x8 x2 x5 x10 x11 x3 x6 x4 x9 x7) (x1 x9 x5 x6 x11 x10 x2 x4 x7 x3 x8) (x1 x10 x6 x2 x8 x5 x11 x9 x3 x7 x4) (x1 x11 x10 x9 x6 x3 x5 x7 x8 x4 x2))."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set -> set -> set -> set -> set -> set) -> (set -> set -> set -> set -> set -> set -> set) -> set -> set -> set -> set -> set -> set -> set) -> set -> set -> set -> set -> set -> set -> set => lam 2 (fun x1 : set => If_i (x1 = 0) (missingname_eb5db5f738ad7aa7a16e5fd9f1201ca51305373920f987771a6afffbc5cda3de (x0 (fun x2 x3 : set -> set -> set -> set -> set -> set -> set => x2))) (missingname_eb5db5f738ad7aa7a16e5fd9f1201ca51305373920f987771a6afffbc5cda3de (x0 (fun x2 x3 : set -> set -> set -> set -> set -> set -> set => x3)))))."?
Can you please invent a name for the term defined by " (fun x0 : set -> prop => fun x1 : (set -> prop) -> prop => fun x2 : (set -> set -> prop) -> prop => fun x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 : set => fun x17 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x18 x19 x20 : set -> set -> set => fun x21 x22 x23 : set => x20 (x19 (x19 x23 x21) x22) (x19 x21 x22))."?
Can you please invent a name for the term defined by " fun Obj : set -> prop => fun Hom : set -> set -> set -> prop => fun Id : set -> set => fun Comp : set -> set -> set -> set -> set -> set => (fun x4 x5 x6 x7 x8 : set => fun x9 : set -> set -> set -> set => and (and (and (and (and (Obj x4) (Obj x5)) (Obj x6)) (Hom x6 x4 x7)) (Hom x6 x5 x8)) (forall x10, Obj x10 -> (forall x11 x12, Hom x10 x4 x11 -> Hom x10 x5 x12 -> and (and (and (Hom x10 x6 (x9 x10 x11 x12)) (Comp x10 x6 x4 x7 (x9 x10 x11 x12) = x11)) (Comp x10 x6 x5 x8 (x9 x10 x11 x12) = x12)) (forall x13, Hom x10 x6 x13 -> Comp x10 x6 x4 x7 x13 = x11 -> Comp x10 x6 x5 x8 x13 = x12 -> x13 = x9 x10 x11 x12))))."?
Can you please invent a name for the term defined by " (fun x0 : (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x0 missingname_2e12608647c99a68694a61275a0e9156460645755458f1551d68b75293953059 missingname_2e12608647c99a68694a61275a0e9156460645755458f1551d68b75293953059)."?
Can you please invent a name for the term defined by " (fun x0 : (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x0 missingname_2e12608647c99a68694a61275a0e9156460645755458f1551d68b75293953059 missingname_d616e801762a7e0b9e4e1f65312c0e6fe6dbec7c6eb43b9297104e2c3939fd97)."?
Can you please invent a name for the term defined by " (fun x0 : (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x0 missingname_2e12608647c99a68694a61275a0e9156460645755458f1551d68b75293953059 missingname_19578582e28e520ae18640d2da9cfec3ac640cd755b8c49951cb91fa674e73a0)."?
Can you please invent a name for the term defined by " (fun x0 : (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x0 missingname_2e12608647c99a68694a61275a0e9156460645755458f1551d68b75293953059 missingname_6b7c843a0ad78ff8e468206d1828ddb5a88aab5415d071258483af482b92c6b7)."?
Can you please invent a name for the term defined by " (fun x0 : (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x0 missingname_d616e801762a7e0b9e4e1f65312c0e6fe6dbec7c6eb43b9297104e2c3939fd97 missingname_2e12608647c99a68694a61275a0e9156460645755458f1551d68b75293953059)."?
Can you please invent a name for the term defined by " (fun x0 : (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x0 missingname_d616e801762a7e0b9e4e1f65312c0e6fe6dbec7c6eb43b9297104e2c3939fd97 missingname_d616e801762a7e0b9e4e1f65312c0e6fe6dbec7c6eb43b9297104e2c3939fd97)."?
Can you please invent a name for the term defined by " (fun x0 : (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x0 missingname_d616e801762a7e0b9e4e1f65312c0e6fe6dbec7c6eb43b9297104e2c3939fd97 missingname_19578582e28e520ae18640d2da9cfec3ac640cd755b8c49951cb91fa674e73a0)."?
Can you please invent a name for the term defined by " (fun x0 : (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x0 missingname_d616e801762a7e0b9e4e1f65312c0e6fe6dbec7c6eb43b9297104e2c3939fd97 missingname_6b7c843a0ad78ff8e468206d1828ddb5a88aab5415d071258483af482b92c6b7)."?
Can you please invent a name for the term defined by " (fun x0 : (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x0 missingname_19578582e28e520ae18640d2da9cfec3ac640cd755b8c49951cb91fa674e73a0 missingname_2e12608647c99a68694a61275a0e9156460645755458f1551d68b75293953059)."?
Can you please invent a name for the term defined by " (fun x0 : (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x0 missingname_19578582e28e520ae18640d2da9cfec3ac640cd755b8c49951cb91fa674e73a0 missingname_d616e801762a7e0b9e4e1f65312c0e6fe6dbec7c6eb43b9297104e2c3939fd97)."?
Can you please invent a name for the term defined by " (fun x0 : (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x0 missingname_19578582e28e520ae18640d2da9cfec3ac640cd755b8c49951cb91fa674e73a0 missingname_19578582e28e520ae18640d2da9cfec3ac640cd755b8c49951cb91fa674e73a0)."?
Can you please invent a name for the term defined by " (fun x0 : (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x0 missingname_19578582e28e520ae18640d2da9cfec3ac640cd755b8c49951cb91fa674e73a0 missingname_6b7c843a0ad78ff8e468206d1828ddb5a88aab5415d071258483af482b92c6b7)."?
Can you please invent a name for the term defined by " (fun x0 : (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x0 missingname_6b7c843a0ad78ff8e468206d1828ddb5a88aab5415d071258483af482b92c6b7 missingname_2e12608647c99a68694a61275a0e9156460645755458f1551d68b75293953059)."?
Can you please invent a name for the term defined by " (fun x0 : (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x0 missingname_6b7c843a0ad78ff8e468206d1828ddb5a88aab5415d071258483af482b92c6b7 missingname_d616e801762a7e0b9e4e1f65312c0e6fe6dbec7c6eb43b9297104e2c3939fd97)."?
Can you please invent a name for the term defined by " (fun x0 : (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x0 missingname_6b7c843a0ad78ff8e468206d1828ddb5a88aab5415d071258483af482b92c6b7 missingname_19578582e28e520ae18640d2da9cfec3ac640cd755b8c49951cb91fa674e73a0)."?
Can you please invent a name for the term defined by " (fun x0 : (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x0 missingname_6b7c843a0ad78ff8e468206d1828ddb5a88aab5415d071258483af482b92c6b7 missingname_6b7c843a0ad78ff8e468206d1828ddb5a88aab5415d071258483af482b92c6b7)."?
Can you please invent a name for the term defined by " (fun x0 : (set -> prop) -> prop => fun x1 : (set -> set -> prop) -> prop => fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 : set => fun x12 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x13 : set => ap (ap (x12 (x12 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) (x12 x3 x7 x11 x4 x9 x8 x2 x5 x6 x10) (x12 x4 x11 x3 x7 x8 x10 x5 x6 x2 x9) (x12 x5 x4 x7 x3 x2 x9 x10 x11 x8 x6) (x12 x6 x9 x8 x2 x7 x4 x11 x10 x5 x3) (x12 x7 x8 x10 x9 x4 x6 x3 x2 x11 x5) (x12 x8 x2 x5 x10 x11 x3 x6 x4 x9 x7) (x12 x9 x5 x6 x11 x10 x2 x4 x7 x3 x8) (x12 x10 x6 x2 x8 x5 x11 x9 x3 x7 x4) (x12 x11 x10 x9 x6 x3 x5 x7 x8 x4 x2)) x13))."?
Can you please invent a name for the term defined by " (fun x0 : (set -> prop) -> prop => fun x1 : (set -> set -> prop) -> prop => fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 : set => fun x12 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x13 : set => ap (ap (x12 (x12 x2 x8 x10 x6 x5 x9 x3 x7 x4 x11) (x12 x3 x2 x4 x5 x11 x8 x7 x10 x9 x6) (x12 x4 x5 x2 x3 x7 x6 x9 x8 x11 x10) (x12 x5 x9 x8 x2 x10 x11 x4 x3 x6 x7) (x12 x6 x10 x9 x11 x2 x7 x8 x4 x3 x5) (x12 x7 x3 x5 x4 x6 x2 x11 x9 x10 x8) (x12 x8 x7 x6 x10 x4 x3 x2 x11 x5 x9) (x12 x9 x6 x11 x7 x3 x5 x10 x2 x8 x4) (x12 x10 x11 x7 x8 x9 x4 x5 x6 x2 x3) (x12 x11 x4 x3 x9 x8 x10 x6 x5 x7 x2)) x13))."?
Can you please invent a name for the term defined by " (fun x0 : set -> prop => fun x1 : (set -> prop) -> prop => fun x2 : (set -> set -> prop) -> prop => fun x3 : set => fun x4 x5 : set -> set -> set => and (and (and (and (and (x2 (fun x6 x7 : set => x0 (x4 x6 x7))) (x1 (fun x6 : set => x1 (fun x7 : set => x0 (x5 x6 x7))))) (x1 (fun x6 : set => forall x7 : set -> set -> prop, x7 (x4 x6 x3) x6 -> x7 x6 (x4 x6 x3)))) (x2 (fun x6 x7 : set => forall x8 : set -> set -> prop, x8 (x4 x6 x7) (x4 x7 x6) -> x8 (x4 x7 x6) (x4 x6 x7)))) (x1 (fun x6 : set => x1 (fun x7 : set => forall x8 : set -> set -> prop, x8 (x4 (x5 x6 x7) x7) x6 -> x8 x6 (x4 (x5 x6 x7) x7))))) (x1 (fun x6 : set => x1 (fun x7 : set => forall x8 : set -> set -> prop, x8 (x5 (x4 x6 x7) x7) x6 -> x8 x6 (x5 (x4 x6 x7) x7)))))."?
Can you please invent a name for the term defined by " (fun x0 : set => and (struct_b_b_e_e x0) (unpack_b_b_e_e_o x0 (fun x1 : set => fun x2 x3 : set -> set -> set => fun x4 x5 : set => and (and (and (and (and (and (and (and (forall x6, x6 :e x1 -> (forall x7, x7 :e x1 -> (forall x8, x8 :e x1 -> x2 (x2 x6 x7) x8 = x2 x6 (x2 x7 x8)))) (forall x6, x6 :e x1 -> (forall x7, x7 :e x1 -> x2 x6 x7 = x2 x7 x6))) (forall x6, x6 :e x1 -> x2 x6 x4 = x6)) (forall x6, x6 :e x1 -> (forall x7, x7 :e x1 -> (forall x8, x8 :e x1 -> x3 (x3 x6 x7) x8 = x3 x6 (x3 x7 x8))))) (forall x6, x6 :e x1 -> and (x3 x6 x5 = x6) (x3 x5 x6 = x6))) (forall x6, x6 :e x1 -> (forall x7, x7 :e x1 -> (forall x8, x8 :e x1 -> x3 x6 (x2 x7 x8) = x2 (x3 x6 x7) (x3 x6 x8))))) (forall x6, x6 :e x1 -> (forall x7, x7 :e x1 -> (forall x8, x8 :e x1 -> x3 (x2 x6 x7) x8 = x2 (x3 x6 x8) (x3 x7 x8))))) (forall x6, x6 :e x1 -> x3 x6 x4 = x4)) (forall x6, x6 :e x1 -> x3 x4 x6 = x4))))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x2 x3 : set => x0 (x1 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3 x2) (x1 x2 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3) (x1 x3 x2 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3 x3) (x1 x3 x3 x2 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3) (x1 x3 x3 x3 x2 x3 x2 x3 x3 x3 x2 x3 x3 x2) (x1 x2 x3 x3 x3 x2 x3 x2 x3 x3 x3 x2 x3 x3) (x1 x3 x2 x3 x3 x3 x2 x3 x2 x3 x3 x3 x2 x3) (x1 x3 x3 x2 x3 x3 x3 x2 x3 x2 x3 x3 x3 x2) (x1 x2 x3 x3 x2 x3 x3 x3 x2 x3 x2 x3 x3 x3) (x1 x3 x2 x3 x3 x2 x3 x3 x3 x2 x3 x2 x3 x3) (x1 x3 x3 x2 x3 x3 x2 x3 x3 x3 x2 x3 x2 x3) (x1 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3 x2 x3 x2) (x1 x2 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3 x2 x3))."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => forall x1 : (set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set) -> prop, x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x2) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x3) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x4) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x5) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x6) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x7) -> x1 x0)."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 : (set -> set) -> set -> set => x0 x1 x8 x7 x6 x5 x4 x3 x2)."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 : (set -> set) -> set -> set => x0 x5 x6 x7 x8 x1 x2 x3 x4)."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 : (set -> set) -> set -> set => x0 x6 x7 x8 x1 x2 x3 x4 x5)."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 : (set -> set) -> set -> set => x0 x4 x5 x6 x7 x8 x1 x2 x3)."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 : (set -> set) -> set -> set => x0 x7 x8 x1 x2 x3 x4 x5 x6)."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 : (set -> set) -> set -> set => x0 x3 x4 x5 x6 x7 x8 x1 x2)."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 : (set -> set) -> set -> set => x0 x8 x1 x2 x3 x4 x5 x6 x7)."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 x2 x3 x4 x5 x6 x7 x8 : (set -> set) -> set -> set => x0 x2 x3 x4 x5 x6 x7 x8 x1)."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 : set => forall x4 : (set -> set -> set) -> (set -> set -> set) -> prop, x4 (missingname_e4c128d492933589c3cc92b565612fcec0e08141b66eea664bfaaeae59632b46 (missingname_d45c1fe6a3dff7795ce0a3b891aea8946efc8dceebae3c8b8977b41878b0e841 x0) (missingname_d45c1fe6a3dff7795ce0a3b891aea8946efc8dceebae3c8b8977b41878b0e841 x1) (missingname_d45c1fe6a3dff7795ce0a3b891aea8946efc8dceebae3c8b8977b41878b0e841 x2) (missingname_d45c1fe6a3dff7795ce0a3b891aea8946efc8dceebae3c8b8977b41878b0e841 x3)) (fun x5 x6 : set => x5) -> x4 (fun x5 x6 : set => x5) (missingname_e4c128d492933589c3cc92b565612fcec0e08141b66eea664bfaaeae59632b46 (missingname_d45c1fe6a3dff7795ce0a3b891aea8946efc8dceebae3c8b8977b41878b0e841 x0) (missingname_d45c1fe6a3dff7795ce0a3b891aea8946efc8dceebae3c8b8977b41878b0e841 x1) (missingname_d45c1fe6a3dff7795ce0a3b891aea8946efc8dceebae3c8b8977b41878b0e841 x2) (missingname_d45c1fe6a3dff7795ce0a3b891aea8946efc8dceebae3c8b8977b41878b0e841 x3)))."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set -> set -> set -> set -> set -> set) -> (set -> set -> set -> set -> set -> set -> set) -> set -> set -> set -> set -> set -> set -> set) -> set -> set -> set -> set -> set -> set -> set => forall x1 : (((set -> set -> set -> set -> set -> set -> set) -> (set -> set -> set -> set -> set -> set -> set) -> set -> set -> set -> set -> set -> set -> set) -> set -> set -> set -> set -> set -> set -> set) -> prop, (forall x2 x3 : set -> set -> set -> set -> set -> set -> set, missingname_d09d227a13baf82dd9fb97506200eec56009ace6e9b5e539a544c04594b1dd10 x2 -> missingname_d09d227a13baf82dd9fb97506200eec56009ace6e9b5e539a544c04594b1dd10 x3 -> x1 (fun x4 : (set -> set -> set -> set -> set -> set -> set) -> (set -> set -> set -> set -> set -> set -> set) -> set -> set -> set -> set -> set -> set -> set => x4 x2 x3)) -> x1 x0)."?
Can you please invent a name for the term defined by " (fun x0 : (set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set) -> prop => and (and (and (and (and (and (and (and (and (x0 missingname_9ed94aa81a158cf2838b6e3347c1d83280a2b37914d5c7e246ff38b5b0751101) (x0 missingname_0160cbd5f03b772c32962cff610c8ff61ac71013d4cb8a0f43c138227821e0d7)) (x0 missingname_dd7c6467b10f0145b66f29abbf2003c9c65288ed1148798a2ca697bd78065b3d)) (x0 missingname_677bc60a8fdcf643e080cc574e7493ee36a94ad607a880f86aa31eca9c2a20b2)) (x0 missingname_08160c37a1ab38c2a8741bd21f5d85ae4e1ecc1f471131813ac76a14df5e34ca)) (x0 missingname_e29e8aa444e52a9aff7677b4a659f06cce7015e180359810492b097b9052d91c)) (x0 missingname_c5c365fe7c2d693786824197d1c188164cd70a1ba3bdae2dd2c5d26dbadee658)) (x0 missingname_f8849ca3b750d3ad38db8e876e60e1fed4c255e45fb4a9e6dda634e638c9b9ae)) (x0 missingname_0563ecdd0f6df49f087d7271b4758716802ec79d849b006b520dcdac44c56ddb)) (x0 missingname_af9da978aa7b87cdab764777559ede69d9aea6f76d01b4a0eebdc7c271c36d40))."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => forall x1 : (set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set) -> prop, x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x2) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x3) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x4) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x5) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x6) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x7) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x8) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x9) -> x1 x0)."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x2 x3 x4 : (set -> set) -> set -> set => x0 (x1 x2 x4 x4 x4 x4 x4 x4 x4) (x1 x4 x3 x3 x3 x3 x3 x3 x3) (x1 x3 x2 x2 x2 x2 x2 x2 x2))."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x2 x3 x4 : (set -> set) -> set -> set => x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x4 x2 x3))."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x2 x3 x4 : (set -> set) -> set -> set => x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x4 x2 x3) (x1 x4 x2 x3))."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x2 x3 x4 : (set -> set) -> set -> set => x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3))."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x2 x3 x4 : (set -> set) -> set -> set => x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3))."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x2 x3 x4 : (set -> set) -> set -> set => x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3))."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x2 x3 x4 : (set -> set) -> set -> set => x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3))."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x2 x3 x4 : (set -> set) -> set -> set => x0 (x1 x2 x3 x4) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3))."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x2 x3 x4 : (set -> set) -> set -> set => x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2))."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x2 x3 x4 : (set -> set) -> set -> set => x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2))."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x2 x3 x4 : (set -> set) -> set -> set => x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2))."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x2 x3 x4 : (set -> set) -> set -> set => x0 (x1 x2 x3 x4) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2))."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x2 x3 x4 : (set -> set) -> set -> set => x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x3 x4 x2))."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x2 x3 x4 : (set -> set) -> set -> set => x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x3 x4 x2) (x1 x3 x4 x2))."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x2 x3 x4 : (set -> set) -> set -> set => x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2))."?
Can you please invent a name for the term defined by " (fun x0 x1 : (set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set) -> (set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set) -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x2 x3 x4 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => x1 (x0 (x0 x4 x2) x3) (x0 x2 x3))."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => forall x1 : (set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set) -> prop, x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : set => x2) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : set => x3) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : set => x4) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : set => x5) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : set => x6) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : set => x7) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : set => x8) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : set => x9) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : set => x10) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : set => x11) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : set => x12) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : set => x13) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : set => x14) -> x1 x0)."?
Can you please invent a name for the term defined by " (fun x0 x1 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x2 x3 : set => x0 (x1 x3 x2 x2 x3 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3 x3 x2 x3) (x1 x2 x3 x3 x2 x3 x3 x2 x3 x3 x3 x3 x2 x2 x3 x3 x3 x3) (x1 x2 x3 x3 x2 x3 x2 x3 x3 x2 x3 x3 x3 x3 x3 x2 x3 x3) (x1 x3 x2 x2 x3 x2 x3 x3 x3 x3 x2 x3 x3 x3 x2 x3 x3 x3) (x1 x3 x3 x3 x2 x3 x2 x2 x3 x3 x3 x2 x3 x3 x3 x3 x2 x3) (x1 x3 x3 x2 x3 x2 x3 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x3) (x1 x3 x2 x3 x3 x2 x3 x3 x2 x2 x3 x3 x3 x3 x3 x2 x3 x3) (x1 x2 x3 x3 x3 x3 x2 x2 x3 x3 x2 x3 x3 x3 x2 x3 x3 x3) (x1 x3 x3 x2 x3 x3 x3 x2 x3 x3 x3 x3 x2 x2 x2 x3 x3 x3) (x1 x3 x3 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3 x2 x3 x3 x2 x3) (x1 x2 x3 x3 x3 x2 x3 x3 x3 x3 x2 x3 x3 x3 x2 x2 x3 x3) (x1 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3 x3 x3 x2 x2 x3) (x1 x3 x2 x3 x3 x3 x2 x3 x3 x2 x2 x3 x3 x3 x3 x3 x3 x2) (x1 x3 x3 x3 x2 x3 x3 x3 x2 x2 x3 x2 x3 x3 x3 x3 x3 x2) (x1 x3 x3 x2 x3 x3 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x3 x2) (x1 x2 x3 x3 x3 x2 x3 x3 x3 x3 x2 x3 x2 x3 x3 x3 x3 x2) (x1 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x2 x2 x2 x2 x3))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x2 x3 : set => x0 (x1 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2) (x1 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2) (x1 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3) (x1 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2) (x1 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3) (x1 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3) (x1 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3) (x1 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2) (x1 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2) (x1 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3) (x1 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3) (x1 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3) (x1 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2) (x1 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3) (x1 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2) (x1 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2) (x1 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3))."?
Can you please invent a name for the term defined by " (fun x0 x1 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x2 x3 : set => x0 (x1 x2 x2 x2 x3 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3 x3 x2 x3) (x1 x2 x2 x3 x2 x3 x3 x2 x3 x3 x3 x3 x2 x2 x3 x3 x3 x3) (x1 x2 x3 x2 x2 x3 x2 x3 x3 x2 x3 x3 x3 x3 x3 x2 x3 x3) (x1 x3 x2 x2 x2 x2 x3 x3 x3 x3 x2 x3 x3 x3 x2 x3 x3 x3) (x1 x3 x3 x3 x2 x2 x2 x2 x3 x3 x3 x2 x3 x3 x3 x3 x2 x3) (x1 x3 x3 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x3) (x1 x3 x2 x3 x3 x2 x3 x2 x2 x2 x3 x3 x3 x3 x3 x2 x3 x3) (x1 x2 x3 x3 x3 x3 x2 x2 x2 x3 x2 x3 x3 x3 x2 x3 x3 x3) (x1 x3 x3 x2 x3 x3 x3 x2 x3 x2 x3 x3 x2 x2 x2 x3 x3 x3) (x1 x3 x3 x3 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x3 x3 x2 x3) (x1 x2 x3 x3 x3 x2 x3 x3 x3 x3 x2 x2 x3 x3 x2 x2 x3 x3) (x1 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3 x3 x2 x3 x3 x2 x2 x3) (x1 x3 x2 x3 x3 x3 x2 x3 x3 x2 x2 x3 x3 x2 x3 x3 x3 x2) (x1 x3 x3 x3 x2 x3 x3 x3 x2 x2 x3 x2 x3 x3 x2 x3 x3 x2) (x1 x3 x3 x2 x3 x3 x3 x2 x3 x3 x3 x2 x2 x3 x3 x2 x3 x2) (x1 x2 x3 x3 x3 x2 x3 x3 x3 x3 x2 x3 x2 x3 x3 x3 x2 x2) (x1 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x2 x2 x2 x2 x2))."?
Can you please invent a name for the term defined by " (fun x0 : set -> prop => fun x1 : (set -> prop) -> prop => fun x2 : (set -> set -> prop) -> prop => fun x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 : set => fun x17 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x18 : set -> set -> set => fun x19 : set => x18 (x18 (x17 (x17 x3 x5 x4 x6 x8 x7 x15 x11 x10 x12 x16 x14 x9 x13) (x17 x4 x3 x13 x10 x16 x9 x8 x6 x15 x14 x5 x12 x11 x7) (x17 x5 x15 x3 x11 x12 x8 x14 x16 x6 x7 x13 x9 x4 x10) (x17 x6 x14 x11 x3 x9 x16 x7 x13 x5 x15 x10 x4 x12 x8) (x17 x7 x12 x10 x9 x3 x13 x6 x5 x16 x4 x8 x15 x14 x11) (x17 x8 x9 x14 x13 x11 x3 x4 x12 x7 x10 x6 x5 x16 x15) (x17 x9 x16 x8 x7 x6 x5 x3 x15 x14 x13 x12 x11 x10 x4) (x17 x10 x13 x12 x8 x14 x6 x16 x3 x11 x5 x4 x7 x15 x9) (x17 x11 x4 x9 x12 x15 x10 x5 x8 x3 x6 x14 x13 x7 x16) (x17 x12 x7 x16 x14 x4 x11 x10 x9 x8 x3 x15 x6 x13 x5) (x17 x13 x8 x7 x15 x5 x4 x9 x10 x12 x11 x3 x16 x6 x14) (x17 x14 x10 x6 x5 x13 x15 x11 x4 x9 x16 x7 x3 x8 x12) (x17 x15 x11 x5 x16 x7 x12 x13 x14 x4 x8 x9 x10 x3 x6) (x17 x16 x6 x15 x4 x10 x14 x12 x7 x13 x9 x11 x8 x5 x3)) x19))."?
Can you please invent a name for the term defined by " (fun x0 : set -> prop => fun x1 : (set -> prop) -> prop => fun x2 : (set -> set -> prop) -> prop => fun x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 : set => fun x17 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x18 : set -> set -> set => fun x19 : set => x18 (x18 (x17 (x17 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) (x17 x4 x11 x3 x16 x12 x13 x8 x14 x15 x7 x10 x6 x5 x9) (x17 x5 x3 x15 x14 x13 x9 x11 x7 x6 x10 x4 x8 x16 x12) (x17 x6 x16 x14 x3 x9 x10 x7 x4 x5 x11 x8 x12 x13 x15) (x17 x7 x12 x13 x9 x15 x3 x6 x16 x8 x5 x14 x10 x11 x4) (x17 x8 x13 x9 x10 x3 x5 x4 x11 x12 x15 x7 x16 x14 x6) (x17 x9 x8 x11 x7 x6 x4 x13 x12 x14 x16 x15 x5 x3 x10) (x17 x10 x14 x7 x4 x16 x11 x12 x13 x3 x8 x6 x15 x9 x5) (x17 x11 x15 x6 x5 x8 x12 x14 x3 x10 x13 x16 x9 x4 x7) (x17 x12 x7 x10 x11 x5 x15 x16 x8 x13 x3 x9 x4 x6 x14) (x17 x13 x10 x4 x8 x14 x7 x15 x6 x16 x9 x5 x11 x12 x3) (x17 x14 x6 x8 x12 x10 x16 x5 x15 x9 x4 x11 x3 x7 x13) (x17 x15 x5 x16 x13 x11 x14 x3 x9 x4 x6 x12 x7 x10 x8) (x17 x16 x9 x12 x15 x4 x6 x10 x5 x7 x14 x3 x13 x8 x11)) x19))."?
Can you please invent a name for the term defined by " (fun x0 : (((((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> set -> set -> set => missingname_ebd1166cec90389df647753858049cc6fd98aabc3fb4fd2dca22ac79311d7847 (fun x1 : ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => missingname_ebd1166cec90389df647753858049cc6fd98aabc3fb4fd2dca22ac79311d7847 (fun x2 : ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x0 (fun x3 : (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x3 x1 x2))))."?
Can you please invent a name for the term defined by " (fun x0 : (((((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> set -> set -> set => missingname_aac1c284a47e5dd485b71b33f9d5736b411bb6383a9586a9ba39ad5e68f28afa (fun x1 : ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => missingname_aac1c284a47e5dd485b71b33f9d5736b411bb6383a9586a9ba39ad5e68f28afa (fun x2 : ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x0 (fun x3 : (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x3 x1 x2))))."?
Can you please invent a name for the term defined by " (fun x0 : ((((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => and (and (x0 = (fun x2 : (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x2 (x0 (fun x3 x4 : ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x3)) (x0 (fun x3 x4 : ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x4)))) (missingname_39fd9549c17bb512eb0f99b47ad27071bb34f5e0d246d1966322bbecfcadbab8 (x0 (fun x1 x2 : ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x1)))) (missingname_39fd9549c17bb512eb0f99b47ad27071bb34f5e0d246d1966322bbecfcadbab8 (x0 (fun x1 x2 : ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x2))))."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x1 x2 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => fun x3 x4 : set => x1 (x2 x4 x3 x3 x4 x4 x4 x4 x3 x4 x4 x3 x4 x4 x4 x4 x3 x4) (x2 x3 x4 x4 x3 x4 x4 x3 x4 x4 x4 x4 x3 x3 x4 x4 x4 x4) (x2 x3 x4 x4 x3 x4 x3 x4 x4 x3 x4 x4 x4 x4 x4 x3 x4 x4) (x2 x4 x3 x3 x4 x3 x4 x4 x4 x4 x3 x4 x4 x4 x3 x4 x4 x4) (x2 x4 x4 x4 x3 x4 x3 x3 x4 x4 x4 x3 x4 x4 x4 x4 x3 x4) (x2 x4 x4 x3 x4 x3 x4 x4 x3 x4 x4 x4 x3 x3 x4 x4 x4 x4) (x2 x4 x3 x4 x4 x3 x4 x4 x3 x3 x4 x4 x4 x4 x4 x3 x4 x4) (x2 x3 x4 x4 x4 x4 x3 x3 x4 x4 x3 x4 x4 x4 x3 x4 x4 x4) (x2 x4 x4 x3 x4 x4 x4 x3 x4 x4 x4 x4 x3 x3 x3 x4 x4 x4) (x2 x4 x4 x4 x3 x4 x4 x4 x3 x4 x4 x3 x4 x3 x4 x4 x3 x4) (x2 x3 x4 x4 x4 x3 x4 x4 x4 x4 x3 x4 x4 x4 x3 x3 x4 x4) (x2 x4 x3 x4 x4 x4 x3 x4 x4 x3 x4 x4 x4 x4 x4 x3 x3 x4) (x2 x4 x3 x4 x4 x4 x3 x4 x4 x3 x3 x4 x4 x4 x4 x4 x4 x3) (x2 x4 x4 x4 x3 x4 x4 x4 x3 x3 x4 x3 x4 x4 x4 x4 x4 x3) (x2 x4 x4 x3 x4 x4 x4 x3 x4 x4 x4 x3 x3 x4 x4 x4 x4 x3) (x2 x3 x4 x4 x4 x3 x4 x4 x4 x4 x3 x4 x3 x4 x4 x4 x4 x3) (x2 x4 x4 x4 x4 x4 x4 x4 x4 x4 x4 x4 x4 x3 x3 x3 x3 x4))."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x2 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x3 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => and (x0 = x2) (x1 = x3))."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x2 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x3 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => not (missingname_12a33904568297deaf1153b453b55716649c42ac90ce8657680c698f26a9f0f0 x0 x1 x2 x3))."?
Can you please invent a name for the term defined by " (fun x0 x1 : ((((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> (((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set) -> ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => missingname_792d152efe262dcaabf368bc6467ac057697a53fc33616f54269226b8862b39f (missingname_e705adc25b2512365394b0e25f155fbe016b3b60511bfca72bbcceb2dfdbf19d (x0 (fun x2 x3 : ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x2)) (x1 (fun x2 x3 : ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x2))) (missingname_e705adc25b2512365394b0e25f155fbe016b3b60511bfca72bbcceb2dfdbf19d (x0 (fun x2 x3 : ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x3)) (x1 (fun x2 x3 : ((set -> set -> set) -> (set -> set -> set) -> set -> set -> set) -> set -> set -> set => x3))))."?
Can you please invent a name for the term defined by " (fun x0 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => forall x1 : (set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set) -> prop, x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x2) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x3) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x4) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x5) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x6) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x7) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x8) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x9) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x10) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x11) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x12) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x13) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x14) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x15) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x16) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x17) -> x1 (fun x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 : set => x18) -> x1 x0)."?
Can you please invent a name for the term defined by " (fun x0 x1 : set => forall x2 x3 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set, forall x4 x5 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set, ChurchNum_3ary_proj_p x2 -> ChurchNum_3ary_proj_p x3 -> ChurchNum_8ary_proj_p x4 -> ChurchNum_8ary_proj_p x5 -> x0 = x2 (fun x7 : set -> set => fun x8 : set => x8) (fun x7 : set -> set => fun x8 : set => x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 x8)))))))) (fun x7 : set -> set => fun x8 : set => x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 x8)))))))))))))))) ordsucc (x4 (fun x7 : set -> set => fun x8 : set => x8) (fun x7 : set -> set => x7) (fun x7 : set -> set => fun x8 : set => x7 (x7 x8)) (fun x7 : set -> set => fun x8 : set => x7 (x7 (x7 x8))) (fun x7 : set -> set => fun x8 : set => x7 (x7 (x7 (x7 x8)))) (fun x7 : set -> set => fun x8 : set => x7 (x7 (x7 (x7 (x7 x8))))) (fun x7 : set -> set => fun x8 : set => x7 (x7 (x7 (x7 (x7 (x7 x8)))))) (fun x7 : set -> set => fun x8 : set => x7 (x7 (x7 (x7 (x7 (x7 (x7 x8))))))) ordsucc 0) -> x1 = x3 (fun x7 : set -> set => fun x8 : set => x8) (fun x7 : set -> set => fun x8 : set => x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 x8)))))))) (fun x7 : set -> set => fun x8 : set => x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 x8)))))))))))))))) ordsucc (x5 (fun x7 : set -> set => fun x8 : set => x8) (fun x7 : set -> set => x7) (fun x7 : set -> set => fun x8 : set => x7 (x7 x8)) (fun x7 : set -> set => fun x8 : set => x7 (x7 (x7 x8))) (fun x7 : set -> set => fun x8 : set => x7 (x7 (x7 (x7 x8)))) (fun x7 : set -> set => fun x8 : set => x7 (x7 (x7 (x7 (x7 x8))))) (fun x7 : set -> set => fun x8 : set => x7 (x7 (x7 (x7 (x7 (x7 x8)))))) (fun x7 : set -> set => fun x8 : set => x7 (x7 (x7 (x7 (x7 (x7 (x7 x8))))))) ordsucc 0) -> missingname_f15783baeb7e85a1ff545f53d5ddb4c43d32933da197ebc12c53bd1d42508ff9 x2 x4 x3 x5 = (fun x7 x8 : set => x7))."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => x0 (x1 (fun x2 : set -> set => fun x3 : set => x3) (fun x2 : set -> set => x2) (fun x2 : set -> set => fun x3 : set => x2 (x2 x3)) (fun x2 : set -> set => fun x3 : set => x2 (x2 (x2 x3))) (fun x2 : set -> set => fun x3 : set => x2 (x2 (x2 (x2 x3)))) (fun x2 : set -> set => fun x3 : set => x2 (x2 (x2 (x2 (x2 x3))))) (fun x2 : set -> set => fun x3 : set => x2 (x2 (x2 (x2 (x2 (x2 x3)))))) (fun x2 : set -> set => fun x3 : set => x2 (x2 (x2 (x2 (x2 (x2 (x2 x3)))))))) (fun x2 : set -> set => fun x3 : set => x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x1 (fun x4 : set -> set => fun x5 : set => x5) (fun x4 : set -> set => x4) (fun x4 : set -> set => fun x5 : set => x4 (x4 x5)) (fun x4 : set -> set => fun x5 : set => x4 (x4 (x4 x5))) (fun x4 : set -> set => fun x5 : set => x4 (x4 (x4 (x4 x5)))) (fun x4 : set -> set => fun x5 : set => x4 (x4 (x4 (x4 (x4 x5))))) (fun x4 : set -> set => fun x5 : set => x4 (x4 (x4 (x4 (x4 (x4 x5)))))) (fun x4 : set -> set => fun x5 : set => x4 (x4 (x4 (x4 (x4 (x4 (x4 x5))))))) x2 x3))))))))) (fun x2 : set -> set => fun x3 : set => x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x1 (fun x4 : set -> set => fun x5 : set => x5) (fun x4 : set -> set => x4) (fun x4 : set -> set => fun x5 : set => x4 (x4 x5)) (fun x4 : set -> set => fun x5 : set => x4 (x4 (x4 x5))) (fun x4 : set -> set => fun x5 : set => x4 (x4 (x4 (x4 x5)))) (fun x4 : set -> set => fun x5 : set => x4 (x4 (x4 (x4 (x4 x5))))) (fun x4 : set -> set => fun x5 : set => x4 (x4 (x4 (x4 (x4 (x4 x5)))))) (fun x4 : set -> set => fun x5 : set => x4 (x4 (x4 (x4 (x4 (x4 (x4 x5))))))) x2 x3))))))))))))))))) ordsucc 0)."?
Can you please invent a name for the term defined by " (fun x0 x1 : (set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set) -> (set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set) -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => and (and (and (missingname_a8d4cefd4df688d41b5c1b67b444fe845da4239aaa45044c26a0f587c440c03b (fun x2 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => forall x3 : (set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set) -> (set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set) -> prop, x3 (x0 x2 missingname_9ed94aa81a158cf2838b6e3347c1d83280a2b37914d5c7e246ff38b5b0751101) x2 -> x3 x2 (x0 x2 missingname_9ed94aa81a158cf2838b6e3347c1d83280a2b37914d5c7e246ff38b5b0751101))) (missingname_e79a2247a94350fc96d40568c9883e01665d4c1aa8e6fe0ca2b7cdd48cfeeca0 (fun x2 x3 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => forall x4 : (set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set) -> (set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set) -> prop, x4 (x0 x2 x3) (x0 x3 x2) -> x4 (x0 x3 x2) (x0 x2 x3)))) (missingname_a8d4cefd4df688d41b5c1b67b444fe845da4239aaa45044c26a0f587c440c03b (fun x2 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => missingname_a8d4cefd4df688d41b5c1b67b444fe845da4239aaa45044c26a0f587c440c03b (fun x3 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => forall x4 : (set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set) -> (set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set) -> prop, x4 (x0 (x1 x2 x3) x3) x2 -> x4 x2 (x0 (x1 x2 x3) x3))))) (missingname_a8d4cefd4df688d41b5c1b67b444fe845da4239aaa45044c26a0f587c440c03b (fun x2 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => missingname_a8d4cefd4df688d41b5c1b67b444fe845da4239aaa45044c26a0f587c440c03b (fun x3 : set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set => forall x4 : (set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set) -> (set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set) -> prop, x4 (x1 (x0 x2 x3) x3) x2 -> x4 x2 (x1 (x0 x2 x3) x3)))))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 : set -> set -> set -> set -> set -> set -> set => fun x4 x5 : set => x0 (x1 (x2 (x3 x4 x5 x4 x5 x4 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x5 x4 x4 x4 x5) (x3 x5 x4 x4 x5 x4 x5) (x3 x5 x5 x4 x4 x5 x5) (x3 x4 x5 x4 x4 x5 x4)) (x2 (x3 x5 x4 x5 x4 x5 x4) (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x5 x4 x4 x5 x4) (x3 x4 x5 x5 x4 x5 x4) (x3 x5 x5 x4 x4 x5 x5) (x3 x5 x4 x4 x4 x5 x4)) (x2 (x3 x4 x5 x4 x5 x5 x4) (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x4 x5 x5 x4 x5 x4) (x3 x4 x4 x5 x5 x5 x5) (x3 x4 x4 x4 x5 x5 x4)) (x2 (x3 x5 x4 x5 x4 x4 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x4 x4 x5 x4 x5) (x3 x4 x4 x5 x5 x5 x5) (x3 x4 x4 x5 x4 x5 x4)) (x2 (x3 x4 x5 x5 x4 x4 x5) (x3 x5 x4 x4 x5 x5 x5) (x3 x4 x5 x5 x4 x4 x4) (x3 x4 x5 x5 x4 x4 x4) (x3 x5 x4 x4 x5 x5 x5) (x3 x5 x5 x5 x5 x4 x4)) (x2 (x3 x5 x4 x4 x5 x5 x4) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x4 x4 x5 x4 x4) (x3 x5 x4 x4 x5 x4 x4) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x5 x5 x5 x4 x4))) (x1 (x2 (x3 x4 x4 x5 x5 x5 x4) (x3 x4 x5 x4 x5 x5 x4) (x3 x4 x5 x5 x5 x4 x5) (x3 x5 x4 x4 x4 x4 x5) (x3 x5 x4 x4 x5 x5 x4) (x3 x5 x4 x5 x5 x5 x4)) (x2 (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x4 x5 x4 x4 x5) (x3 x5 x4 x5 x5 x5 x4) (x3 x4 x5 x4 x4 x5 x4) (x3 x4 x5 x5 x4 x4 x5) (x3 x4 x5 x5 x5 x5 x4)) (x2 (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x5 x4 x5 x5 x4) (x3 x5 x5 x4 x5 x4 x5) (x3 x4 x4 x5 x4 x5 x4) (x3 x4 x5 x5 x4 x5 x4) (x3 x5 x5 x5 x4 x5 x4)) (x2 (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x4 x5 x4 x4 x5) (x3 x5 x5 x5 x4 x5 x4) (x3 x4 x4 x4 x5 x4 x5) (x3 x5 x4 x4 x5 x4 x5) (x3 x5 x5 x4 x5 x5 x4)) (x2 (x3 x4 x5 x4 x5 x5 x5) (x3 x5 x4 x5 x4 x4 x4) (x3 x5 x4 x5 x4 x5 x5) (x3 x5 x5 x5 x5 x4 x4) (x3 x5 x5 x5 x5 x5 x4) (x3 x5 x4 x5 x4 x4 x4)) (x2 (x3 x5 x4 x5 x4 x5 x5) (x3 x4 x5 x4 x5 x4 x4) (x3 x4 x5 x4 x5 x5 x5) (x3 x5 x5 x5 x5 x4 x4) (x3 x5 x5 x5 x5 x4 x5) (x3 x4 x5 x4 x5 x4 x4))) (x1 (x2 (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x5 x5 x5 x5 x4) (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x4 x4 x5 x5 x4) (x3 x5 x5 x4 x4 x5 x5) (x3 x5 x5 x4 x5 x4 x4)) (x2 (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x4 x5 x5 x4 x5) (x3 x4 x4 x5 x5 x5 x4) (x3 x4 x5 x5 x4 x4 x5) (x3 x5 x5 x4 x4 x5 x5) (x3 x5 x5 x5 x4 x4 x4)) (x2 (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x5 x4 x5 x5 x4) (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x5 x5 x4 x4 x5) (x3 x4 x4 x5 x5 x5 x5) (x3 x4 x5 x5 x5 x4 x4)) (x2 (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x5 x5 x4 x4 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x4 x4 x5 x5 x4) (x3 x4 x4 x5 x5 x5 x5) (x3 x5 x4 x5 x5 x4 x4)) (x2 (x3 x4 x5 x4 x5 x4 x4) (x3 x4 x5 x4 x5 x5 x5) (x3 x4 x5 x4 x5 x4 x4) (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x4 x5 x4 x5 x5) (x3 x5 x5 x5 x5 x5 x4)) (x2 (x3 x5 x4 x5 x4 x4 x4) (x3 x5 x4 x5 x4 x5 x5) (x3 x5 x4 x5 x4 x4 x4) (x3 x5 x5 x5 x5 x5 x5) (x3 x4 x5 x4 x5 x5 x5) (x3 x5 x5 x5 x5 x5 x4))) (x1 (x2 (x3 x5 x4 x4 x5 x4 x5) (x3 x5 x4 x4 x4 x5 x5) (x3 x5 x4 x4 x5 x5 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x5 x4 x5 x5 x4) (x3 x4 x4 x5 x5 x4 x4)) (x2 (x3 x4 x5 x5 x4 x5 x4) (x3 x4 x5 x4 x4 x5 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x5 x5 x4 x4 x5) (x3 x4 x4 x5 x5 x4 x4)) (x2 (x3 x4 x5 x5 x4 x5 x4) (x3 x4 x4 x5 x4 x5 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x4 x5 x5 x5 x5 x4) (x3 x5 x5 x4 x4 x4 x4)) (x2 (x3 x5 x4 x4 x5 x4 x5) (x3 x4 x4 x4 x5 x5 x5) (x3 x5 x4 x4 x5 x5 x5) (x3 x5 x5 x4 x4 x4 x5) (x3 x5 x4 x5 x5 x4 x5) (x3 x5 x5 x4 x4 x4 x4)) (x2 (x3 x4 x5 x5 x4 x4 x4) (x3 x4 x5 x5 x4 x4 x4) (x3 x5 x4 x4 x5 x5 x5) (x3 x4 x5 x5 x4 x4 x5) (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x4 x4 x5 x5 x4)) (x2 (x3 x5 x4 x4 x5 x4 x4) (x3 x5 x4 x4 x5 x4 x4) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x4 x4 x5 x5 x4) (x3 x5 x5 x5 x5 x5 x5) (x3 x4 x5 x5 x4 x5 x4))) (x1 (x2 (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x4 x4 x5 x5 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x5 x4 x5 x5 x5) (x3 x4 x5 x4 x4 x5 x4) (x3 x4 x4 x5 x5 x5 x4)) (x2 (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x5 x4 x4 x4 x5) (x3 x5 x5 x5 x4 x5 x5) (x3 x5 x4 x4 x4 x4 x5) (x3 x4 x4 x5 x5 x5 x4)) (x2 (x3 x4 x4 x5 x5 x4 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x4 x4 x5 x5 x5 x4) (x3 x4 x5 x5 x5 x5 x5) (x3 x4 x4 x4 x5 x5 x4) (x3 x5 x5 x4 x4 x5 x4)) (x2 (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x4 x4 x5 x5 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x4 x5 x5 x5 x5) (x3 x4 x4 x5 x4 x4 x5) (x3 x5 x5 x4 x4 x5 x4)) (x2 (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x4 x5 x4 x5 x4) (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x4 x5 x4 x5 x5) (x3 x5 x4 x5 x4 x4 x5) (x3 x4 x4 x4 x4 x4 x4)) (x2 (x3 x5 x5 x5 x5 x5 x5) (x3 x4 x5 x4 x5 x4 x5) (x3 x5 x5 x5 x5 x5 x5) (x3 x4 x5 x4 x5 x5 x5) (x3 x4 x5 x4 x5 x5 x4) (x3 x4 x4 x4 x4 x4 x4))) (x1 (x2 (x3 x4 x5 x4 x4 x5 x5) (x3 x5 x4 x5 x5 x5 x4) (x3 x5 x5 x4 x5 x5 x5) (x3 x4 x4 x5 x5 x5 x4) (x3 x4 x4 x5 x5 x4 x4) (x3 x4 x5 x5 x4 x5 x4)) (x2 (x3 x5 x4 x4 x4 x5 x5) (x3 x4 x5 x5 x5 x4 x5) (x3 x5 x5 x5 x4 x5 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x4 x4 x5 x5 x4 x4) (x3 x5 x4 x4 x5 x5 x4)) (x2 (x3 x4 x4 x4 x5 x5 x5) (x3 x5 x5 x5 x4 x5 x4) (x3 x4 x5 x5 x5 x5 x5) (x3 x5 x5 x4 x4 x4 x5) (x3 x5 x5 x4 x4 x4 x4) (x3 x5 x4 x4 x5 x5 x4)) (x2 (x3 x4 x4 x5 x4 x5 x5) (x3 x5 x5 x4 x5 x4 x5) (x3 x5 x4 x5 x5 x5 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x5 x4 x4 x4 x4) (x3 x4 x5 x5 x4 x5 x4)) (x2 (x3 x5 x5 x5 x5 x4 x4) (x3 x5 x5 x5 x5 x4 x4) (x3 x4 x4 x4 x4 x5 x5) (x3 x4 x4 x4 x4 x5 x5) (x3 x5 x5 x5 x5 x4 x4) (x3 x5 x5 x5 x5 x4 x4)) (x2 (x3 x4 x4 x4 x4 x4 x4) (x3 x4 x4 x4 x4 x4 x4) (x3 x4 x4 x4 x4 x4 x4) (x3 x4 x4 x4 x4 x4 x4) (x3 x4 x4 x4 x4 x4 x4) (x3 x4 x4 x4 x4 x4 x4))))."?
Can you please invent a name for the term defined by " (fun x0 x1 x2 x3 : set -> set -> set -> set -> set -> set -> set => fun x4 x5 : set => x0 (x1 (x2 (x3 x5 x5 x4 x5 x4 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x5 x4 x4 x4 x5) (x3 x5 x4 x4 x5 x4 x5) (x3 x5 x5 x4 x4 x5 x5) (x3 x4 x5 x4 x4 x5 x5)) (x2 (x3 x5 x5 x5 x4 x5 x4) (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x5 x4 x4 x5 x4) (x3 x4 x5 x5 x4 x5 x4) (x3 x5 x5 x4 x4 x5 x5) (x3 x5 x4 x4 x4 x5 x5)) (x2 (x3 x4 x5 x5 x5 x5 x4) (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x4 x5 x5 x4 x5 x4) (x3 x4 x4 x5 x5 x5 x5) (x3 x4 x4 x4 x5 x5 x5)) (x2 (x3 x5 x4 x5 x5 x4 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x4 x4 x5 x4 x5) (x3 x4 x4 x5 x5 x5 x5) (x3 x4 x4 x5 x4 x5 x5)) (x2 (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x4 x4 x5 x5 x5) (x3 x4 x5 x5 x4 x4 x4) (x3 x4 x5 x5 x4 x4 x4) (x3 x5 x4 x4 x5 x5 x5) (x3 x5 x5 x5 x5 x4 x5)) (x2 (x3 x5 x4 x4 x5 x5 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x4 x4 x5 x4 x4) (x3 x5 x4 x4 x5 x4 x4) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x5 x5 x5 x4 x5))) (x1 (x2 (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x5 x4 x5 x5 x4) (x3 x4 x5 x5 x5 x4 x5) (x3 x5 x4 x4 x4 x4 x5) (x3 x5 x4 x4 x5 x5 x4) (x3 x5 x4 x5 x5 x5 x5)) (x2 (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x5 x5 x4 x4 x5) (x3 x5 x4 x5 x5 x5 x4) (x3 x4 x5 x4 x4 x5 x4) (x3 x4 x5 x5 x4 x4 x5) (x3 x4 x5 x5 x5 x5 x5)) (x2 (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x5 x5 x5 x5 x4) (x3 x5 x5 x4 x5 x4 x5) (x3 x4 x4 x5 x4 x5 x4) (x3 x4 x5 x5 x4 x5 x4) (x3 x5 x5 x5 x4 x5 x5)) (x2 (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x4 x5 x5 x4 x5) (x3 x5 x5 x5 x4 x5 x4) (x3 x4 x4 x4 x5 x4 x5) (x3 x5 x4 x4 x5 x4 x5) (x3 x5 x5 x4 x5 x5 x5)) (x2 (x3 x4 x5 x4 x5 x5 x5) (x3 x5 x4 x5 x4 x5 x4) (x3 x5 x4 x5 x4 x5 x5) (x3 x5 x5 x5 x5 x4 x4) (x3 x5 x5 x5 x5 x5 x4) (x3 x5 x4 x5 x4 x4 x5)) (x2 (x3 x5 x4 x5 x4 x5 x5) (x3 x4 x5 x4 x5 x4 x5) (x3 x4 x5 x4 x5 x5 x5) (x3 x5 x5 x5 x5 x4 x4) (x3 x5 x5 x5 x5 x4 x5) (x3 x4 x5 x4 x5 x4 x5))) (x1 (x2 (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x5 x5 x5 x5 x4) (x3 x5 x4 x5 x5 x4 x5) (x3 x5 x4 x4 x5 x5 x4) (x3 x5 x5 x4 x4 x5 x5) (x3 x5 x5 x4 x5 x4 x5)) (x2 (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x4 x5 x5 x4 x5) (x3 x4 x5 x5 x5 x5 x4) (x3 x4 x5 x5 x4 x4 x5) (x3 x5 x5 x4 x4 x5 x5) (x3 x5 x5 x5 x4 x4 x5)) (x2 (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x5 x4 x5 x5 x4) (x3 x5 x5 x5 x4 x4 x5) (x3 x4 x5 x5 x4 x4 x5) (x3 x4 x4 x5 x5 x5 x5) (x3 x4 x5 x5 x5 x4 x5)) (x2 (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x5 x5 x4 x4 x5) (x3 x5 x5 x4 x5 x5 x4) (x3 x5 x4 x4 x5 x5 x4) (x3 x4 x4 x5 x5 x5 x5) (x3 x5 x4 x5 x5 x4 x5)) (x2 (x3 x4 x5 x4 x5 x4 x4) (x3 x4 x5 x4 x5 x5 x5) (x3 x4 x5 x4 x5 x5 x4) (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x4 x5 x4 x5 x5) (x3 x5 x5 x5 x5 x5 x5)) (x2 (x3 x5 x4 x5 x4 x4 x4) (x3 x5 x4 x5 x4 x5 x5) (x3 x5 x4 x5 x4 x4 x5) (x3 x5 x5 x5 x5 x5 x5) (x3 x4 x5 x4 x5 x5 x5) (x3 x5 x5 x5 x5 x5 x5))) (x1 (x2 (x3 x5 x4 x4 x5 x4 x5) (x3 x5 x4 x4 x4 x5 x5) (x3 x5 x4 x4 x5 x5 x5) (x3 x5 x4 x5 x5 x4 x5) (x3 x5 x5 x4 x5 x5 x4) (x3 x4 x4 x5 x5 x4 x5)) (x2 (x3 x4 x5 x5 x4 x5 x4) (x3 x4 x5 x4 x4 x5 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x4 x5 x5 x5 x5 x4) (x3 x5 x5 x5 x4 x4 x5) (x3 x4 x4 x5 x5 x4 x5)) (x2 (x3 x4 x5 x5 x4 x5 x4) (x3 x4 x4 x5 x4 x5 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x5 x5 x4 x5 x4) (x3 x4 x5 x5 x5 x5 x4) (x3 x5 x5 x4 x4 x4 x5)) (x2 (x3 x5 x4 x4 x5 x4 x5) (x3 x4 x4 x4 x5 x5 x5) (x3 x5 x4 x4 x5 x5 x5) (x3 x5 x5 x4 x5 x4 x5) (x3 x5 x4 x5 x5 x4 x5) (x3 x5 x5 x4 x4 x4 x5)) (x2 (x3 x4 x5 x5 x4 x4 x4) (x3 x4 x5 x5 x4 x4 x4) (x3 x5 x4 x4 x5 x5 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x4 x4 x5 x5 x5)) (x2 (x3 x5 x4 x4 x5 x4 x4) (x3 x5 x4 x4 x5 x4 x4) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x4 x4 x5 x5 x5) (x3 x5 x5 x5 x5 x5 x5) (x3 x4 x5 x5 x4 x5 x5))) (x1 (x2 (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x4 x4 x5 x5 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x5 x4 x5 x5 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x4 x4 x5 x5 x5 x5)) (x2 (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x5 x4 x4 x4 x5) (x3 x5 x5 x5 x4 x5 x5) (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x4 x5 x5 x5 x5)) (x2 (x3 x4 x4 x5 x5 x4 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x4 x4 x5 x5 x5 x4) (x3 x4 x5 x5 x5 x5 x5) (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x5 x4 x4 x5 x5)) (x2 (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x4 x4 x5 x5 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x4 x5 x5 x5 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x5 x4 x4 x5 x5)) (x2 (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x4 x5 x4 x5 x4) (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x4 x5 x4 x5 x5) (x3 x5 x4 x5 x4 x5 x5) (x3 x4 x4 x4 x4 x4 x5)) (x2 (x3 x5 x5 x5 x5 x5 x5) (x3 x4 x5 x4 x5 x4 x5) (x3 x5 x5 x5 x5 x5 x5) (x3 x4 x5 x4 x5 x5 x5) (x3 x4 x5 x4 x5 x5 x5) (x3 x4 x4 x4 x4 x4 x5))) (x1 (x2 (x3 x4 x5 x4 x4 x5 x5) (x3 x5 x4 x5 x5 x5 x4) (x3 x5 x5 x4 x5 x5 x5) (x3 x4 x4 x5 x5 x5 x4) (x3 x4 x4 x5 x5 x4 x4) (x3 x5 x5 x5 x4 x5 x5)) (x2 (x3 x5 x4 x4 x4 x5 x5) (x3 x4 x5 x5 x5 x4 x5) (x3 x5 x5 x5 x4 x5 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x4 x4 x5 x5 x4 x4) (x3 x5 x5 x4 x5 x5 x5)) (x2 (x3 x4 x4 x4 x5 x5 x5) (x3 x5 x5 x5 x4 x5 x4) (x3 x4 x5 x5 x5 x5 x5) (x3 x5 x5 x4 x4 x4 x5) (x3 x5 x5 x4 x4 x4 x4) (x3 x5 x4 x5 x5 x5 x5)) (x2 (x3 x4 x4 x5 x4 x5 x5) (x3 x5 x5 x4 x5 x4 x5) (x3 x5 x4 x5 x5 x5 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x5 x4 x4 x4 x4) (x3 x4 x5 x5 x5 x5 x5)) (x2 (x3 x5 x5 x5 x5 x4 x4) (x3 x5 x5 x5 x5 x4 x4) (x3 x4 x4 x4 x4 x5 x5) (x3 x4 x4 x4 x4 x5 x5) (x3 x5 x5 x5 x5 x4 x4) (x3 x5 x5 x5 x5 x5 x5)) (x2 (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x5 x5 x5 x5 x5))))."?
Can you please invent a name for the term defined by " (fun x0 : (set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set) -> (set -> set -> set -> set -> set -> set -> set -> set -> set -> set -> set) -> prop => and (and (and (and (and (and (and (and (x0 missingname_9ed94aa81a158cf2838b6e3347c1d83280a2b37914d5c7e246ff38b5b0751101 missingname_0160cbd5f03b772c32962cff610c8ff61ac71013d4cb8a0f43c138227821e0d7) (and (x0 missingname_9ed94aa81a158cf2838b6e3347c1d83280a2b37914d5c7e246ff38b5b0751101 missingname_dd7c6467b10f0145b66f29abbf2003c9c65288ed1148798a2ca697bd78065b3d) (x0 missingname_0160cbd5f03b772c32962cff610c8ff61ac71013d4cb8a0f43c138227821e0d7 missingname_dd7c6467b10f0145b66f29abbf2003c9c65288ed1148798a2ca697bd78065b3d))) (and (and (x0 missingname_9ed94aa81a158cf2838b6e3347c1d83280a2b37914d5c7e246ff38b5b0751101 missingname_677bc60a8fdcf643e080cc574e7493ee36a94ad607a880f86aa31eca9c2a20b2) (x0 missingname_0160cbd5f03b772c32962cff610c8ff61ac71013d4cb8a0f43c138227821e0d7 missingname_677bc60a8fdcf643e080cc574e7493ee36a94ad607a880f86aa31eca9c2a20b2)) (x0 missingname_dd7c6467b10f0145b66f29abbf2003c9c65288ed1148798a2ca697bd78065b3d missingname_677bc60a8fdcf643e080cc574e7493ee36a94ad607a880f86aa31eca9c2a20b2))) (and (and (and (x0 missingname_9ed94aa81a158cf2838b6e3347c1d83280a2b37914d5c7e246ff38b5b0751101 missingname_08160c37a1ab38c2a8741bd21f5d85ae4e1ecc1f471131813ac76a14df5e34ca) (x0 missingname_0160cbd5f03b772c32962cff610c8ff61ac71013d4cb8a0f43c138227821e0d7 missingname_08160c37a1ab38c2a8741bd21f5d85ae4e1ecc1f471131813ac76a14df5e34ca)) (x0 missingname_dd7c6467b10f0145b66f29abbf2003c9c65288ed1148798a2ca697bd78065b3d missingname_08160c37a1ab38c2a8741bd21f5d85ae4e1ecc1f471131813ac76a14df5e34ca)) (x0 missingname_677bc60a8fdcf643e080cc574e7493ee36a94ad607a880f86aa31eca9c2a20b2 missingname_08160c37a1ab38c2a8741bd21f5d85ae4e1ecc1f471131813ac76a14df5e34ca))) (and (and (and (and (x0 missingname_9ed94aa81a158cf2838b6e3347c1d83280a2b37914d5c7e246ff38b5b0751101 missingname_e29e8aa444e52a9aff7677b4a659f06cce7015e180359810492b097b9052d91c) (x0 missingname_0160cbd5f03b772c32962cff610c8ff61ac71013d4cb8a0f43c138227821e0d7 missingname_e29e8aa444e52a9aff7677b4a659f06cce7015e180359810492b097b9052d91c)) (x0 missingname_dd7c6467b10f0145b66f29abbf2003c9c65288ed1148798a2ca697bd78065b3d missingname_e29e8aa444e52a9aff7677b4a659f06cce7015e180359810492b097b9052d91c)) (x0 missingname_677bc60a8fdcf643e080cc574e7493ee36a94ad607a880f86aa31eca9c2a20b2 missingname_e29e8aa444e52a9aff7677b4a659f06cce7015e180359810492b097b9052d91c)) (x0 missingname_08160c37a1ab38c2a8741bd21f5d85ae4e1ecc1f471131813ac76a14df5e34ca missingname_e29e8aa444e52a9aff7677b4a659f06cce7015e180359810492b097b9052d91c))) (and (and (and (and (and (x0 missingname_9ed94aa81a158cf2838b6e3347c1d83280a2b37914d5c7e246ff38b5b0751101 missingname_c5c365fe7c2d693786824197d1c188164cd70a1ba3bdae2dd2c5d26dbadee658) (x0 missingname_0160cbd5f03b772c32962cff610c8ff61ac71013d4cb8a0f43c138227821e0d7 missingname_c5c365fe7c2d693786824197d1c188164cd70a1ba3bdae2dd2c5d26dbadee658)) (x0 missingname_dd7c6467b10f0145b66f29abbf2003c9c65288ed1148798a2ca697bd78065b3d missingname_c5c365fe7c2d693786824197d1c188164cd70a1ba3bdae2dd2c5d26dbadee658)) (x0 missingname_677bc60a8fdcf643e080cc574e7493ee36a94ad607a880f86aa31eca9c2a20b2 missingname_c5c365fe7c2d693786824197d1c188164cd70a1ba3bdae2dd2c5d26dbadee658)) (x0 missingname_08160c37a1ab38c2a8741bd21f5d85ae4e1ecc1f471131813ac76a14df5e34ca missingname_c5c365fe7c2d693786824197d1c188164cd70a1ba3bdae2dd2c5d26dbadee658)) (x0 missingname_e29e8aa444e52a9aff7677b4a659f06cce7015e180359810492b097b9052d91c missingname_c5c365fe7c2d693786824197d1c188164cd70a1ba3bdae2dd2c5d26dbadee658))) (and (and (and (and (and (and (x0 missingname_9ed94aa81a158cf2838b6e3347c1d83280a2b37914d5c7e246ff38b5b0751101 missingname_f8849ca3b750d3ad38db8e876e60e1fed4c255e45fb4a9e6dda634e638c9b9ae) (x0 missingname_0160cbd5f03b772c32962cff610c8ff61ac71013d4cb8a0f43c138227821e0d7 missingname_f8849ca3b750d3ad38db8e876e60e1fed4c255e45fb4a9e6dda634e638c9b9ae)) (x0 missingname_dd7c6467b10f0145b66f29abbf2003c9c65288ed1148798a2ca697bd78065b3d missingname_f8849ca3b750d3ad38db8e876e60e1fed4c255e45fb4a9e6dda634e638c9b9ae)) (x0 missingname_677bc60a8fdcf643e080cc574e7493ee36a94ad607a880f86aa31eca9c2a20b2 missingname_f8849ca3b750d3ad38db8e876e60e1fed4c255e45fb4a9e6dda634e638c9b9ae)) (x0 missingname_08160c37a1ab38c2a8741bd21f5d85ae4e1ecc1f471131813ac76a14df5e34ca missingname_f8849ca3b750d3ad38db8e876e60e1fed4c255e45fb4a9e6dda634e638c9b9ae)) (x0 missingname_e29e8aa444e52a9aff7677b4a659f06cce7015e180359810492b097b9052d91c missingname_f8849ca3b750d3ad38db8e876e60e1fed4c255e45fb4a9e6dda634e638c9b9ae)) (x0 missingname_c5c365fe7c2d693786824197d1c188164cd70a1ba3bdae2dd2c5d26dbadee658 missingname_f8849ca3b750d3ad38db8e876e60e1fed4c255e45fb4a9e6dda634e638c9b9ae))) (and (and (and (and (and (and (and (x0 missingname_9ed94aa81a158cf2838b6e3347c1d83280a2b37914d5c7e246ff38b5b0751101 missingname_0563ecdd0f6df49f087d7271b4758716802ec79d849b006b520dcdac44c56ddb) (x0 missingname_0160cbd5f03b772c32962cff610c8ff61ac71013d4cb8a0f43c138227821e0d7 missingname_0563ecdd0f6df49f087d7271b4758716802ec79d849b006b520dcdac44c56ddb)) (x0 missingname_dd7c6467b10f0145b66f29abbf2003c9c65288ed1148798a2ca697bd78065b3d missingname_0563ecdd0f6df49f087d7271b4758716802ec79d849b006b520dcdac44c56ddb)) (x0 missingname_677bc60a8fdcf643e080cc574e7493ee36a94ad607a880f86aa31eca9c2a20b2 missingname_0563ecdd0f6df49f087d7271b4758716802ec79d849b006b520dcdac44c56ddb)) (x0 missingname_08160c37a1ab38c2a8741bd21f5d85ae4e1ecc1f471131813ac76a14df5e34ca missingname_0563ecdd0f6df49f087d7271b4758716802ec79d849b006b520dcdac44c56ddb)) (x0 missingname_e29e8aa444e52a9aff7677b4a659f06cce7015e180359810492b097b9052d91c missingname_0563ecdd0f6df49f087d7271b4758716802ec79d849b006b520dcdac44c56ddb)) (x0 missingname_c5c365fe7c2d693786824197d1c188164cd70a1ba3bdae2dd2c5d26dbadee658 missingname_0563ecdd0f6df49f087d7271b4758716802ec79d849b006b520dcdac44c56ddb)) (x0 missingname_f8849ca3b750d3ad38db8e876e60e1fed4c255e45fb4a9e6dda634e638c9b9ae missingname_0563ecdd0f6df49f087d7271b4758716802ec79d849b006b520dcdac44c56ddb))) (and (and (and (and (and (and (and (and (x0 missingname_9ed94aa81a158cf2838b6e3347c1d83280a2b37914d5c7e246ff38b5b0751101 missingname_af9da978aa7b87cdab764777559ede69d9aea6f76d01b4a0eebdc7c271c36d40) (x0 missingname_0160cbd5f03b772c32962cff610c8ff61ac71013d4cb8a0f43c138227821e0d7 missingname_af9da978aa7b87cdab764777559ede69d9aea6f76d01b4a0eebdc7c271c36d40)) (x0 missingname_dd7c6467b10f0145b66f29abbf2003c9c65288ed1148798a2ca697bd78065b3d missingname_af9da978aa7b87cdab764777559ede69d9aea6f76d01b4a0eebdc7c271c36d40)) (x0 missingname_677bc60a8fdcf643e080cc574e7493ee36a94ad607a880f86aa31eca9c2a20b2 missingname_af9da978aa7b87cdab764777559ede69d9aea6f76d01b4a0eebdc7c271c36d40)) (x0 missingname_08160c37a1ab38c2a8741bd21f5d85ae4e1ecc1f471131813ac76a14df5e34ca missingname_af9da978aa7b87cdab764777559ede69d9aea6f76d01b4a0eebdc7c271c36d40)) (x0 missingname_e29e8aa444e52a9aff7677b4a659f06cce7015e180359810492b097b9052d91c missingname_af9da978aa7b87cdab764777559ede69d9aea6f76d01b4a0eebdc7c271c36d40)) (x0 missingname_c5c365fe7c2d693786824197d1c188164cd70a1ba3bdae2dd2c5d26dbadee658 missingname_af9da978aa7b87cdab764777559ede69d9aea6f76d01b4a0eebdc7c271c36d40)) (x0 missingname_f8849ca3b750d3ad38db8e876e60e1fed4c255e45fb4a9e6dda634e638c9b9ae missingname_af9da978aa7b87cdab764777559ede69d9aea6f76d01b4a0eebdc7c271c36d40)) (x0 missingname_0563ecdd0f6df49f087d7271b4758716802ec79d849b006b520dcdac44c56ddb missingname_af9da978aa7b87cdab764777559ede69d9aea6f76d01b4a0eebdc7c271c36d40)))."?
Can you please invent a name for the term defined by " (fun x0 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x1 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x2 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x3 : ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> ((set -> set) -> set -> set) -> (set -> set) -> set -> set => fun x4 : set => x0 (x1 (x2 (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6)) (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5)) (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5))) (x2 (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6)) (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6)) (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5))) (x2 (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6)) (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6)) (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6))) (x2 (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5)) (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6)) (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5))) (x2 (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6)) (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6)) (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6))) (x2 (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5)) (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6)) (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6))) (x2 (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5)) (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5)) (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6))) (x2 (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5)) (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5)) (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5)))) (x1 (x2 (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5)) (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6)) (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5))) (x2 (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5)) (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6)) (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6))) (x2 (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6)) (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6)) (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6))) (x2 (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5)) (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5)) (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6))) (x2 (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6)) (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6)) (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6))) (x2 (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6)) (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5)) (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6))) (x2 (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6)) (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5)) (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5))) (x2 (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5)) (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5)) (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5)))) (x1 (x2 (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5)) (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5)) (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6))) (x2 (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6)) (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5)) (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6))) (x2 (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6)) (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6)) (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6))) (x2 (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6)) (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5)) (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5))) (x2 (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6)) (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6)) (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6))) (x2 (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6)) (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6)) (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5))) (x2 (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5)) (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6)) (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5))) (x2 (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5)) (x3 (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5)) (x3 (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => fun x6 : set => x6) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5) (fun x5 : set -> set => x5)))) (fun x5 : set => x4))."?