iProver---3.9.4.THM-CRf.s

%------------------------------------------------------------------------------
% File     : iProver---3.9.4
% Problem  : ITP305_1 : TPTP v9.3.1. Released v8.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM

% Computer : n016.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Fri Sep 25 01:49:24 PM UTC 2026

% Result   : Theorem 9.87s 2.28s
% Output   : CNFRefutation 9.87s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : ITP305_1 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.04  % Command  : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/0.35  % Computer : n016.cluster.edu
% 0.08/0.35  % Model    : x86_64 x86_64
% 0.08/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35  % Memory   : 8046.5625MB
% 0.08/0.35  % OS       : Linux 6.8.0-71-generic
% 0.08/0.35  % CPULimit : 300
% 0.08/0.35  % WCLimit  : 300
% 0.08/0.35  % DateTime : Wed Sep 23 18:27:11 UTC 2026
% 0.08/0.35  % CPUTime  : 
% 0.08/0.35  Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.39  Running first-order theorem proving
% 0.13/0.39  Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.40  
% 0.13/0.40  % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.40  
% 0.13/0.40  % Detected problem language: tptp
% 0.13/0.41  % Proving...
% 9.87/2.28  % SZS status Started for theBenchmark.p
% 9.87/2.28  % SZS status Theorem for theBenchmark.p
% 9.87/2.28  
% 9.87/2.28  %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 9.87/2.28  
% 9.87/2.28  % ------  iProver source info
% 9.87/2.28  
% 9.87/2.28  % git: date: 2026-07-19 20:42:38 +0200
% 9.87/2.28  % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 9.87/2.28  % git: non_committed_changes: false
% 9.87/2.28  
% 9.87/2.28  % ------ Parsing...
% 9.87/2.28  % ------ Clausification by vclausify_rel  & Parsing by iProver...
% 9.87/2.28  % ------ Proving...
% 9.87/2.28  % ------ Problem Properties 
% 9.87/2.28  
% 9.87/2.28  % 
% 9.87/2.28  % clauses                               925
% 9.87/2.28  % conjectures                           1
% 9.87/2.28  % EPR                                   113
% 9.87/2.28  % Horn                                  782
% 9.87/2.28  % unary                                 89
% 9.87/2.28  % binary                                428
% 9.87/2.28  % lits                                  2704
% 9.87/2.28  % lits eq                               543
% 9.87/2.28  % fd_pure                               0
% 9.87/2.28  % fd_pseudo                             0
% 9.87/2.28  % fd_cond                               0
% 9.87/2.28  % fd_pseudo_cond                        50
% 9.87/2.28  % AC symbols                            0
% 9.87/2.28  
% 9.87/2.28  % ------ Input Options Time Limit: Unbounded
% 9.87/2.28  
% 9.87/2.28  
% 9.87/2.28  % ------ 
% 9.87/2.28  % Current options:
% 9.87/2.28  % ------ 
% 9.87/2.28  
% 9.87/2.28  
% 9.87/2.28  % 
% 9.87/2.28  
% 9.87/2.28  % ------ Proving...
% 9.87/2.28  % 
% 9.87/2.28  
% 9.87/2.28  % SZS status Theorem for theBenchmark.p
% 9.87/2.28  
% 9.87/2.28  % SZS output start CNFRefutation for theBenchmark.p
% 9.87/2.28  
% 9.87/2.28  tff(func_def_0, type, 'uu$': 'A_set$' > 'A_bool_fun$').
% 9.87/2.28  tff(pred_def_1, type, 'functor$e': 'ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_2, type, 'functor_comp_def$h': ('A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$' * 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$') > $o).
% 9.87/2.28  tff(pred_def_3, type, 'functor$m': 'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_4, type, 'functorM$e': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_5, type, 'functorM$d': 'ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_6, type, 'fun_app$b': ('ZF_bool_fun$' * 'ZF$') > $o).
% 9.87/2.28  tff(pred_def_7, type, 'natTransP$b': 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > $o).
% 9.87/2.28  tff(pred_def_8, type, 'functor$g': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_9, type, 'preFunctor$e': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_10, type, 'member$f': ('B_a_fun$' * 'B_a_fun_set$') > $o).
% 9.87/2.28  tff(pred_def_11, type, 'fun_app$f': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$') > $o).
% 9.87/2.28  tff(pred_def_12, type, 'preFunctor$c': 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_13, type, 'preFunctor$h': 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_14, type, 'lSCategory$': 'A_b_b_c_LSCategory_ext_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_15, type, 'member$': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$') > $o).
% 9.87/2.28  tff(pred_def_16, type, 'category$d': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext_unit_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_17, type, 'member$j': ('A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' * 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$') > $o).
% 9.87/2.28  tff(pred_def_18, type, 'natTransExt$c': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' > $o).
% 9.87/2.28  tff(pred_def_19, type, 'functor$a': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_20, type, 'functor_abbrev$f': ('A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A_b_b_c_LSCategory_ext_Category_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$') > $o).
% 9.87/2.28  tff(pred_def_21, type, 'functor_comp_def$e': ('ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' * 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$') > $o).
% 9.87/2.28  tff(pred_def_22, type, 'category$a': 'ZF_ZF_unit_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_23, type, 'member$k': ('ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_set$') > $o).
% 9.87/2.28  tff(pred_def_24, type, 'functor_comp_def$c': ('A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$') > $o).
% 9.87/2.28  tff(pred_def_25, type, 'category$b': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_26, type, 'functor_abbrev$c': ('ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' * 'ZF_ZF_unit_Category_ext$' * 'ZF_ZF_unit_Category_ext$') > $o).
% 9.87/2.28  tff(pred_def_27, type, 'nt_abbrev$d': ('ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$') > $o).
% 9.87/2.28  tff(pred_def_28, type, 'functorM_axioms$': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_29, type, 'preFunctor$d': 'ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_30, type, 'functorM$b': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_31, type, 'functorExt$b': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_32, type, 'functorM$f': 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_33, type, 'fun_app$h': ('B_ZF_fun_bool_fun$' * 'B_ZF_fun$') > $o).
% 9.87/2.28  tff(pred_def_34, type, 'functorM$h': 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_35, type, 'functorM_axioms$c': 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_36, type, 'functorM$c': 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_37, type, 'member$d': ('ZF$' * 'ZF_set$') > $o).
% 9.87/2.28  tff(pred_def_38, type, 'nTCompDefined$a': ('ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$') > $o).
% 9.87/2.28  tff(pred_def_39, type, 'preFunctor$k': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_40, type, 'natTrans$a': 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > $o).
% 9.87/2.28  tff(pred_def_41, type, 'fun_app$l': ('A_bool_fun$' * 'A$') > $o).
% 9.87/2.28  tff(pred_def_42, type, 'functor_abbrev$a': ('ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' * 'ZF_ZF_unit_Category_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$') > $o).
% 9.87/2.28  tff(pred_def_43, type, 'functor$j': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_44, type, 'category$i': 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_45, type, 'nt_abbrev$c': ('ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' * 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' * 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$') > $o).
% 9.87/2.28  tff(pred_def_46, type, 'member$g': ('A_b_fun$' * 'A_b_fun_set$') > $o).
% 9.87/2.28  tff(pred_def_47, type, 'category$f': 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext_unit_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_48, type, 'fun_app$j': ('A_b_fun_bool_fun$' * 'A_b_fun$') > $o).
% 9.87/2.28  tff(pred_def_49, type, 'natTransExt$d': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > $o).
% 9.87/2.28  tff(pred_def_50, type, 'functor_abbrev$d': ('ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' * 'ZF_ZF_unit_Category_ext$' * 'A_b_b_c_LSCategory_ext_Category_ext$') > $o).
% 9.87/2.28  tff(pred_def_51, type, 'category_axioms$b': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_52, type, 'category$h': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_a_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_a_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext_unit_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_53, type, 'lSCategory_axioms$': 'A_b_b_c_LSCategory_ext_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_54, type, 'preFunctor$l': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_55, type, 'functorExt$': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_56, type, 'category$c': 'A_b_b_c_LSCategory_ext_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_57, type, 'functor$k': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_58, type, 'fun_app$g': ('B_b_prod_bool_fun$' * 'B_b_prod$') > $o).
% 9.87/2.28  tff(pred_def_59, type, 'extCategory$a': 'A_b_b_c_LSCategory_ext_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_60, type, 'functorM$l': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_61, type, 'functorM$g': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_62, type, 'functor_comp_def$a': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$') > $o).
% 9.87/2.28  tff(pred_def_63, type, 'member$l': ('ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_set$') > $o).
% 9.87/2.28  tff(pred_def_64, type, 'preFunctor$g': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_65, type, 'functor$h': 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_66, type, 'functorM_axioms$a': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_67, type, 'extCategory$': 'ZF_ZF_unit_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_68, type, 'natTransExt$a': 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > $o).
% 9.87/2.28  tff(pred_def_69, type, 'compDefined$c': ('ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$') > $o).
% 9.87/2.28  tff(pred_def_70, type, 'category_axioms$': 'A_b_b_c_LSCategory_ext_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_71, type, 'functor_comp_def$f': ('A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$') > $o).
% 9.87/2.28  tff(pred_def_72, type, 'functor_abbrev$': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A_b_b_c_LSCategory_ext_Category_ext$' * 'ZF_ZF_unit_Category_ext$') > $o).
% 9.87/2.28  tff(pred_def_73, type, 'functorM$i': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_a_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_74, type, 'member$m': ('B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$' * 'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_set$') > $o).
% 9.87/2.28  tff(pred_def_75, type, 'member$a': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$') > $o).
% 9.87/2.28  tff(pred_def_76, type, 'functor$f': 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_77, type, 'natTransP$d': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > $o).
% 9.87/2.28  tff(pred_def_78, type, 'natTrans$c': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' > $o).
% 9.87/2.28  tff(pred_def_79, type, 'mapsTo$c': ('ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$') > $o).
% 9.87/2.28  tff(pred_def_80, type, 'fun_app$e': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$') > $o).
% 9.87/2.28  tff(pred_def_81, type, 'functor_abbrev$e': ('A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$' * 'A_b_b_c_LSCategory_ext_Category_ext$' * 'A_b_b_c_LSCategory_ext_Category_ext$') > $o).
% 9.87/2.28  tff(pred_def_82, type, 'functor$b': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_83, type, 'functorM$a': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_84, type, 'fun_app$k': ('B_bool_fun$' * 'B$') > $o).
% 9.87/2.28  tff(pred_def_85, type, 'natTrans$b': 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > $o).
% 9.87/2.28  tff(pred_def_86, type, 'natTrans$d': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > $o).
% 9.87/2.28  tff(pred_def_87, type, 'member$n': ('ZF_ZF_fun$' * 'ZF_ZF_fun_set$') > $o).
% 9.87/2.28  tff(pred_def_88, type, 'functorExt$d': 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_89, type, 'member$h': ('B$' * 'B_set$') > $o).
% 9.87/2.28  tff(pred_def_90, type, 'functorM_axioms$b': 'ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_91, type, 'functor_comp_def$d': ('A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$') > $o).
% 9.87/2.28  tff(pred_def_92, type, 'member$i': ('A$' * 'A_set$') > $o).
% 9.87/2.28  tff(pred_def_93, type, 'functor$i': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_a_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_94, type, 'category$e': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext_a_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext_unit_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_95, type, 'natTransP$c': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' > $o).
% 9.87/2.28  tff(pred_def_96, type, 'category$g': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_97, type, 'nt_abbrev$a': ('A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' * 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$') > $o).
% 9.87/2.28  tff(pred_def_98, type, 'functor$l': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_99, type, 'member$o': ('ZF_ZF_prod_ZF_fun$' * 'ZF_ZF_prod_ZF_fun_set$') > $o).
% 9.87/2.28  tff(pred_def_100, type, 'equivalence_axioms$a': 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_101, type, 'category_axioms$a': 'ZF_ZF_unit_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_102, type, 'preFunctor$j': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_103, type, 'fun_app$a': ('ZF_ZF_prod_bool_fun$' * 'ZF_ZF_prod$') > $o).
% 9.87/2.28  tff(pred_def_104, type, 'preFunctor$a': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_105, type, 'natTransP$a': 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > $o).
% 9.87/2.28  tff(pred_def_106, type, 'member$c': ('B_b_prod$' * 'B_b_prod_set$') > $o).
% 9.87/2.28  tff(pred_def_107, type, 'preFunctor$f': 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_108, type, 'functor_abbrev$b': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' * 'A_b_b_c_LSCategory_ext_Category_ext$') > $o).
% 9.87/2.28  tff(pred_def_109, type, 'member$p': ('B_b_prod_b_fun$' * 'B_b_prod_b_fun_set$') > $o).
% 9.87/2.28  tff(pred_def_110, type, 'category$j': 'ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext_unit_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_111, type, 'member$b': ('ZF_ZF_prod$' * 'ZF_ZF_prod_set$') > $o).
% 9.87/2.28  tff(pred_def_112, type, 'preFunctor$i': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_a_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_113, type, 'functor_comp_def$': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$') > $o).
% 9.87/2.28  tff(pred_def_114, type, 'natTransExt$b': 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > $o).
% 9.87/2.28  tff(pred_def_115, type, 'functor$d': 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_116, type, 'category$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_117, type, 'functorExt$c': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_118, type, 'functorM$k': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_119, type, 'functor$c': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_120, type, 'fun_app$i': ('B_a_fun_bool_fun$' * 'B_a_fun$') > $o).
% 9.87/2.28  tff(pred_def_121, type, 'functorM$j': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_122, type, 'equivalence$a': 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_123, type, 'preFunctor$b': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_124, type, 'functor_comp_def$g': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$') > $o).
% 9.87/2.28  tff(pred_def_125, type, 'nt_abbrev$b': ('A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' * 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$' * 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$') > $o).
% 9.87/2.28  tff(pred_def_126, type, 'category$k': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_127, type, 'member$e': ('B_ZF_fun$' * 'B_ZF_fun_set$') > $o).
% 9.87/2.28  tff(pred_def_128, type, sP0: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_129, type, sP1: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_130, type, sP2: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_131, type, sP3: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_132, type, sP4: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > $o).
% 9.87/2.28  tff(pred_def_133, type, sP5: 'A_b_b_c_LSCategory_ext_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_134, type, sP6: 'A_b_b_c_LSCategory_ext_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_135, type, sP7: 'A_b_b_c_LSCategory_ext_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_136, type, sP8: 'A_b_b_c_LSCategory_ext_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_137, type, sP9: 'ZF_ZF_unit_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_138, type, sP10: 'ZF_ZF_unit_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_139, type, sP11: 'ZF_ZF_unit_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_140, type, sP12: 'ZF_ZF_unit_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_141, type, sP13: 'A_b_b_c_LSCategory_ext_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_142, type, sP14: 'A_b_b_c_LSCategory_ext_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_143, type, sP15: 'A_b_b_c_LSCategory_ext_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_144, type, sP16: 'A_b_b_c_LSCategory_ext_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_145, type, sP17: 'A_b_b_c_LSCategory_ext_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_146, type, sP18: 'ZF_ZF_unit_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_147, type, sP19: 'ZF_ZF_unit_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_148, type, sP20: 'ZF_ZF_unit_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_149, type, sP21: 'ZF_ZF_unit_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_150, type, sP22: 'ZF_ZF_unit_Category_ext$' > $o).
% 9.87/2.28  tff(pred_def_151, type, sP23: 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > $o).
% 9.87/2.28  tff(pred_def_152, type, sP24: 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' > $o).
% 9.87/2.28  tff(pred_def_153, type, sP25: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > $o).
% 9.87/2.28  tff(pred_def_154, type, sP26: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > $o).
% 9.87/2.28  tff(pred_def_155, type, sP27: 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > $o).
% 9.87/2.28  tff(func_def_156, type, 'yMap$': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'A$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$') > 'ZF$').
% 9.87/2.28  tff(func_def_157, type, 'homFtorContra$a': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'A$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_158, type, 'homFtorContra$': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'A$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_159, type, 'uuu$': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A$') > 'ZF_bool_fun$').
% 9.87/2.28  tff(func_def_160, type, 'catExp$i': ('ZF_ZF_unit_Category_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$') > 'ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext_unit_Category_ext$').
% 9.87/2.28  tff(func_def_161, type, 'mapM$d': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > 'ZF_ZF_fun$').
% 9.87/2.28  tff(func_def_162, type, 'mapM$e': ('ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' * 'ZF$') > 'B$').
% 9.87/2.28  tff(func_def_163, type, 'uve$': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_ZF_fun_fun$').
% 9.87/2.28  tff(func_def_164, type, 'cod$b': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_165, type, 'natTransComp$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$').
% 9.87/2.28  tff(func_def_166, type, 'obj$b': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'A_set$').
% 9.87/2.28  tff(func_def_167, type, 'zFfunComp$': 'ZF_ZF_ZF_fun_fun$').
% 9.87/2.28  tff(func_def_168, type, 'compDefined$a': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'B$') > 'B_bool_fun$').
% 9.87/2.28  tff(func_def_169, type, 'inverse_rel$a': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'B$') > 'B_bool_fun$').
% 9.87/2.28  tff(func_def_170, type, 'the$': 'ZF_bool_fun$' > 'ZF$').
% 9.87/2.28  tff(func_def_171, type, 'functorM_axioms$d': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$').
% 9.87/2.28  tff(func_def_172, type, 'natTransMap$': ('A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' * 'A$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$').
% 9.87/2.28  tff(func_def_173, type, 'constFunctor$b': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'ZF_ZF_unit_Category_ext$' * 'ZF$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_174, type, 'functorComp$': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$') > 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_175, type, 'mapM$': 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$').
% 9.87/2.28  tff(func_def_176, type, 'uuf$': 'A_b_fun_set$' > 'A_b_fun_bool_fun$').
% 9.87/2.28  tff(func_def_177, type, 'fun_app$v': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_178, type, 'restrict$d': ('A_b_fun$' * 'A_set$') > 'A_b_fun$').
% 9.87/2.28  tff(func_def_179, type, 'implode$': 'ZF_set$' > 'ZF$').
% 9.87/2.28  tff(func_def_180, type, 'uuz$': 'ZF_ZF_fun$').
% 9.87/2.28  tff(func_def_181, type, 'mapO$c': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$') > 'A$').
% 9.87/2.28  tff(func_def_182, type, 'identityFunctor$g': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_183, type, 'mapO$a': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A$') > 'ZF$').
% 9.87/2.28  tff(func_def_184, type, 'nTCod$': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_185, type, 'oppositeCategory$c': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$').
% 9.87/2.28  tff(func_def_186, type, 'constFunctor$l': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'ZF_ZF_unit_Category_ext$' * 'ZF$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_187, type, 'obj$c': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_set$').
% 9.87/2.28  tff(func_def_188, type, 'uuc$': 'B_set$' > 'B_bool_fun$').
% 9.87/2.28  tff(func_def_189, type, 'catCod$e': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$' > 'ZF_ZF_unit_Category_ext$').
% 9.87/2.28  tff(func_def_190, type, 'lSCategory_ext$': ('B_ZF_fun$' * 'C$') > 'B_c_LSCategory_ext$').
% 9.87/2.28  tff(func_def_191, type, 'catCod$b': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' > 'A_b_b_c_LSCategory_ext_Category_ext$').
% 9.87/2.28  tff(func_def_192, type, 'collect$b': 'A_bool_fun$' > 'A_set$').
% 9.87/2.28  tff(func_def_193, type, 'natTransMap$a': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'A_b_fun$').
% 9.87/2.28  tff(func_def_194, type, 'equivalence$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$').
% 9.87/2.28  tff(func_def_195, type, 'homSet$': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'A$' * 'A$') > 'ZF$').
% 9.87/2.28  tff(func_def_196, type, 'mapM$a': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'B_ZF_fun$').
% 9.87/2.28  tff(func_def_197, type, 'y$': 'A$').
% 9.87/2.28  tff(func_def_198, type, 'uux$': 'ZF_ZF_fun$').
% 9.87/2.28  tff(func_def_199, type, 'catDom$c': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > 'ZF_ZF_unit_Category_ext$').
% 9.87/2.28  tff(func_def_200, type, 'catExp$j': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' * 'ZF_ZF_unit_Category_ext$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$').
% 9.87/2.28  tff(func_def_201, type, 'fun_app$ae': ('ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$' * 'ZF_ZF_ZF_fun_fun$') > 'ZF_ZF_ZF_fun_fun$').
% 9.87/2.28  tff(func_def_202, type, 'catExp$g': ('ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' * 'A_b_b_c_LSCategory_ext_Category_ext$') > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_a_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_a_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext_unit_Category_ext$').
% 9.87/2.28  tff(func_def_203, type, 'functor$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$').
% 9.87/2.28  tff(func_def_204, type, 'extensional$a': 'B_set$' > 'B_ZF_fun_set$').
% 9.87/2.28  tff(func_def_205, type, 'eta$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$').
% 9.87/2.28  tff(func_def_206, type, 'homFtorMapContra$': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'B$' * 'A$') > 'ZF$').
% 9.87/2.28  tff(func_def_207, type, 'fun_app$n': ('B_b_fun$' * 'B$') > 'B$').
% 9.87/2.28  tff(func_def_208, type, 'extensional$c': 'A_set$' > 'A_b_fun_set$').
% 9.87/2.28  tff(func_def_209, type, 'uuw$': 'ZF$' > 'ZF_ZF_ZF_fun_fun$').
% 9.87/2.28  tff(func_def_210, type, 'dom_update$': ('ZF_ZF_fun_ZF_ZF_fun_fun$' * 'ZF_ZF_unit_Category_ext$') > 'ZF_ZF_unit_Category_ext$').
% 9.87/2.28  tff(func_def_211, type, 'functorComp$f': ('A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$') > 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_212, type, 'functorComp$e': ('ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' * 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$') > 'ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_213, type, 'category_ext$a': ('ZF_set$' * 'ZF_set$' * 'ZF_ZF_fun$' * 'ZF_ZF_fun$' * 'ZF_ZF_fun$' * 'ZF_ZF_ZF_fun_fun$' * 'Unit$') > 'ZF_ZF_unit_Category_ext$').
% 9.87/2.28  tff(func_def_214, type, 'id$b': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'A_b_fun$').
% 9.87/2.28  tff(func_def_215, type, 'homFtorMap$': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'A$') > 'B_ZF_fun$').
% 9.87/2.28  tff(func_def_216, type, 'collect$f': 'B_a_fun_bool_fun$' > 'B_a_fun_set$').
% 9.87/2.28  tff(func_def_217, type, 'uuq$': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'B$') > 'ZF_ZF_fun$').
% 9.87/2.28  tff(func_def_218, type, 'makeNT$a': 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$').
% 9.87/2.28  tff(func_def_219, type, 'inverse$': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_fun$').
% 9.87/2.28  tff(func_def_220, type, 'mapM$g': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$') > 'ZF$').
% 9.87/2.28  tff(func_def_221, type, 'restrict$': ('ZF_ZF_prod_ZF_fun$' * 'ZF_ZF_prod_set$' * 'ZF_ZF_prod$') > 'ZF$').
% 9.87/2.28  tff(func_def_222, type, 'identityFunctor$e': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_223, type, 'functorExt$a': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$').
% 9.87/2.28  tff(func_def_224, type, 'identityFunctor$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_225, type, 'more_update$': ('Unit_unit_fun$' * 'ZF_ZF_unit_Category_ext$') > 'ZF_ZF_unit_Category_ext$').
% 9.87/2.28  tff(func_def_226, type, 'zF2mor$': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'ZF$') > 'B$').
% 9.87/2.28  tff(func_def_227, type, 'uuo$': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'B$') > 'ZF_ZF_fun$').
% 9.87/2.28  tff(func_def_228, type, 'uvc$': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_b_b_fun_fun$').
% 9.87/2.28  tff(func_def_229, type, 'fun_app$ac': ('A_set_a_set_fun$' * 'A_set$') > 'A_set$').
% 9.87/2.28  tff(func_def_230, type, 'category_ext$b': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$' * 'Unit$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$').
% 9.87/2.28  tff(func_def_231, type, 'mapM$b': ('ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' * 'ZF$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$').
% 9.87/2.28  tff(func_def_232, type, 'catExp$c': ('ZF_ZF_unit_Category_ext$' * 'A_b_b_c_LSCategory_ext_Category_ext$') > 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext_unit_Category_ext$').
% 9.87/2.28  tff(func_def_233, type, 'mapO$': ('A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_234, type, 'dom$': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_a_fun$').
% 9.87/2.28  tff(func_def_235, type, 'zFfunDom$': 'ZF_ZF_fun$').
% 9.87/2.28  tff(func_def_236, type, 'fun_app$w': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$').
% 9.87/2.28  tff(func_def_237, type, 'mapO$d': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > 'ZF_ZF_fun$').
% 9.87/2.28  tff(func_def_238, type, 'mor$c': 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext_a_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' > 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$').
% 9.87/2.28  tff(func_def_239, type, 'zFfunApp$': 'ZF_ZF_ZF_fun_fun$').
% 9.87/2.28  tff(func_def_240, type, 'collect$c': 'ZF_bool_fun$' > 'ZF_set$').
% 9.87/2.28  tff(func_def_241, type, 'constFunctor$g': ('ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' * 'A_b_b_c_LSCategory_ext_Category_ext$' * 'A$') > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_a_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_242, type, 'fun_app$q': ('B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$' * 'B$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$').
% 9.87/2.28  tff(func_def_243, type, 'constFunctor$f': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$') > 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_244, type, 'cod$a': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_fun$').
% 9.87/2.28  tff(func_def_245, type, 'functorComp$i': ('A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_246, type, 'functor_comp_def$i': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$').
% 9.87/2.28  tff(func_def_247, type, 'catCod$a': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'ZF_ZF_unit_Category_ext$').
% 9.87/2.28  tff(func_def_248, type, 'hOMCollection$': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'A$' * 'A$') > 'ZF_set$').
% 9.87/2.28  tff(func_def_249, type, 'uup$': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'A$') > 'B_ZF_fun$').
% 9.87/2.28  tff(func_def_250, type, 'mapO$h': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_251, type, 'objIso$a': ('ZF_ZF_unit_Category_ext$' * 'ZF$') > 'ZF_bool_fun$').
% 9.87/2.28  tff(func_def_252, type, 'comp$': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_ZF_fun_fun$').
% 9.87/2.28  tff(func_def_253, type, 'nTDom$': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_254, type, 'isomorphism$': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_bool_fun$').
% 9.87/2.28  tff(func_def_255, type, 'makeNT$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$').
% 9.87/2.28  tff(func_def_256, type, 'idNatTrans$c': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$').
% 9.87/2.28  tff(func_def_257, type, 'makeFtor$b': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_258, type, 'mapM$c': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$') > 'B$').
% 9.87/2.28  tff(func_def_259, type, 'fun_app$z': ('Nat_ZF_fun$' * 'Nat$') > 'ZF$').
% 9.87/2.28  tff(func_def_260, type, 'catExp$l': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'ZF_ZF_unit_Category_ext$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$').
% 9.87/2.28  tff(func_def_261, type, 'makeFtor$d': 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_262, type, 'idNatTrans$f': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$').
% 9.87/2.28  tff(func_def_263, type, 'obj_update$a': ('A_set_a_set_fun$' * 'A_b_b_c_LSCategory_ext_Category_ext$') > 'A_b_b_c_LSCategory_ext_Category_ext$').
% 9.87/2.28  tff(func_def_264, type, 'natTrans_ext$': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A_ZF_fun$' * 'Unit$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$').
% 9.87/2.28  tff(func_def_265, type, 'functor_ext$': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' * 'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$' * 'Unit$') > 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_266, type, 'constFunctor$q': ('ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' * 'A_b_b_c_LSCategory_ext_Category_ext$' * 'A$') > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_a_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_267, type, 'elem$': 'ZF$' > 'ZF_bool_fun$').
% 9.87/2.28  tff(func_def_268, type, 'mapsTo$a': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$').
% 9.87/2.28  tff(func_def_269, type, 'functorM$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$').
% 9.87/2.28  tff(func_def_270, type, 'comp$a': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_b_b_fun_fun$').
% 9.87/2.28  tff(func_def_271, type, 'fun_app$m': ('ZF_ZF_ZF_fun_fun$' * 'ZF$') > 'ZF_ZF_fun$').
% 9.87/2.28  tff(func_def_272, type, 'nTCatCod$d': 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > 'ZF_ZF_unit_Category_ext$').
% 9.87/2.28  tff(func_def_273, type, 'makeNT$d': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$').
% 9.87/2.28  tff(func_def_274, type, 'idNatTrans$e': 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$').
% 9.87/2.28  tff(func_def_275, type, 'catExp$b': ('ZF_ZF_unit_Category_ext$' * 'ZF_ZF_unit_Category_ext$') > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$').
% 9.87/2.28  tff(func_def_276, type, 'fun_app$': ('ZF_ZF_fun$' * 'ZF$') > 'ZF$').
% 9.87/2.28  tff(func_def_277, type, 'makeNT$b': 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$').
% 9.87/2.28  tff(func_def_278, type, 'uuv$': ('A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$').
% 9.87/2.28  tff(func_def_279, type, 'comp$d': 'ZF_ZF_fun$' > 'ZF_ZF_fun_ZF_ZF_fun_fun$').
% 9.87/2.28  tff(func_def_280, type, 'makeCat$': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_unit_Category_ext$').
% 9.87/2.28  tff(func_def_281, type, 'catExp$': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'ZF_ZF_unit_Category_ext$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$').
% 9.87/2.28  tff(func_def_282, type, 'constFunctor$e': ('ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' * 'ZF_ZF_unit_Category_ext$' * 'ZF$') > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_283, type, 'yFtorNT$a': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$').
% 9.87/2.28  tff(func_def_284, type, 'makeFtor$c': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' > 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_285, type, 'fun_app$p': ('B_ZF_fun$' * 'B$') > 'ZF$').
% 9.87/2.28  tff(func_def_286, type, 'fun_app$aa': ('ZF_ZF_fun_ZF_ZF_fun_fun$' * 'ZF_ZF_fun$') > 'ZF_ZF_fun$').
% 9.87/2.28  tff(func_def_287, type, 'catDom$d': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' > 'ZF_ZF_unit_Category_ext$').
% 9.87/2.28  tff(func_def_288, type, 'mor$a': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$').
% 9.87/2.28  tff(func_def_289, type, 'catCod$f': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$' > 'A_b_b_c_LSCategory_ext_Category_ext$').
% 9.87/2.28  tff(func_def_290, type, 'catExp$a': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$') > 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext_a_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$').
% 9.87/2.28  tff(func_def_291, type, 'uvf$': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'A$' * 'A$') > 'ZF_bool_fun$').
% 9.87/2.28  tff(func_def_292, type, 'mapO$e': ('ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' * 'ZF$') > 'A$').
% 9.87/2.28  tff(func_def_293, type, 'mapM_update$': ('B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$' * 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$') > 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_294, type, 'id$a': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_fun$').
% 9.87/2.28  tff(func_def_295, type, 'makeNT$c': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$').
% 9.87/2.28  tff(func_def_296, type, 'catExp$d': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'A_b_b_c_LSCategory_ext_Category_ext$') > 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext_a_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext_unit_Category_ext$').
% 9.87/2.28  tff(func_def_297, type, 'uuj$': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_b_b_fun_fun$').
% 9.87/2.28  tff(func_def_298, type, 'yFtor$': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_299, type, 'homFtor$a': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'A$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_300, type, 'preFunctor$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$').
% 9.87/2.28  tff(func_def_301, type, 'uva$': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'ZF$') > 'B_bool_fun$').
% 9.87/2.28  tff(func_def_302, type, 'pair$': ('ZF$' * 'ZF$') > 'ZF_ZF_prod$').
% 9.87/2.28  tff(func_def_303, type, 'natTransExt$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$').
% 9.87/2.28  tff(func_def_304, type, 'uuh$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$').
% 9.87/2.28  tff(func_def_305, type, 'more$': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'C$').
% 9.87/2.28  tff(func_def_306, type, 'fun_app$t': ('B_a_fun$' * 'B$') > 'A$').
% 9.87/2.28  tff(func_def_307, type, 'collect$g': 'A_b_fun_bool_fun$' > 'A_b_fun_set$').
% 9.87/2.28  tff(func_def_308, type, 'yFtorNT$': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$').
% 9.87/2.28  tff(func_def_309, type, 'fun_app$c': ('A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$' * 'A$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$').
% 9.87/2.28  tff(func_def_310, type, 'mor_update$': ('ZF_set_ZF_set_fun$' * 'ZF_ZF_unit_Category_ext$') > 'ZF_ZF_unit_Category_ext$').
% 9.87/2.28  tff(func_def_311, type, 'catExp$e': ('ZF_ZF_unit_Category_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$') > 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext_unit_Category_ext$').
% 9.87/2.28  tff(func_def_312, type, 'natTransMap$b': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' * 'A$') > 'ZF$').
% 9.87/2.28  tff(func_def_313, type, 'mapO$b': ('ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' * 'ZF$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_314, type, 'nTCatDom$c': 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A_b_b_c_LSCategory_ext_Category_ext$').
% 9.87/2.28  tff(func_def_315, type, 'nTCatDom$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A_b_b_c_LSCategory_ext_Category_ext$').
% 9.87/2.28  tff(func_def_316, type, 'isZFfun$': 'ZF_bool_fun$').
% 9.87/2.28  tff(func_def_317, type, 'uvg$': 'ZF_ZF_prod_bool_fun$').
% 9.87/2.28  tff(func_def_318, type, 'catCod$': 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$').
% 9.87/2.28  tff(func_def_319, type, 'mor$b': 'ZF_ZF_unit_Category_ext$' > 'ZF_set$').
% 9.87/2.28  tff(func_def_320, type, 'uum$': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'ZF_ZF_unit_Category_ext$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$').
% 9.87/2.28  tff(func_def_321, type, 'nTCatCod$b': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'A_b_b_c_LSCategory_ext_Category_ext$').
% 9.87/2.28  tff(func_def_322, type, 'dom$a': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_fun$').
% 9.87/2.28  tff(func_def_323, type, 'yFtor$a': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_324, type, 'nt_abbrev$': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$').
% 9.87/2.28  tff(func_def_325, type, 'id$': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$').
% 9.87/2.28  tff(func_def_326, type, 'identityFunctor$d': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_327, type, 'mor$': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_set$').
% 9.87/2.28  tff(func_def_328, type, sK28: 'ZF_ZF_prod$' > 'ZF$').
% 9.87/2.28  tff(func_def_329, type, sK29: 'ZF_ZF_prod$' > 'ZF$').
% 9.87/2.28  tff(func_def_330, type, sK30: ('ZF_ZF_unit_Category_ext$' * 'ZF_ZF_prod$') > 'ZF$').
% 9.87/2.28  tff(func_def_331, type, sK31: ('ZF_ZF_unit_Category_ext$' * 'ZF_ZF_prod$') > 'ZF$').
% 9.87/2.28  tff(func_def_332, type, sK32: ('A_b_b_c_LSCategory_ext_Category_ext$' * 'B_b_prod$') > 'B$').
% 9.87/2.28  tff(func_def_333, type, sK33: ('A_b_b_c_LSCategory_ext_Category_ext$' * 'B_b_prod$') > 'B$').
% 9.87/2.28  tff(func_def_334, type, sK34: ('A_b_b_c_LSCategory_ext_Category_ext$' * 'A$' * 'A$' * 'ZF$') > 'B$').
% 9.87/2.28  tff(func_def_335, type, sK35: ('B_ZF_fun$' * 'B_ZF_fun_b_ZF_fun_fun$' * 'B_ZF_fun_b_ZF_fun_fun$') > 'B_ZF_fun$').
% 9.87/2.28  tff(func_def_336, type, sK36: ('B_ZF_fun$' * 'B_ZF_fun_b_ZF_fun_fun$' * 'B_ZF_fun_b_ZF_fun_fun$') > 'B_ZF_fun$').
% 9.87/2.28  tff(func_def_337, type, sK37: ('A_bool_fun$' * 'A_bool_fun$') > 'A$').
% 9.87/2.28  tff(func_def_338, type, sK38: ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_339, type, sK39: ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$').
% 9.87/2.28  tff(func_def_340, type, sK40: ('B_b_prod_bool_fun$' * 'B_b_prod_bool_fun$') > 'B_b_prod$').
% 9.87/2.28  tff(func_def_341, type, sK41: ('ZF_bool_fun$' * 'ZF_bool_fun$') > 'ZF$').
% 9.87/2.28  tff(func_def_342, type, sK42: ('ZF_ZF_prod_bool_fun$' * 'ZF_ZF_prod_bool_fun$') > 'ZF_ZF_prod$').
% 9.87/2.28  tff(func_def_343, type, sK43: ('A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_344, type, sK44: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'B$').
% 9.87/2.28  tff(func_def_345, type, sK45: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A$').
% 9.87/2.28  tff(func_def_346, type, sK46: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A$').
% 9.87/2.28  tff(func_def_347, type, sK47: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'B$').
% 9.87/2.28  tff(func_def_348, type, sK48: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A$').
% 9.87/2.28  tff(func_def_349, type, sK49: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A$').
% 9.87/2.28  tff(func_def_350, type, sK50: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'B$').
% 9.87/2.28  tff(func_def_351, type, sK51: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A$').
% 9.87/2.28  tff(func_def_352, type, sK52: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A$').
% 9.87/2.28  tff(func_def_353, type, sK53: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'B$').
% 9.87/2.28  tff(func_def_354, type, sK54: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A$').
% 9.87/2.28  tff(func_def_355, type, sK55: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A$').
% 9.87/2.28  tff(func_def_356, type, sK56: ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A$' * 'A$' * 'ZF$') > 'B$').
% 9.87/2.28  tff(func_def_357, type, sK57: ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'ZF$') > 'A$').
% 9.87/2.28  tff(func_def_358, type, sK58: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'B$').
% 9.87/2.28  tff(func_def_359, type, sK59: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'B$').
% 9.87/2.28  tff(func_def_360, type, sK60: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A$').
% 9.87/2.28  tff(func_def_361, type, sK61: 'ZF_ZF_unit_Category_ext$' > 'ZF_set$').
% 9.87/2.28  tff(func_def_362, type, sK62: 'ZF_ZF_unit_Category_ext$' > 'ZF_set$').
% 9.87/2.28  tff(func_def_363, type, sK63: 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_fun$').
% 9.87/2.28  tff(func_def_364, type, sK64: 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_fun$').
% 9.87/2.28  tff(func_def_365, type, sK65: 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_fun$').
% 9.87/2.28  tff(func_def_366, type, sK66: 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_ZF_fun_fun$').
% 9.87/2.28  tff(func_def_367, type, sK67: 'ZF_ZF_unit_Category_ext$' > 'Unit$').
% 9.87/2.28  tff(func_def_368, type, sK68: ('A_b_b_c_LSCategory_ext_Category_ext$' * 'B$') > 'B$').
% 9.87/2.28  tff(func_def_369, type, sK69: ('ZF_ZF_unit_Category_ext$' * 'ZF$') > 'ZF$').
% 9.87/2.28  tff(func_def_370, type, sK70: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'B$').
% 9.87/2.28  tff(func_def_371, type, sK71: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'B$').
% 9.87/2.28  tff(func_def_372, type, sK72: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A$').
% 9.87/2.28  tff(func_def_373, type, sK73: ('A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_374, type, sK74: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'B$').
% 9.87/2.28  tff(func_def_375, type, sK75: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A$').
% 9.87/2.28  tff(func_def_376, type, sK76: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A$').
% 9.87/2.28  tff(func_def_377, type, sK77: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'B$').
% 9.87/2.28  tff(func_def_378, type, sK78: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A$').
% 9.87/2.28  tff(func_def_379, type, sK79: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A$').
% 9.87/2.28  tff(func_def_380, type, sK80: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_381, type, sK81: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_382, type, sK82: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'B$').
% 9.87/2.28  tff(func_def_383, type, sK83: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A$').
% 9.87/2.28  tff(func_def_384, type, sK84: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A$').
% 9.87/2.28  tff(func_def_385, type, sK85: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'B$').
% 9.87/2.28  tff(func_def_386, type, sK86: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A$').
% 9.87/2.28  tff(func_def_387, type, sK87: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A$').
% 9.87/2.28  tff(func_def_388, type, sK88: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$').
% 9.87/2.28  tff(func_def_389, type, sK89: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.87/2.28  tff(func_def_390, type, sK90: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A$').
% 9.87/2.28  tff(func_def_391, type, sK91: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A$').
% 9.87/2.28  tff(func_def_392, type, sK92: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_393, type, sK93: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_394, type, sK94: ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A$' * 'A$' * 'ZF$') > 'B$').
% 9.87/2.28  tff(func_def_395, type, sK95: ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'ZF$') > 'A$').
% 9.87/2.28  tff(func_def_396, type, sK96: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'B$').
% 9.87/2.28  tff(func_def_397, type, sK97: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A$').
% 9.87/2.28  tff(func_def_398, type, sK98: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A$').
% 9.87/2.28  tff(func_def_399, type, sK99: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'B$').
% 9.87/2.28  tff(func_def_400, type, sK100: ('A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A$' * 'A$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$') > 'B$').
% 9.87/2.28  tff(func_def_401, type, sK101: ('A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$') > 'A$').
% 9.87/2.28  tff(func_def_402, type, sK102: 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B$').
% 9.87/2.28  tff(func_def_403, type, sK103: 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B$').
% 9.87/2.28  tff(func_def_404, type, sK104: 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B$').
% 9.87/2.28  tff(func_def_405, type, sK105: 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B$').
% 9.87/2.28  tff(func_def_406, type, sK106: 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B$').
% 9.87/2.28  tff(func_def_407, type, sK107: 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B$').
% 9.87/2.28  tff(func_def_408, type, sK108: 'A_b_b_c_LSCategory_ext_Category_ext$' > 'A$').
% 9.87/2.28  tff(func_def_409, type, sK109: 'A_b_b_c_LSCategory_ext_Category_ext$' > 'A$').
% 9.87/2.28  tff(func_def_410, type, sK110: 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B$').
% 9.87/2.28  tff(func_def_411, type, sK111: 'A_b_b_c_LSCategory_ext_Category_ext$' > 'A$').
% 9.87/2.28  tff(func_def_412, type, sK112: 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B$').
% 9.87/2.28  tff(func_def_413, type, sK113: 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B$').
% 9.87/2.28  tff(func_def_414, type, sK114: 'A_b_b_c_LSCategory_ext_Category_ext$' > 'A$').
% 9.87/2.28  tff(func_def_415, type, sK115: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_416, type, sK116: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_417, type, sK117: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_418, type, sK118: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_419, type, sK119: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_420, type, sK120: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_421, type, sK121: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_422, type, sK122: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_423, type, sK123: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_424, type, sK124: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_425, type, sK125: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_426, type, sK126: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_427, type, sK127: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_428, type, sK128: 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B$').
% 9.87/2.28  tff(func_def_429, type, sK129: 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B$').
% 9.87/2.28  tff(func_def_430, type, sK130: 'A_b_b_c_LSCategory_ext_Category_ext$' > 'A$').
% 9.87/2.28  tff(func_def_431, type, sK131: 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B$').
% 9.87/2.28  tff(func_def_432, type, sK132: 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B$').
% 9.87/2.28  tff(func_def_433, type, sK133: 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B$').
% 9.87/2.28  tff(func_def_434, type, sK134: 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B$').
% 9.87/2.28  tff(func_def_435, type, sK135: 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B$').
% 9.87/2.28  tff(func_def_436, type, sK136: 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B$').
% 9.87/2.28  tff(func_def_437, type, sK137: 'A_b_b_c_LSCategory_ext_Category_ext$' > 'A$').
% 9.87/2.28  tff(func_def_438, type, sK138: 'A_b_b_c_LSCategory_ext_Category_ext$' > 'A$').
% 9.87/2.28  tff(func_def_439, type, sK139: 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B$').
% 9.87/2.28  tff(func_def_440, type, sK140: 'A_b_b_c_LSCategory_ext_Category_ext$' > 'A$').
% 9.87/2.28  tff(func_def_441, type, sK141: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_442, type, sK142: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_443, type, sK143: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_444, type, sK144: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_445, type, sK145: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_446, type, sK146: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_447, type, sK147: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_448, type, sK148: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_449, type, sK149: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_450, type, sK150: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_451, type, sK151: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_452, type, sK152: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_453, type, sK153: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_454, type, sK154: ('A_b_b_c_LSCategory_ext_Category_ext$' * 'A$' * 'A$') > 'B$').
% 9.87/2.28  tff(func_def_455, type, sK155: ('ZF_ZF_unit_Category_ext$' * 'ZF$' * 'ZF$') > 'ZF$').
% 9.87/2.28  tff(func_def_456, type, sK156: 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'A$').
% 9.87/2.28  tff(func_def_457, type, sK157: 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'B$').
% 9.87/2.28  tff(func_def_458, type, sK158: 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'A$').
% 9.87/2.28  tff(func_def_459, type, sK159: 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'A$').
% 9.87/2.28  tff(func_def_460, type, sK160: 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_461, type, sK161: 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_462, type, sK162: 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_463, type, sK163: 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_464, type, sK164: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A$').
% 9.87/2.28  tff(func_def_465, type, sK165: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'B$').
% 9.87/2.28  tff(func_def_466, type, sK166: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A$').
% 9.87/2.28  tff(func_def_467, type, sK167: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A$').
% 9.87/2.28  tff(func_def_468, type, sK168: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A$').
% 9.87/2.28  tff(func_def_469, type, sK169: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'B$').
% 9.87/2.28  tff(func_def_470, type, sK170: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A$').
% 9.87/2.28  tff(func_def_471, type, sK171: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A$').
% 9.87/2.28  tff(func_def_472, type, sK172: 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_473, type, sK173: 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_474, type, sK174: 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_475, type, sK175: 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_476, type, sK176: 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'A$').
% 9.87/2.28  tff(func_def_477, type, sK177: 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'B$').
% 9.87/2.28  tff(func_def_478, type, sK178: 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'A$').
% 9.87/2.28  tff(func_def_479, type, sK179: 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'A$').
% 9.87/2.28  tff(func_def_480, type, sK180: 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_481, type, sK181: 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_482, type, sK182: 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_483, type, sK183: 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_484, type, sK184: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A$').
% 9.87/2.28  tff(func_def_485, type, sK185: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'B$').
% 9.87/2.28  tff(func_def_486, type, sK186: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A$').
% 9.87/2.28  tff(func_def_487, type, sK187: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A$').
% 9.87/2.28  tff(func_def_488, type, sK188: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A$').
% 9.87/2.28  tff(func_def_489, type, sK189: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'B$').
% 9.87/2.28  tff(func_def_490, type, sK190: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A$').
% 9.87/2.28  tff(func_def_491, type, sK191: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A$').
% 9.87/2.28  tff(func_def_492, type, sK192: 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_493, type, sK193: 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_494, type, sK194: 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_495, type, sK195: 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > 'ZF$').
% 9.87/2.28  tff(func_def_496, type, sK196: 'ZF_ZF_unit_Category_ext$' > 'ZF_set$').
% 9.87/2.28  tff(func_def_497, type, sK197: 'ZF_ZF_unit_Category_ext$' > 'ZF_set$').
% 9.87/2.28  tff(func_def_498, type, sK198: 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_fun$').
% 9.87/2.28  tff(func_def_499, type, sK199: 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_fun$').
% 9.87/2.28  tff(func_def_500, type, sK200: 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_fun$').
% 9.87/2.28  tff(func_def_501, type, sK201: 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_ZF_fun_fun$').
% 9.87/2.28  tff(func_def_502, type, sK202: ('ZF$' * 'ZF_ZF_fun$' * 'ZF_ZF_fun$') > 'ZF$').
% 9.87/2.28  tff(func_def_503, type, sK203: ('ZF$' * 'ZF$') > 'ZF$').
% 9.87/2.28  tff(func_def_504, type, sK204: ('ZF$' * 'ZF_ZF_fun$' * 'ZF$') > 'ZF$').
% 9.87/2.28  tff(func_def_505, type, sK205: ('ZF$' * 'ZF$') > 'ZF$').
% 9.87/2.28  tff(func_def_506, type, sK206: ('ZF_bool_fun$' * 'ZF$') > 'ZF$').
% 9.87/2.28  tff(func_def_507, type, sK207: 'ZF_bool_fun$' > 'ZF$').
% 9.87/2.28  tff(func_def_508, type, sK208: ('ZF$' * 'ZF_bool_fun$') > 'ZF$').
% 9.87/2.28  tff(func_def_509, type, sK209: ('ZF$' * 'Nat_ZF_fun$') > 'Nat$').
% 9.87/2.28  tff(func_def_510, type, sK210: ('ZF$' * 'ZF_ZF_fun$' * 'ZF$') > 'ZF$').
% 9.87/2.28  tff(func_def_511, type, sK211: ('A_set$' * 'A_set_a_set_fun$' * 'A_set_a_set_fun$') > 'A_set$').
% 9.87/2.28  tff(func_def_512, type, sK212: ('ZF_set$' * 'ZF_set_ZF_set_fun$' * 'ZF_set_ZF_set_fun$') > 'ZF_set$').
% 9.87/2.28  tff(func_def_513, type, sK213: ('A_set$' * 'A_set_a_set_fun$' * 'A_set_a_set_fun$') > 'A_set$').
% 9.87/2.28  tff(func_def_514, type, sK214: ('ZF_set$' * 'ZF_set_ZF_set_fun$' * 'ZF_set_ZF_set_fun$') > 'ZF_set$').
% 9.87/2.28  tff(func_def_515, type, sK215: ('ZF_set$' * 'ZF_set_ZF_set_fun$' * 'ZF_set_ZF_set_fun$') > 'ZF_set$').
% 9.87/2.28  tff(func_def_516, type, sK216: ('ZF_set$' * 'ZF_set_ZF_set_fun$' * 'ZF_set_ZF_set_fun$') > 'ZF_set$').
% 9.87/2.28  tff(func_def_517, type, sK217: ('B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$' * 'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$' * 'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$') > 'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$').
% 9.87/2.28  tff(func_def_518, type, sK218: ('B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$' * 'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$' * 'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$') > 'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$').
% 9.87/2.28  tff(func_def_519, type, sK219: ('ZF_ZF_fun$' * 'ZF_ZF_fun_ZF_ZF_fun_fun$' * 'ZF_ZF_fun_ZF_ZF_fun_fun$') > 'ZF_ZF_fun$').
% 9.87/2.28  tff(func_def_520, type, sK220: ('ZF_ZF_fun$' * 'ZF_ZF_fun_ZF_ZF_fun_fun$' * 'ZF_ZF_fun_ZF_ZF_fun_fun$') > 'ZF_ZF_fun$').
% 9.87/2.28  tff(func_def_521, type, sK221: ('ZF_ZF_ZF_fun_fun$' * 'ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$' * 'ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$') > 'ZF_ZF_ZF_fun_fun$').
% 9.87/2.28  tff(func_def_522, type, sK222: ('ZF_ZF_ZF_fun_fun$' * 'ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$' * 'ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$') > 'ZF_ZF_ZF_fun_fun$').
% 9.87/2.28  tff(func_def_523, type, sK223: ('ZF_ZF_fun$' * 'ZF_ZF_fun_ZF_ZF_fun_fun$' * 'ZF_ZF_fun_ZF_ZF_fun_fun$') > 'ZF_ZF_fun$').
% 9.87/2.28  tff(func_def_524, type, sK224: ('ZF_ZF_fun$' * 'ZF_ZF_fun_ZF_ZF_fun_fun$' * 'ZF_ZF_fun_ZF_ZF_fun_fun$') > 'ZF_ZF_fun$').
% 9.87/2.28  tff(func_def_525, type, sK225: ('ZF_ZF_fun$' * 'ZF_ZF_fun_ZF_ZF_fun_fun$' * 'ZF_ZF_fun_ZF_ZF_fun_fun$') > 'ZF_ZF_fun$').
% 9.87/2.28  tff(func_def_526, type, sK226: ('ZF_ZF_fun$' * 'ZF_ZF_fun_ZF_ZF_fun_fun$' * 'ZF_ZF_fun_ZF_ZF_fun_fun$') > 'ZF_ZF_fun$').
% 9.87/2.28  tff(f35,conjecture,(
% 9.87/2.28    'yMapInv$'('c$','x$','mapO$'('yFtor$'('c$'),'y$'),'fun_app$p'('mor2ZF$'('c$'),'zF2mor$'('c$','yMap$'('c$','x$','eta$')))) = 'yMapInv$'('c$','x$','mapO$'('yFtor$'('c$'),'y$'),'yMap$'('c$','x$','eta$'))),
% 9.87/2.28    file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture34)).
% 9.87/2.28  
% 9.87/2.28  tff(f36,negated_conjecture,(
% 9.87/2.28    ~ 'yMapInv$'('c$','x$','mapO$'('yFtor$'('c$'),'y$'),'fun_app$p'('mor2ZF$'('c$'),'zF2mor$'('c$','yMap$'('c$','x$','eta$')))) = 'yMapInv$'('c$','x$','mapO$'('yFtor$'('c$'),'y$'),'yMap$'('c$','x$','eta$'))),
% 9.87/2.28    inference(negated_conjecture,[status(cth)],[f35])).
% 9.87/2.28  
% 9.87/2.28  tff(f37,axiom,(
% 9.87/2.28    'lSCategory$'('c$')),
% 9.87/2.28    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom35)).
% 9.87/2.28  
% 9.87/2.28  tff(f38,axiom,(
% 9.87/2.28    'member$i'('x$','obj$b'('c$'))),
% 9.87/2.28    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom36)).
% 9.87/2.28  
% 9.87/2.28  tff(f39,axiom,(
% 9.87/2.28    'member$i'('y$','obj$b'('c$'))),
% 9.87/2.28    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom37)).
% 9.87/2.28  
% 9.87/2.28  tff(f41,axiom,(
% 9.87/2.28    'fun_app$b'('elem$'('yMap$'('c$','x$','eta$')),'homSet$'('c$','x$','y$'))),
% 9.87/2.28    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom39)).
% 9.87/2.28  
% 9.87/2.28  tff(f42,axiom,(
% 9.87/2.28    'fun_app$q'('mapM$'('yFtor$'('c$')),'zF2mor$'('c$','yMap$'('c$','x$','eta$'))) = 'yMapInv$'('c$','x$','mapO$'('yFtor$'('c$'),'y$'),'fun_app$p'('mor2ZF$'('c$'),'zF2mor$'('c$','yMap$'('c$','x$','eta$'))))),
% 9.87/2.28    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom40)).
% 9.87/2.28  
% 9.87/2.28  tff(f49,axiom,(
% 9.87/2.28    ! [X0 : 'A_b_b_c_LSCategory_ext_Category_ext$',X1 : 'A$',X2 : 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$',X3 : 'ZF$'] : 'yMapInv$'(X0,X1,X2,X3) = 'makeNT$'('yMapInv$a'(X0,X1,X2,X3))),
% 9.87/2.28    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom47)).
% 9.87/2.28  
% 9.87/2.28  tff(f73,axiom,(
% 9.87/2.28    ! [X0 : 'A_b_b_c_LSCategory_ext_Category_ext$',X1 : 'A$',X2 : 'A$',X3 : 'ZF$'] : (('lSCategory$'(X0) & 'member$i'(X1,'obj$b'(X0)) & 'member$i'(X2,'obj$b'(X0)) & 'fun_app$b'('elem$'(X3),'homSet$'(X0,X1,X2))) => ('fun_app$l'('mapsTo$'(X0,'zF2mor$'(X0,X3),X1),X2) & 'fun_app$p'('mor2ZF$'(X0),'zF2mor$'(X0,X3)) = X3))),
% 9.87/2.28    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom71)).
% 9.87/2.28  
% 9.87/2.28  tff(f341,axiom,(
% 9.87/2.28    ! [X0 : 'A_b_b_c_LSCategory_ext_Category_ext$'] : 'yFtor$'(X0) = 'makeFtor$d'('yFtor$a'(X0))),
% 9.87/2.28    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom339)).
% 9.87/2.28  
% 9.87/2.28  tff(f468,axiom,(
% 9.87/2.28    ! [X0 : 'A_b_b_c_LSCategory_ext_Category_ext$',X1 : 'A$',X2 : 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'] : 'yMap$'(X0,X1,X2) = 'fun_app$'('fun_app$m'('zFfunApp$','natTransMap$b'(X2,X1)),'fun_app$p'('mor2ZF$'(X0),'fun_app$r'('id$b'(X0),X1)))),
% 9.87/2.28    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom466)).
% 9.87/2.28  
% 9.87/2.28  tff(f489,axiom,(
% 9.87/2.28    ! [X0 : 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$'] : 'makeFtor$d'(X0) = 'functor_ext$'('catDom$'(X0),'catCod$'(X0),'restrict$b'('mapM$'(X0),'mor$'('catDom$'(X0))),'more$c'(X0))),
% 9.87/2.28    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom487)).
% 9.87/2.28  
% 9.87/2.28  tff(f546,axiom,(
% 9.87/2.28    ! [X0 : 'A_b_b_c_LSCategory_ext_Category_ext$'] : 'oppositeCategory$'(X0) = 'category_ext$'('obj$b'(X0),'mor$'(X0),'cod$'(X0),'dom$'(X0),'id$b'(X0),'uuj$'(X0),'more$a'(X0))),
% 9.87/2.28    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom544)).
% 9.87/2.28  
% 9.87/2.28  tff(f558,axiom,(
% 9.87/2.28    ! [X0 : 'A_b_b_c_LSCategory_ext_Category_ext$'] : 'yFtor$a'(X0) = 'functor_ext$'(X0,'catExp$'('oppositeCategory$'(X0),'set$'),'yFtorNT$'(X0),'unity$')),
% 9.87/2.28    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom556)).
% 9.87/2.28  
% 9.87/2.28  tff(f560,axiom,(
% 9.87/2.28    ! [X0 : 'A_b_b_c_LSCategory_ext_Category_ext$',X1 : 'A$',X2 : 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$',X3 : 'ZF$'] : 'yMapInv$a'(X0,X1,X2,X3) = 'natTrans_ext$'('mapO$'('yFtor$'(X0),X1),X2,'uur$'(X0,X1,X2,X3),'unity$')),
% 9.87/2.28    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom558)).
% 9.87/2.28  
% 9.87/2.28  tff(f564,axiom,(
% 9.87/2.28    ! [X0 : 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$',X1 : 'A$'] : 'mapO$'(X0,X1) = 'the$a'('uuv$'(X0,X1))),
% 9.87/2.28    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom562)).
% 9.87/2.28  
% 9.87/2.28  tff(f581,axiom,(
% 9.87/2.28    ! [X0 : 'A_b_b_c_LSCategory_ext_Category_ext$',X1 : 'ZF$'] : 'zF2mor$'(X0,X1) = 'the$b'('uva$'(X0,X1))),
% 9.87/2.28    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom579)).
% 9.87/2.28  
% 9.87/2.28  tff(f591,axiom,(
% 9.87/2.28    ! [X0 : 'A_b_b_c_LSCategory_ext_Category_ext$',X1 : 'A$',X2 : 'A$'] : 'hOMCollection$'(X0,X1,X2) = 'collect$c'('uvf$'(X0,X1,X2))),
% 9.87/2.28    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom589)).
% 9.87/2.28  
% 9.87/2.28  tff(f593,axiom,(
% 9.87/2.28    ! [X0 : 'A_b_b_c_LSCategory_ext_Category_ext$',X1 : 'A$',X2 : 'A$'] : 'homSet$'(X0,X1,X2) = 'implode$'('hOMCollection$'(X0,X1,X2))),
% 9.87/2.28    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom591)).
% 9.87/2.28  
% 9.87/2.28  tff(f627,plain,(
% 9.87/2.28    'yMapInv$'('c$','x$','mapO$'('yFtor$'('c$'),'y$'),'fun_app$p'('mor2ZF$'('c$'),'zF2mor$'('c$','yMap$'('c$','x$','eta$')))) != 'yMapInv$'('c$','x$','mapO$'('yFtor$'('c$'),'y$'),'yMap$'('c$','x$','eta$'))),
% 9.87/2.28    inference(flattening,[],[f36])).
% 9.87/2.28  
% 9.87/2.28  tff(f758,plain,(
% 9.87/2.28    ! [X0 : 'A_b_b_c_LSCategory_ext_Category_ext$',X1 : 'A$',X2 : 'A$',X3 : 'ZF$'] : (('fun_app$l'('mapsTo$'(X0,'zF2mor$'(X0,X3),X1),X2) & 'fun_app$p'('mor2ZF$'(X0),'zF2mor$'(X0,X3)) = X3) | (~'lSCategory$'(X0) | ~'member$i'(X1,'obj$b'(X0)) | ~'member$i'(X2,'obj$b'(X0)) | ~'fun_app$b'('elem$'(X3),'homSet$'(X0,X1,X2))))),
% 9.87/2.28    inference(ennf_transformation,[],[f73])).
% 9.87/2.28  
% 9.87/2.28  tff(f759,plain,(
% 9.87/2.28    ! [X0 : 'A_b_b_c_LSCategory_ext_Category_ext$',X1 : 'A$',X2 : 'A$',X3 : 'ZF$'] : (('fun_app$l'('mapsTo$'(X0,'zF2mor$'(X0,X3),X1),X2) & 'fun_app$p'('mor2ZF$'(X0),'zF2mor$'(X0,X3)) = X3) | ~'lSCategory$'(X0) | ~'member$i'(X1,'obj$b'(X0)) | ~'member$i'(X2,'obj$b'(X0)) | ~'fun_app$b'('elem$'(X3),'homSet$'(X0,X1,X2)))),
% 9.87/2.28    inference(flattening,[],[f758])).
% 9.87/2.28  
% 9.87/2.28  tff(f1730,plain,(
% 9.87/2.28    'yMapInv$'('c$','x$','mapO$'('yFtor$'('c$'),'y$'),'fun_app$p'('mor2ZF$'('c$'),'zF2mor$'('c$','yMap$'('c$','x$','eta$')))) != 'yMapInv$'('c$','x$','mapO$'('yFtor$'('c$'),'y$'),'yMap$'('c$','x$','eta$'))),
% 9.87/2.28    inference(cnf_transformation,[],[f627])).
% 9.87/2.28  
% 9.87/2.28  tff(f1731,plain,(
% 9.87/2.28    'lSCategory$'('c$')),
% 9.87/2.28    inference(cnf_transformation,[],[f37])).
% 9.87/2.28  
% 9.87/2.28  tff(f1732,plain,(
% 9.87/2.28    'member$i'('x$','obj$b'('c$'))),
% 9.87/2.28    inference(cnf_transformation,[],[f38])).
% 9.87/2.28  
% 9.87/2.28  tff(f1733,plain,(
% 9.87/2.28    'member$i'('y$','obj$b'('c$'))),
% 9.87/2.28    inference(cnf_transformation,[],[f39])).
% 9.87/2.28  
% 9.87/2.28  tff(f1735,plain,(
% 9.87/2.28    'fun_app$b'('elem$'('yMap$'('c$','x$','eta$')),'homSet$'('c$','x$','y$'))),
% 9.87/2.28    inference(cnf_transformation,[],[f41])).
% 9.87/2.28  
% 9.87/2.28  tff(f1736,plain,(
% 9.87/2.28    'yMapInv$'('c$','x$','mapO$'('yFtor$'('c$'),'y$'),'fun_app$p'('mor2ZF$'('c$'),'zF2mor$'('c$','yMap$'('c$','x$','eta$')))) = 'fun_app$q'('mapM$'('yFtor$'('c$')),'zF2mor$'('c$','yMap$'('c$','x$','eta$')))),
% 9.87/2.28    inference(cnf_transformation,[],[f42])).
% 9.87/2.28  
% 9.87/2.28  tff(f1743,plain,(
% 9.87/2.28    ( ! [X2 : 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$',X3 : 'ZF$',X0 : 'A_b_b_c_LSCategory_ext_Category_ext$',X1 : 'A$'] : ('yMapInv$'(X0,X1,X2,X3) = 'makeNT$'('yMapInv$a'(X0,X1,X2,X3))) )),
% 9.87/2.28    inference(cnf_transformation,[],[f49])).
% 9.87/2.28  
% 9.87/2.28  tff(f1772,plain,(
% 9.87/2.28    ( ! [X2 : 'A$',X3 : 'ZF$',X0 : 'A_b_b_c_LSCategory_ext_Category_ext$',X1 : 'A$'] : ('fun_app$p'('mor2ZF$'(X0),'zF2mor$'(X0,X3)) = X3 | ~'lSCategory$'(X0) | ~'member$i'(X1,'obj$b'(X0)) | ~'member$i'(X2,'obj$b'(X0)) | ~'fun_app$b'('elem$'(X3),'homSet$'(X0,X1,X2))) )),
% 9.87/2.28    inference(cnf_transformation,[],[f759])).
% 9.87/2.28  
% 9.87/2.28  tff(f2042,plain,(
% 9.87/2.28    ( ! [X0 : 'A_b_b_c_LSCategory_ext_Category_ext$'] : ('yFtor$'(X0) = 'makeFtor$d'('yFtor$a'(X0))) )),
% 9.87/2.28    inference(cnf_transformation,[],[f341])).
% 9.87/2.28  
% 9.87/2.28  tff(f2339,plain,(
% 9.87/2.28    ( ! [X2 : 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$',X0 : 'A_b_b_c_LSCategory_ext_Category_ext$',X1 : 'A$'] : ('yMap$'(X0,X1,X2) = 'fun_app$'('fun_app$m'('zFfunApp$','natTransMap$b'(X2,X1)),'fun_app$p'('mor2ZF$'(X0),'fun_app$r'('id$b'(X0),X1)))) )),
% 9.87/2.28    inference(cnf_transformation,[],[f468])).
% 9.87/2.28  
% 9.87/2.28  tff(f2367,plain,(
% 9.87/2.28    ( ! [X0 : 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$'] : ('makeFtor$d'(X0) = 'functor_ext$'('catDom$'(X0),'catCod$'(X0),'restrict$b'('mapM$'(X0),'mor$'('catDom$'(X0))),'more$c'(X0))) )),
% 9.87/2.28    inference(cnf_transformation,[],[f489])).
% 9.87/2.28  
% 9.87/2.28  tff(f2498,plain,(
% 9.87/2.28    ( ! [X0 : 'A_b_b_c_LSCategory_ext_Category_ext$'] : ('oppositeCategory$'(X0) = 'category_ext$'('obj$b'(X0),'mor$'(X0),'cod$'(X0),'dom$'(X0),'id$b'(X0),'uuj$'(X0),'more$a'(X0))) )),
% 9.87/2.28    inference(cnf_transformation,[],[f546])).
% 9.87/2.28  
% 9.87/2.28  tff(f2510,plain,(
% 9.87/2.28    ( ! [X0 : 'A_b_b_c_LSCategory_ext_Category_ext$'] : ('yFtor$a'(X0) = 'functor_ext$'(X0,'catExp$'('oppositeCategory$'(X0),'set$'),'yFtorNT$'(X0),'unity$')) )),
% 9.87/2.28    inference(cnf_transformation,[],[f558])).
% 9.87/2.28  
% 9.87/2.28  tff(f2512,plain,(
% 9.87/2.28    ( ! [X2 : 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$',X3 : 'ZF$',X0 : 'A_b_b_c_LSCategory_ext_Category_ext$',X1 : 'A$'] : ('yMapInv$a'(X0,X1,X2,X3) = 'natTrans_ext$'('mapO$'('yFtor$'(X0),X1),X2,'uur$'(X0,X1,X2,X3),'unity$')) )),
% 9.87/2.28    inference(cnf_transformation,[],[f560])).
% 9.87/2.28  
% 9.87/2.28  tff(f2516,plain,(
% 9.87/2.28    ( ! [X0 : 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$',X1 : 'A$'] : ('mapO$'(X0,X1) = 'the$a'('uuv$'(X0,X1))) )),
% 9.87/2.28    inference(cnf_transformation,[],[f564])).
% 9.87/2.28  
% 9.87/2.28  tff(f2541,plain,(
% 9.87/2.28    ( ! [X0 : 'A_b_b_c_LSCategory_ext_Category_ext$',X1 : 'ZF$'] : ('zF2mor$'(X0,X1) = 'the$b'('uva$'(X0,X1))) )),
% 9.87/2.28    inference(cnf_transformation,[],[f581])).
% 9.87/2.28  
% 9.87/2.28  tff(f2559,plain,(
% 9.87/2.28    ( ! [X2 : 'A$',X0 : 'A_b_b_c_LSCategory_ext_Category_ext$',X1 : 'A$'] : ('hOMCollection$'(X0,X1,X2) = 'collect$c'('uvf$'(X0,X1,X2))) )),
% 9.87/2.28    inference(cnf_transformation,[],[f591])).
% 9.87/2.28  
% 9.87/2.28  tff(f2561,plain,(
% 9.87/2.28    ( ! [X2 : 'A$',X0 : 'A_b_b_c_LSCategory_ext_Category_ext$',X1 : 'A$'] : ('homSet$'(X0,X1,X2) = 'implode$'('hOMCollection$'(X0,X1,X2))) )),
% 9.87/2.28    inference(cnf_transformation,[],[f593])).
% 9.87/2.28  
% 9.87/2.28  tff(f2620,plain,(
% 9.87/2.28    ( ! [X0 : 'A_b_b_c_LSCategory_ext_Category_ext$'] : ('yFtor$a'(X0) = 'functor_ext$'(X0,'catExp$'('category_ext$'('obj$b'(X0),'mor$'(X0),'cod$'(X0),'dom$'(X0),'id$b'(X0),'uuj$'(X0),'more$a'(X0)),'set$'),'yFtorNT$'(X0),'unity$')) )),
% 9.87/2.28    inference(definition_unfolding,[],[f2510,f2498])).
% 9.87/2.28  
% 9.87/2.28  tff(f2623,plain,(
% 9.87/2.28    ( ! [X0 : 'A_b_b_c_LSCategory_ext_Category_ext$'] : ('yFtor$'(X0) = 'functor_ext$'('catDom$'('functor_ext$'(X0,'catExp$'('category_ext$'('obj$b'(X0),'mor$'(X0),'cod$'(X0),'dom$'(X0),'id$b'(X0),'uuj$'(X0),'more$a'(X0)),'set$'),'yFtorNT$'(X0),'unity$')),'catCod$'('functor_ext$'(X0,'catExp$'('category_ext$'('obj$b'(X0),'mor$'(X0),'cod$'(X0),'dom$'(X0),'id$b'(X0),'uuj$'(X0),'more$a'(X0)),'set$'),'yFtorNT$'(X0),'unity$')),'restrict$b'('mapM$'('functor_ext$'(X0,'catExp$'('category_ext$'('obj$b'(X0),'mor$'(X0),'cod$'(X0),'dom$'(X0),'id$b'(X0),'uuj$'(X0),'more$a'(X0)),'set$'),'yFtorNT$'(X0),'unity$')),'mor$'('catDom$'('functor_ext$'(X0,'catExp$'('category_ext$'('obj$b'(X0),'mor$'(X0),'cod$'(X0),'dom$'(X0),'id$b'(X0),'uuj$'(X0),'more$a'(X0)),'set$'),'yFtorNT$'(X0),'unity$')))),'more$c'('functor_ext$'(X0,'catExp$'('category_ext$'('obj$b'(X0),'mor$'(X0),'cod$'(X0),'dom$'(X0),'id$b'(X0),'uuj$'(X0),'more$a'(X0)),'set$'),'yFtorNT$'(X0),'unity$')))) )),
% 9.87/2.28    inference(definition_unfolding,[],[f2042,f2367,f2620])).
% 9.87/2.28  
% 9.87/2.28  tff(f2624,plain,(
% 9.87/2.28    ( ! [X2 : 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$',X3 : 'ZF$',X0 : 'A_b_b_c_LSCategory_ext_Category_ext$',X1 : 'A$'] : ('yMapInv$a'(X0,X1,X2,X3) = 'natTrans_ext$'('the$a'('uuv$'('functor_ext$'('catDom$'('functor_ext$'(X0,'catExp$'('category_ext$'('obj$b'(X0),'mor$'(X0),'cod$'(X0),'dom$'(X0),'id$b'(X0),'uuj$'(X0),'more$a'(X0)),'set$'),'yFtorNT$'(X0),'unity$')),'catCod$'('functor_ext$'(X0,'catExp$'('category_ext$'('obj$b'(X0),'mor$'(X0),'cod$'(X0),'dom$'(X0),'id$b'(X0),'uuj$'(X0),'more$a'(X0)),'set$'),'yFtorNT$'(X0),'unity$')),'restrict$b'('mapM$'('functor_ext$'(X0,'catExp$'('category_ext$'('obj$b'(X0),'mor$'(X0),'cod$'(X0),'dom$'(X0),'id$b'(X0),'uuj$'(X0),'more$a'(X0)),'set$'),'yFtorNT$'(X0),'unity$')),'mor$'('catDom$'('functor_ext$'(X0,'catExp$'('category_ext$'('obj$b'(X0),'mor$'(X0),'cod$'(X0),'dom$'(X0),'id$b'(X0),'uuj$'(X0),'more$a'(X0)),'set$'),'yFtorNT$'(X0),'unity$')))),'more$c'('functor_ext$'(X0,'catExp$'('category_ext$'('obj$b'(X0),'mor$'(X0),'cod$'(X0),'dom$'(X0),'id$b'(X0),'uuj$'(X0),'more$a'(X0)),'set$'),'yFtorNT$'(X0),'unity$'))),X1)),X2,'uur$'(X0,X1,X2,X3),'unity$')) )),
% 9.87/2.28    inference(definition_unfolding,[],[f2512,f2516,f2623])).
% 9.87/2.28  
% 9.87/2.28  tff(f2625,plain,(
% 9.87/2.28    ( ! [X2 : 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$',X3 : 'ZF$',X0 : 'A_b_b_c_LSCategory_ext_Category_ext$',X1 : 'A$'] : ('yMapInv$'(X0,X1,X2,X3) = 'makeNT$'('natTrans_ext$'('the$a'('uuv$'('functor_ext$'('catDom$'('functor_ext$'(X0,'catExp$'('category_ext$'('obj$b'(X0),'mor$'(X0),'cod$'(X0),'dom$'(X0),'id$b'(X0),'uuj$'(X0),'more$a'(X0)),'set$'),'yFtorNT$'(X0),'unity$')),'catCod$'('functor_ext$'(X0,'catExp$'('category_ext$'('obj$b'(X0),'mor$'(X0),'cod$'(X0),'dom$'(X0),'id$b'(X0),'uuj$'(X0),'more$a'(X0)),'set$'),'yFtorNT$'(X0),'unity$')),'restrict$b'('mapM$'('functor_ext$'(X0,'catExp$'('category_ext$'('obj$b'(X0),'mor$'(X0),'cod$'(X0),'dom$'(X0),'id$b'(X0),'uuj$'(X0),'more$a'(X0)),'set$'),'yFtorNT$'(X0),'unity$')),'mor$'('catDom$'('functor_ext$'(X0,'catExp$'('category_ext$'('obj$b'(X0),'mor$'(X0),'cod$'(X0),'dom$'(X0),'id$b'(X0),'uuj$'(X0),'more$a'(X0)),'set$'),'yFtorNT$'(X0),'unity$')))),'more$c'('functor_ext$'(X0,'catExp$'('category_ext$'('obj$b'(X0),'mor$'(X0),'cod$'(X0),'dom$'(X0),'id$b'(X0),'uuj$'(X0),'more$a'(X0)),'set$'),'yFtorNT$'(X0),'unity$'))),X1)),X2,'uur$'(X0,X1,X2,X3),'unity$'))) )),
% 9.87/2.28    inference(definition_unfolding,[],[f1743,f2624])).
% 9.87/2.28  
% 9.87/2.28  tff(f2626,plain,(
% 9.87/2.28    ( ! [X2 : 'A$',X0 : 'A_b_b_c_LSCategory_ext_Category_ext$',X1 : 'A$'] : ('homSet$'(X0,X1,X2) = 'implode$'('collect$c'('uvf$'(X0,X1,X2)))) )),
% 9.87/2.28    inference(definition_unfolding,[],[f2561,f2559])).
% 9.87/2.28  
% 9.87/2.28  tff(f2633,plain,(
% 9.87/2.28    'makeNT$'('natTrans_ext$'('the$a'('uuv$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$'))),'x$')),'the$a'('uuv$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$'))),'y$')),'uur$'('c$','x$','the$a'('uuv$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$'))),'y$')),'fun_app$p'('mor2ZF$'('c$'),'the$b'('uva$'('c$','fun_app$'('fun_app$m'('zFfunApp$','natTransMap$b'('eta$','x$')),'fun_app$p'('mor2ZF$'('c$'),'fun_app$r'('id$b'('c$'),'x$'))))))),'unity$')) != 'makeNT$'('natTrans_ext$'('the$a'('uuv$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$'))),'x$')),'the$a'('uuv$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$'))),'y$')),'uur$'('c$','x$','the$a'('uuv$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$'))),'y$')),'fun_app$'('fun_app$m'('zFfunApp$','natTransMap$b'('eta$','x$')),'fun_app$p'('mor2ZF$'('c$'),'fun_app$r'('id$b'('c$'),'x$')))),'unity$'))),
% 9.87/2.28    inference(definition_unfolding,[],[f1730,f2625,f2516,f2623,f2541,f2339,f2625,f2516,f2623,f2339])).
% 9.87/2.28  
% 9.87/2.28  tff(f2635,plain,(
% 9.87/2.28    'fun_app$b'('elem$'('fun_app$'('fun_app$m'('zFfunApp$','natTransMap$b'('eta$','x$')),'fun_app$p'('mor2ZF$'('c$'),'fun_app$r'('id$b'('c$'),'x$')))),'implode$'('collect$c'('uvf$'('c$','x$','y$'))))),
% 9.87/2.28    inference(definition_unfolding,[],[f1735,f2339,f2626])).
% 9.87/2.28  
% 9.87/2.28  tff(f2636,plain,(
% 9.87/2.28    'makeNT$'('natTrans_ext$'('the$a'('uuv$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$'))),'x$')),'the$a'('uuv$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$'))),'y$')),'uur$'('c$','x$','the$a'('uuv$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$'))),'y$')),'fun_app$p'('mor2ZF$'('c$'),'the$b'('uva$'('c$','fun_app$'('fun_app$m'('zFfunApp$','natTransMap$b'('eta$','x$')),'fun_app$p'('mor2ZF$'('c$'),'fun_app$r'('id$b'('c$'),'x$'))))))),'unity$')) = 'fun_app$q'('mapM$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'the$b'('uva$'('c$','fun_app$'('fun_app$m'('zFfunApp$','natTransMap$b'('eta$','x$')),'fun_app$p'('mor2ZF$'('c$'),'fun_app$r'('id$b'('c$'),'x$'))))))),
% 9.87/2.28    inference(definition_unfolding,[],[f1736,f2625,f2516,f2623,f2541,f2339,f2623,f2541,f2339])).
% 9.87/2.28  
% 9.87/2.28  tff(f2663,plain,(
% 9.87/2.28    ( ! [X2 : 'A$',X3 : 'ZF$',X0 : 'A_b_b_c_LSCategory_ext_Category_ext$',X1 : 'A$'] : ('fun_app$p'('mor2ZF$'(X0),'the$b'('uva$'(X0,X3))) = X3 | ~'lSCategory$'(X0) | ~'member$i'(X1,'obj$b'(X0)) | ~'member$i'(X2,'obj$b'(X0)) | ~'fun_app$b'('elem$'(X3),'implode$'('collect$c'('uvf$'(X0,X1,X2))))) )),
% 9.87/2.28    inference(definition_unfolding,[],[f1772,f2541,f2626])).
% 9.87/2.28  
% 9.87/2.28  tcf(c_110,negated_conjecture, 
% 9.87/2.28      ('makeNT$'('natTrans_ext$'('the$a'('uuv$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$'))),'x$')),'the$a'('uuv$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$'))),'y$')),'uur$'('c$','x$','the$a'('uuv$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$'))),'y$')),'fun_app$p'('mor2ZF$'('c$'),'the$b'('uva$'('c$','fun_app$'('fun_app$m'('zFfunApp$','natTransMap$b'('eta$','x$')),'fun_app$p'('mor2ZF$'('c$'),'fun_app$r'('id$b'('c$'),'x$'))))))),'unity$')) != 'makeNT$'('natTrans_ext$'('the$a'('uuv$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$'))),'x$')),'the$a'('uuv$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$'))),'y$')),'uur$'('c$','x$','the$a'('uuv$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$'))),'y$')),'fun_app$'('fun_app$m'('zFfunApp$','natTransMap$b'('eta$','x$')),'fun_app$p'('mor2ZF$'('c$'),'fun_app$r'('id$b'('c$'),'x$')))),'unity$'))),
% 9.87/2.28      inference(cnf_transformation,[],[f2633])).
% 9.87/2.28  
% 9.87/2.28  tcf(c_111,plain, 
% 9.87/2.28      ('lSCategory$'('c$')),
% 9.87/2.28      inference(cnf_transformation,[],[f1731])).
% 9.87/2.28  
% 9.87/2.28  tcf(c_112,plain, 
% 9.87/2.28      ('member$i'('x$','obj$b'('c$'))),
% 9.87/2.28      inference(cnf_transformation,[],[f1732])).
% 9.87/2.28  
% 9.87/2.28  tcf(c_113,plain, 
% 9.87/2.28      ('member$i'('y$','obj$b'('c$'))),
% 9.87/2.28      inference(cnf_transformation,[],[f1733])).
% 9.87/2.28  
% 9.87/2.28  tcf(c_115,plain, 
% 9.87/2.28      ('fun_app$b'('elem$'('fun_app$'('fun_app$m'('zFfunApp$','natTransMap$b'('eta$','x$')),'fun_app$p'('mor2ZF$'('c$'),'fun_app$r'('id$b'('c$'),'x$')))),'implode$'('collect$c'('uvf$'('c$','x$','y$'))))),
% 9.87/2.28      inference(cnf_transformation,[],[f2635])).
% 9.87/2.28  
% 9.87/2.28  tcf(c_116,plain, 
% 9.87/2.28      ('makeNT$'('natTrans_ext$'('the$a'('uuv$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$'))),'x$')),'the$a'('uuv$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$'))),'y$')),'uur$'('c$','x$','the$a'('uuv$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$'))),'y$')),'fun_app$p'('mor2ZF$'('c$'),'the$b'('uva$'('c$','fun_app$'('fun_app$m'('zFfunApp$','natTransMap$b'('eta$','x$')),'fun_app$p'('mor2ZF$'('c$'),'fun_app$r'('id$b'('c$'),'x$'))))))),'unity$')) = 'fun_app$q'('mapM$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'the$b'('uva$'('c$','fun_app$'('fun_app$m'('zFfunApp$','natTransMap$b'('eta$','x$')),'fun_app$p'('mor2ZF$'('c$'),'fun_app$r'('id$b'('c$'),'x$'))))))),
% 9.87/2.28      inference(cnf_transformation,[],[f2636])).
% 9.87/2.28  
% 9.87/2.28  tcf(c_152,plain,![X0_'A_b_b_c_LSCategory_ext_Category_ext':'A_b_b_c_LSCategory_ext_Category_ext$',X0_'A':'A$',X0_'ZF':'ZF$',X1_'A':'A$']:  
% 9.87/2.28      (~'fun_app$b'('elem$'(X0_'ZF'),'implode$'('collect$c'('uvf$'(X0_'A_b_b_c_LSCategory_ext_Category_ext',X0_'A',X1_'A'))))|
% 9.87/2.28      ~'member$i'(X0_'A','obj$b'(X0_'A_b_b_c_LSCategory_ext_Category_ext'))|
% 9.87/2.28      ~'member$i'(X1_'A','obj$b'(X0_'A_b_b_c_LSCategory_ext_Category_ext'))|
% 9.87/2.28      ~'lSCategory$'(X0_'A_b_b_c_LSCategory_ext_Category_ext')|'fun_app$p'('mor2ZF$'(X0_'A_b_b_c_LSCategory_ext_Category_ext'),'the$b'('uva$'(X0_'A_b_b_c_LSCategory_ext_Category_ext',X0_'ZF'))) = X0_'ZF'),
% 9.87/2.28      inference(cnf_transformation,[],[f2663])).
% 9.87/2.28  
% 9.87/2.28  tcf(c_1411,plain, 
% 9.87/2.28      (~'member$i'('x$','obj$b'('c$'))|~'member$i'('y$','obj$b'('c$'))|
% 9.87/2.28      ~'lSCategory$'('c$')|'fun_app$p'('mor2ZF$'('c$'),'the$b'('uva$'('c$','fun_app$'('fun_app$m'('zFfunApp$','natTransMap$b'('eta$','x$')),'fun_app$p'('mor2ZF$'('c$'),'fun_app$r'('id$b'('c$'),'x$')))))) = 'fun_app$'('fun_app$m'('zFfunApp$','natTransMap$b'('eta$','x$')),'fun_app$p'('mor2ZF$'('c$'),'fun_app$r'('id$b'('c$'),'x$')))),
% 9.87/2.28      inference(superposition,[status(thm)],[c_115,c_152])).
% 9.87/2.28  
% 9.87/2.28  tcf(c_1522,plain, 
% 9.87/2.28      ('makeNT$'('natTrans_ext$'('the$a'('uuv$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$'))),'x$')),'the$a'('uuv$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$'))),'y$')),'uur$'('c$','x$','the$a'('uuv$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$'))),'y$')),'fun_app$'('fun_app$m'('zFfunApp$','natTransMap$b'('eta$','x$')),'fun_app$p'('mor2ZF$'('c$'),'fun_app$r'('id$b'('c$'),'x$')))),'unity$')) != 'fun_app$q'('mapM$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'the$b'('uva$'('c$','fun_app$'('fun_app$m'('zFfunApp$','natTransMap$b'('eta$','x$')),'fun_app$p'('mor2ZF$'('c$'),'fun_app$r'('id$b'('c$'),'x$'))))))),
% 9.87/2.28      inference(light_normalisation,[status(thm)],[c_110,c_116])).
% 9.87/2.28  
% 9.87/2.28  tcf(c_1523,plain, 
% 9.87/2.28      ('fun_app$p'('mor2ZF$'('c$'),'the$b'('uva$'('c$','fun_app$'('fun_app$m'('zFfunApp$','natTransMap$b'('eta$','x$')),'fun_app$p'('mor2ZF$'('c$'),'fun_app$r'('id$b'('c$'),'x$')))))) = 'fun_app$'('fun_app$m'('zFfunApp$','natTransMap$b'('eta$','x$')),'fun_app$p'('mor2ZF$'('c$'),'fun_app$r'('id$b'('c$'),'x$')))),
% 9.87/2.28      inference(global_subsumption_just,
% 9.87/2.28                [status(thm)],
% 9.87/2.28                [c_1411,c_111,c_113,c_112,c_1411])).
% 9.87/2.28  
% 9.87/2.28  tcf(c_1527,plain, 
% 9.87/2.28      ('makeNT$'('natTrans_ext$'('the$a'('uuv$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$'))),'x$')),'the$a'('uuv$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$'))),'y$')),'uur$'('c$','x$','the$a'('uuv$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$'))),'y$')),'fun_app$'('fun_app$m'('zFfunApp$','natTransMap$b'('eta$','x$')),'fun_app$p'('mor2ZF$'('c$'),'fun_app$r'('id$b'('c$'),'x$')))),'unity$')) = 'fun_app$q'('mapM$'('functor_ext$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'catCod$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'restrict$b'('mapM$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')),'mor$'('catDom$'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'more$c'('functor_ext$'('c$','catExp$'('category_ext$'('obj$b'('c$'),'mor$'('c$'),'cod$'('c$'),'dom$'('c$'),'id$b'('c$'),'uuj$'('c$'),'more$a'('c$')),'set$'),'yFtorNT$'('c$'),'unity$')))),'the$b'('uva$'('c$','fun_app$'('fun_app$m'('zFfunApp$','natTransMap$b'('eta$','x$')),'fun_app$p'('mor2ZF$'('c$'),'fun_app$r'('id$b'('c$'),'x$'))))))),
% 9.87/2.28      inference(superposition,[status(thm)],[c_1523,c_116])).
% 9.87/2.28  
% 9.87/2.28  tcf(c_1529,plain, 
% 9.87/2.28      ($false),
% 9.87/2.28      inference(backward_subsumption_resolution,[status(thm)],[c_1522,c_1527])).
% 9.87/2.28  
% 9.87/2.28  
% 9.87/2.28  % SZS output end CNFRefutation for theBenchmark.p
% 9.87/2.28  
% 9.87/2.28  
%------------------------------------------------------------------------------