%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : ITP299_1 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n026.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:23 PM UTC 2026
% Result : Theorem 4.04s 1.70s
% Output : CNFRefutation 8.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP299_1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.35 % Computer : n026.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Wed Sep 23 18:24:24 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/0.39 Running TFA theorem proving
% 0.14/0.39 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s tfa_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.40
% 0.14/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.40
% 0.14/0.40 % Detected problem language: tptp
% 0.14/0.41 % Proving...
% 4.04/1.70 % SZS status Started for theBenchmark.p
% 4.04/1.70 % SZS status Theorem for theBenchmark.p
% 4.04/1.70
% 4.04/1.70 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 4.04/1.70
% 4.04/1.70 % ------ iProver source info
% 4.04/1.70
% 4.04/1.70 % git: date: 2026-07-19 20:42:38 +0200
% 4.04/1.70 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 4.04/1.70 % git: non_committed_changes: false
% 4.04/1.70
% 4.04/1.70 % ------ Parsing...
% 4.04/1.70 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 4.04/1.70
% 4.04/1.70 % ------ Preprocessing...%
% 4.04/1.70
% 4.04/1.70 % SZS status Theorem for theBenchmark.p
% 4.04/1.70
% 4.04/1.70 % SZS output start CNFRefutation for theBenchmark.p
% 4.04/1.70
% 4.04/1.70 tff(func_def_0, type, 'more$b': 'ZF_ZF_unit_Category_ext$' > 'Unit$').
% 4.04/1.70 tff(pred_def_1, type, 'fun_app$g': ('ZF_ZF_prod_ZF_fun_bool_fun$' * 'ZF_ZF_prod_ZF_fun$') > $o).
% 4.04/1.70 tff(pred_def_2, type, 'wellDefined$b': ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > $o).
% 4.04/1.70 tff(pred_def_3, type, 'signature$g': 'ZF_ZF_Expression_ZF_ZF_Language_unit_Signature_ext$' > $o).
% 4.04/1.70 tff(pred_def_4, type, 'fun_app$c': ('ZF_ZF_unit_TermEquivClT_ext_bool_fun$' * 'ZF_ZF_unit_TermEquivClT_ext$') > $o).
% 4.04/1.70 tff(pred_def_5, type, 'interpretation$e': 'ZF_ZF_ZF_Language_ZF_ZF_unit_Interpretation_ext$' > $o).
% 4.04/1.70 tff(pred_def_6, type, 'fun_app$q': ('ZF_ZF_ZF_Language_Language_bool_fun$' * 'ZF_ZF_ZF_Language_Language$') > $o).
% 4.04/1.70 tff(pred_def_7, type, 'signature$h': 'ZF_ZF_Expression_ZF_ZF_Expression_unit_Signature_ext$' > $o).
% 4.04/1.70 tff(pred_def_8, type, 'fun_app$e': ('ZF_ZF_prod_bool_fun$' * 'ZF_ZF_prod$') > $o).
% 4.04/1.70 tff(pred_def_9, type, 'wellDefined$c': ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > $o).
% 4.04/1.70 tff(pred_def_10, type, 'inj_on$': ('ZF_ZF_unit_TermEquivClT_ext_ZF_fun$' * 'ZF_ZF_unit_TermEquivClT_ext_set$') > $o).
% 4.04/1.70 tff(pred_def_11, type, 'signature$f': 'ZF_ZF_Expression_ZF_unit_Signature_ext$' > $o).
% 4.04/1.70 tff(pred_def_12, type, 'model$': ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_13, type, 'signature$a': 'ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' > $o).
% 4.04/1.70 tff(pred_def_14, type, 'fun_app$n': ('ZF_ZF_Language_ZF_ZF_Language_Language_bool_fun$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > $o).
% 4.04/1.70 tff(pred_def_15, type, 'fun_app$p': ('ZF_ZF_ZF_Expression_Language_bool_fun$' * 'ZF_ZF_ZF_Expression_Language$') > $o).
% 4.04/1.70 tff(pred_def_16, type, 'theoryp$a': ('ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > $o).
% 4.04/1.70 tff(pred_def_17, type, 'signature$c': 'ZF_ZF_Language_ZF_unit_Signature_ext$' > $o).
% 4.04/1.70 tff(pred_def_18, type, 'member$d': ('ZF$' * 'ZF_set$') > $o).
% 4.04/1.70 tff(pred_def_19, type, 'member$e': ('ZF_ZF_prod_ZF_fun$' * 'ZF_ZF_prod_ZF_fun_set$') > $o).
% 4.04/1.70 tff(pred_def_20, type, 'fun_app$o': ('ZF_ZF_Language_ZF_Language_bool_fun$' * 'ZF_ZF_Language_ZF_Language$') > $o).
% 4.04/1.70 tff(pred_def_21, type, 'member$j': ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_Language_set$') > $o).
% 4.04/1.70 tff(pred_def_22, type, 'model_axioms$': ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_23, type, 'inj_on$b': ('ZF_ZF_unit_TermEquivClT_ext_ZF_ZF_unit_TermEquivClT_ext_IType_ZF_ZF_IType_fun$' * 'ZF_ZF_unit_TermEquivClT_ext_ZF_ZF_unit_TermEquivClT_ext_IType_set$') > $o).
% 4.04/1.70 tff(pred_def_24, type, 'axioms$e': 'ZF_ZF_Expression_ZF_unit_Axioms_ext$' > $o).
% 4.04/1.70 tff(pred_def_25, type, 'interpretation$': 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$' > $o).
% 4.04/1.70 tff(pred_def_26, type, 'fun_app$f': ('ZF_bool_fun$' * 'ZF$') > $o).
% 4.04/1.70 tff(pred_def_27, type, 'interpretation$a': 'ZF_ZF_Language_ZF_ZF_Expression_ZF_ZF_unit_Interpretation_ext$' > $o).
% 4.04/1.70 tff(pred_def_28, type, 'interpretation$c': 'ZF_ZF_Language_ZF_ZF_ZF_unit_Interpretation_ext$' > $o).
% 4.04/1.70 tff(pred_def_29, type, 'fun_app$i': ('ZF_ZF_IType_bool_fun$' * 'ZF_ZF_IType$') > $o).
% 4.04/1.70 tff(pred_def_30, type, 'axioms$': 'ZF_ZF_unit_Axioms_ext$' > $o).
% 4.04/1.70 tff(pred_def_31, type, 'interp$': ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > $o).
% 4.04/1.70 tff(pred_def_32, type, 'inj_on$a': ('ZF_ZF_unit_TermEquivClT_ext_ZF_ZF_unit_TermEquivClT_ext_Language_ZF_ZF_Language_fun$' * 'ZF_ZF_unit_TermEquivClT_ext_ZF_ZF_unit_TermEquivClT_ext_Language_set$') > $o).
% 4.04/1.70 tff(pred_def_33, type, 'less_eq$a': ('ZF_ZF_Language_ZF_Language_set$' * 'ZF_ZF_Language_ZF_Language_set$') > $o).
% 4.04/1.70 tff(pred_def_34, type, 'wellDefined$e': ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > $o).
% 4.04/1.70 tff(pred_def_35, type, 'wellDefined$d': ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > $o).
% 4.04/1.70 tff(pred_def_36, type, 'theoryp$b': ('ZF_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_ZF_Language_Language$') > $o).
% 4.04/1.70 tff(pred_def_37, type, 'interpretation$b': 'ZF_ZF_Language_ZF_ZF_Language_ZF_ZF_unit_Interpretation_ext$' > $o).
% 4.04/1.70 tff(pred_def_38, type, 'axioms$a': 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$' > $o).
% 4.04/1.70 tff(pred_def_39, type, 'extCategory$': 'ZF_ZF_unit_Category_ext$' > $o).
% 4.04/1.70 tff(pred_def_40, type, 'signature$': 'ZF_ZF_unit_Signature_ext$' > $o).
% 4.04/1.70 tff(pred_def_41, type, 'signature$d': 'ZF_ZF_ZF_Expression_unit_Signature_ext$' > $o).
% 4.04/1.70 tff(pred_def_42, type, 'member$b': ('ZF_ZF_Expression$' * 'ZF_ZF_Expression_set$') > $o).
% 4.04/1.70 tff(pred_def_43, type, 'category$': 'ZF_ZF_unit_Category_ext$' > $o).
% 4.04/1.70 tff(pred_def_44, type, 'wellDefined$a': ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > $o).
% 4.04/1.70 tff(pred_def_45, type, 'member$f': ('ZF_ZF_fun$' * 'ZF_ZF_fun_set$') > $o).
% 4.04/1.70 tff(pred_def_46, type, 'member$g': ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_Language_set$') > $o).
% 4.04/1.70 tff(pred_def_47, type, 'zFAxioms$': 'ZF_ZF_unit_Axioms_ext$' > $o).
% 4.04/1.70 tff(pred_def_48, type, 'member$c': ('ZF_ZF_prod$' * 'ZF_ZF_prod_set$') > $o).
% 4.04/1.70 tff(pred_def_49, type, 'fun_app$d': ('ZF_ZF_Expression_bool_fun$' * 'ZF_ZF_Expression$') > $o).
% 4.04/1.70 tff(pred_def_50, type, 'less_eq$b': ('ZF_ZF_ZF_Expression_Language_set$' * 'ZF_ZF_ZF_Expression_Language_set$') > $o).
% 4.04/1.70 tff(pred_def_51, type, 'fun_app$b': ('ZF_ZF_Language_bool_fun$' * 'ZF_ZF_Language$') > $o).
% 4.04/1.70 tff(pred_def_52, type, 'axioms$b': 'ZF_ZF_Language_ZF_unit_Axioms_ext$' > $o).
% 4.04/1.70 tff(pred_def_53, type, 'less_eq$': ('ZF_ZF_Language_ZF_ZF_Language_Language_set$' * 'ZF_ZF_Language_ZF_ZF_Language_Language_set$') > $o).
% 4.04/1.70 tff(pred_def_54, type, 'inj_on$c': ('ZF_ZF_unit_TermEquivClT_ext_ZF_ZF_unit_TermEquivClT_ext_Expression_ZF_ZF_Expression_fun$' * 'ZF_ZF_unit_TermEquivClT_ext_ZF_ZF_unit_TermEquivClT_ext_Expression_set$') > $o).
% 4.04/1.70 tff(pred_def_55, type, 'axioms$c': 'ZF_ZF_ZF_Expression_unit_Axioms_ext$' > $o).
% 4.04/1.70 tff(pred_def_56, type, 'theoryp$c': ('ZF_ZF_Expression_ZF_unit_Axioms_ext$' * 'ZF_ZF_Expression_ZF_Language$') > $o).
% 4.04/1.70 tff(pred_def_57, type, 'interpretation$d': 'ZF_ZF_ZF_Expression_ZF_ZF_unit_Interpretation_ext$' > $o).
% 4.04/1.70 tff(pred_def_58, type, 'axioms$d': 'ZF_ZF_ZF_Language_unit_Axioms_ext$' > $o).
% 4.04/1.70 tff(pred_def_59, type, 'less_eq$c': ('ZF_ZF_ZF_Language_Language_set$' * 'ZF_ZF_ZF_Language_Language_set$') > $o).
% 4.04/1.70 tff(pred_def_60, type, 'category_axioms$': 'ZF_ZF_unit_Category_ext$' > $o).
% 4.04/1.70 tff(pred_def_61, type, 'member$i': ('ZF_ZF_Expression_ZF_Language$' * 'ZF_ZF_Expression_ZF_Language_set$') > $o).
% 4.04/1.70 tff(pred_def_62, type, 'zFAxioms_axioms$': 'ZF_ZF_unit_Axioms_ext$' > $o).
% 4.04/1.70 tff(pred_def_63, type, 'member$': ('ZF_ZF_Language$' * 'ZF_ZF_Language_set$') > $o).
% 4.04/1.70 tff(pred_def_64, type, 'less_eq$d': ('ZF_ZF_Language_set$' * 'ZF_ZF_Language_set$') > $o).
% 4.04/1.70 tff(pred_def_65, type, 'interpretation$f': 'ZF_ZF_Expression_ZF_ZF_ZF_unit_Interpretation_ext$' > $o).
% 4.04/1.70 tff(pred_def_66, type, 'member$a': ('ZF_ZF_unit_TermEquivClT_ext$' * 'ZF_ZF_unit_TermEquivClT_ext_set$') > $o).
% 4.04/1.70 tff(pred_def_67, type, 'fun_app$h': ('ZF_ZF_fun_bool_fun$' * 'ZF_ZF_fun$') > $o).
% 4.04/1.70 tff(pred_def_68, type, 'signature$b': 'ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' > $o).
% 4.04/1.70 tff(pred_def_69, type, 'theoryp$d': ('ZF_ZF_Language_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_Language$') > $o).
% 4.04/1.70 tff(pred_def_70, type, 'signature$e': 'ZF_ZF_ZF_Language_unit_Signature_ext$' > $o).
% 4.04/1.70 tff(pred_def_71, type, 'member$h': ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_Language_set$') > $o).
% 4.04/1.70 tff(pred_def_72, type, 'signature$i': 'ZF_ZF_fun_ZF_unit_Signature_ext$' > $o).
% 4.04/1.70 tff(pred_def_73, type, 'wellDefined$f': ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > $o).
% 4.04/1.70 tff(func_def_74, type, 'funsignature_abbrev$b': ('ZF$' * 'ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression$') > 'ZF_ZF_Expression_bool_fun$').
% 4.04/1.70 tff(func_def_75, type, 'map_IType$a': ('ZF_ZF_ZF_unit_TermEquivClT_ext_fun$' * 'ZF_ZF_ZF_unit_TermEquivClT_ext_fun$' * 'ZF_ZF_IType$') > 'ZF_ZF_unit_TermEquivClT_ext_ZF_ZF_unit_TermEquivClT_ext_IType$').
% 4.04/1.70 tff(pred_def_76, type, sP0: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_77, type, sP1: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_78, type, sP2: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_79, type, sP3: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_80, type, sP4: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_81, type, sP5: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_82, type, sP6: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_83, type, sP7: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_84, type, sP8: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_85, type, sP9: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_86, type, sP10: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_87, type, sP11: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_88, type, sP12: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_89, type, sP13: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_90, type, sP14: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_91, type, sP15: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_92, type, sP16: ('ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > $o).
% 4.04/1.70 tff(pred_def_93, type, sP17: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_94, type, sP18: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_95, type, sP19: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_96, type, sP20: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_97, type, sP21: ('ZF_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_ZF_Language_Language$') > $o).
% 4.04/1.70 tff(pred_def_98, type, sP22: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_99, type, sP23: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_100, type, sP24: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_101, type, sP25: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_102, type, sP26: ('ZF_ZF_Language_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_Language$') > $o).
% 4.04/1.70 tff(pred_def_103, type, sP27: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_104, type, sP28: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_105, type, sP29: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_106, type, sP30: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_107, type, sP31: ('ZF_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language$') > $o).
% 4.04/1.70 tff(pred_def_108, type, sP32: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 4.04/1.70 tff(pred_def_109, type, sP33: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_110, type, sP34: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_111, type, sP35: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_112, type, sP36: ('ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > $o).
% 8.43/1.70 tff(pred_def_113, type, sP37: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_114, type, sP38: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_115, type, sP39: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_116, type, sP40: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_117, type, sP41: ('ZF_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_ZF_Language_Language$') > $o).
% 8.43/1.70 tff(pred_def_118, type, sP42: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_119, type, sP43: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_120, type, sP44: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_121, type, sP45: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_122, type, sP46: ('ZF_ZF_Language_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_Language$') > $o).
% 8.43/1.70 tff(pred_def_123, type, sP47: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_124, type, sP48: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_125, type, sP49: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_126, type, sP50: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_127, type, sP51: ('ZF_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language$') > $o).
% 8.43/1.70 tff(pred_def_128, type, sP52: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_129, type, sP53: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_130, type, sP54: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_131, type, sP55: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_132, type, sP56: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_133, type, sP57: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_134, type, sP58: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_135, type, sP59: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_136, type, sP60: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_137, type, sP61: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_138, type, sP62: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_139, type, sP63: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > $o).
% 8.43/1.70 tff(pred_def_140, type, sP64: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > $o).
% 8.43/1.70 tff(pred_def_141, type, sP65: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > $o).
% 8.43/1.70 tff(pred_def_142, type, sP66: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > $o).
% 8.43/1.70 tff(pred_def_143, type, sP67: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > $o).
% 8.43/1.70 tff(pred_def_144, type, sP68: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > $o).
% 8.43/1.70 tff(pred_def_145, type, sP69: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > $o).
% 8.43/1.70 tff(pred_def_146, type, sP70: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > $o).
% 8.43/1.70 tff(pred_def_147, type, sP71: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > $o).
% 8.43/1.70 tff(pred_def_148, type, sP72: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > $o).
% 8.43/1.70 tff(pred_def_149, type, sP73: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > $o).
% 8.43/1.70 tff(pred_def_150, type, sP74: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > $o).
% 8.43/1.70 tff(pred_def_151, type, sP75: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > $o).
% 8.43/1.70 tff(pred_def_152, type, sP76: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > $o).
% 8.43/1.70 tff(pred_def_153, type, sP77: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > $o).
% 8.43/1.70 tff(pred_def_154, type, sP78: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > $o).
% 8.43/1.70 tff(pred_def_155, type, sP79: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > $o).
% 8.43/1.70 tff(pred_def_156, type, sP80: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > $o).
% 8.43/1.70 tff(pred_def_157, type, sP81: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > $o).
% 8.43/1.70 tff(pred_def_158, type, sP82: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > $o).
% 8.43/1.70 tff(pred_def_159, type, sP83: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > $o).
% 8.43/1.70 tff(pred_def_160, type, sP84: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > $o).
% 8.43/1.70 tff(pred_def_161, type, sP85: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > $o).
% 8.43/1.70 tff(pred_def_162, type, sP86: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > $o).
% 8.43/1.70 tff(pred_def_163, type, sP87: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > $o).
% 8.43/1.70 tff(pred_def_164, type, sP88: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > $o).
% 8.43/1.70 tff(pred_def_165, type, sP89: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > $o).
% 8.43/1.70 tff(pred_def_166, type, sP90: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > $o).
% 8.43/1.70 tff(pred_def_167, type, sP91: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > $o).
% 8.43/1.70 tff(pred_def_168, type, sP92: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > $o).
% 8.43/1.70 tff(pred_def_169, type, sP93: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > $o).
% 8.43/1.70 tff(pred_def_170, type, sP94: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > $o).
% 8.43/1.70 tff(pred_def_171, type, sP95: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > $o).
% 8.43/1.70 tff(pred_def_172, type, sP96: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > $o).
% 8.43/1.70 tff(pred_def_173, type, sP97: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > $o).
% 8.43/1.70 tff(pred_def_174, type, sP98: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > $o).
% 8.43/1.70 tff(pred_def_175, type, sP99: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > $o).
% 8.43/1.70 tff(pred_def_176, type, sP100: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > $o).
% 8.43/1.70 tff(pred_def_177, type, sP101: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > $o).
% 8.43/1.70 tff(pred_def_178, type, sP102: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > $o).
% 8.43/1.70 tff(pred_def_179, type, sP103: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > $o).
% 8.43/1.70 tff(pred_def_180, type, sP104: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > $o).
% 8.43/1.70 tff(pred_def_181, type, sP105: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > $o).
% 8.43/1.70 tff(pred_def_182, type, sP106: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > $o).
% 8.43/1.70 tff(pred_def_183, type, sP107: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > $o).
% 8.43/1.70 tff(pred_def_184, type, sP108: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > $o).
% 8.43/1.70 tff(pred_def_185, type, sP109: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > $o).
% 8.43/1.70 tff(pred_def_186, type, sP110: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > $o).
% 8.43/1.70 tff(pred_def_187, type, sP111: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > $o).
% 8.43/1.70 tff(pred_def_188, type, sP112: 'ZF_ZF_unit_Category_ext$' > $o).
% 8.43/1.70 tff(pred_def_189, type, sP113: 'ZF_ZF_unit_Category_ext$' > $o).
% 8.43/1.70 tff(pred_def_190, type, sP114: 'ZF_ZF_unit_Category_ext$' > $o).
% 8.43/1.70 tff(pred_def_191, type, sP115: 'ZF_ZF_unit_Category_ext$' > $o).
% 8.43/1.70 tff(pred_def_192, type, sP116: 'ZF_ZF_unit_Category_ext$' > $o).
% 8.43/1.70 tff(pred_def_193, type, sP117: 'ZF_ZF_unit_Category_ext$' > $o).
% 8.43/1.70 tff(pred_def_194, type, sP118: 'ZF_ZF_unit_Category_ext$' > $o).
% 8.43/1.70 tff(pred_def_195, type, sP119: 'ZF_ZF_unit_Category_ext$' > $o).
% 8.43/1.70 tff(pred_def_196, type, sP120: 'ZF_ZF_unit_Category_ext$' > $o).
% 8.43/1.70 tff(pred_def_197, type, sP121: 'ZF_ZF_IType_ZF_ZF_IType_bool_fun_fun$' > $o).
% 8.43/1.70 tff(pred_def_198, type, sP122: ('ZF_ZF_IType$' * 'ZF_ZF_IType$') > $o).
% 8.43/1.70 tff(pred_def_199, type, sP123: ('ZF_ZF_IType$' * 'ZF_ZF_IType$' * 'ZF_ZF_bool_fun_fun$') > $o).
% 8.43/1.70 tff(func_def_200, type, 'theory$a': 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$' > 'ZF_ZF_Language_ZF_ZF_Language_Language_set$').
% 8.43/1.70 tff(func_def_201, type, 'sup$': 'ZF_ZF_Expression_set$' > 'ZF_ZF_Expression_set_ZF_ZF_Expression_set_fun$').
% 8.43/1.70 tff(func_def_202, type, 'term$a': ('ZF_ZF_Language$' * 'ZF_ZF_Language_ZF_ZF_Expression_Expression$' * 'ZF_ZF_Language$') > 'ZF_ZF_Language_ZF_ZF_Expression_Language$').
% 8.43/1.70 tff(func_def_203, type, 'collect$a': 'ZF_ZF_fun_bool_fun$' > 'ZF_ZF_fun_set$').
% 8.43/1.70 tff(func_def_204, type, 'uut$': 'ZF_ZF_unit_Axioms_ext$' > 'ZF_ZF_Language_bool_fun$').
% 8.43/1.70 tff(func_def_205, type, 'baseTypes$': 'ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' > 'ZF_ZF_Language_set$').
% 8.43/1.70 tff(func_def_206, type, 'subst$d': ('ZF_ZF_Language_ZF_Expression$' * 'ZF_ZF_Language_ZF_Expression$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_207, type, 'uuh$': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_ZF_fun_fun$').
% 8.43/1.70 tff(func_def_208, type, 'fun_app$ah': ('ZF_ZF_unit_TermEquivClT_ext_ZF_ZF_unit_TermEquivClT_ext_Language_ZF_ZF_Language_fun$' * 'ZF_ZF_unit_TermEquivClT_ext_ZF_ZF_unit_TermEquivClT_ext_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_209, type, 'theory$c': 'ZF_ZF_Expression_ZF_unit_Axioms_ext$' > 'ZF_ZF_Expression_ZF_Language_set$').
% 8.43/1.70 tff(func_def_210, type, 'fun_app$af': ('ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$' * 'ZF_ZF_ZF_fun_fun$') > 'ZF_ZF_ZF_fun_fun$').
% 8.43/1.70 tff(func_def_211, type, 'map_IType$b': ('ZF_ZF_fun$' * 'ZF_ZF_fun$' * 'ZF_ZF_IType$') > 'ZF_ZF_IType$').
% 8.43/1.70 tff(func_def_212, type, 'collect$i': 'ZF_ZF_ZF_Expression_Language_bool_fun$' > 'ZF_ZF_ZF_Expression_Language_set$').
% 8.43/1.70 tff(func_def_213, type, 'restrict$': ('ZF_ZF_prod_ZF_fun$' * 'ZF_ZF_prod_set$') > 'ZF_ZF_prod_ZF_fun$').
% 8.43/1.70 tff(func_def_214, type, 'baseFunctions$f': 'ZF_ZF_Expression_ZF_ZF_Language_unit_Signature_ext$' > 'ZF_ZF_Language_set$').
% 8.43/1.70 tff(func_def_215, type, 'aAxioms$d': 'ZF_ZF_Language_ZF_unit_Axioms_ext$' > 'ZF_ZF_Language_ZF_Language_set$').
% 8.43/1.70 tff(func_def_216, type, 'iFunctions$d': 'ZF_ZF_Expression_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_fun$').
% 8.43/1.70 tff(func_def_217, type, 'fun_app$ag': ('ZF_ZF_unit_TermEquivClT_ext_ZF_fun$' * 'ZF_ZF_unit_TermEquivClT_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_218, type, 'sigDom$g': 'ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' > 'ZF_ZF_Expression_ZF_ZF_Language_fun$').
% 8.43/1.70 tff(func_def_219, type, 'fun_app$ak': ('ZF_ZF_Expression_nat_fun$' * 'ZF_ZF_Expression$') > 'Nat$').
% 8.43/1.70 tff(func_def_220, type, 'more$a': 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$' > 'Unit$').
% 8.43/1.70 tff(func_def_221, type, 'term$': ('ZF$' * 'ZF_ZF_Expression$') > 'ZF_ZF_ZF_Language_fun$').
% 8.43/1.70 tff(func_def_222, type, 'funsignature_abbrev$e': ('ZF_ZF_Expression$' * 'ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF_ZF_Language_bool_fun$').
% 8.43/1.70 tff(func_def_223, type, 'mor$': 'ZF_ZF_unit_Category_ext$' > 'ZF_set$').
% 8.43/1.70 tff(func_def_224, type, 'uug$': 'ZF_ZF_unit_Axioms_ext$' > 'ZF_ZF_Language_bool_fun$').
% 8.43/1.70 tff(func_def_225, type, 'signature_ext$b': ('ZF_ZF_Language_set$' * 'ZF_set$' * 'ZF_ZF_ZF_Language_fun$' * 'ZF_ZF_ZF_Language_fun$' * 'Unit$') > 'ZF_ZF_Language_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_226, type, 'baseTypes$h': 'ZF_ZF_Expression_ZF_ZF_Expression_unit_Signature_ext$' > 'ZF_ZF_Expression_set$').
% 8.43/1.70 tff(func_def_227, type, 'comp$': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_ZF_fun_fun$').
% 8.43/1.70 tff(func_def_228, type, 'mapsTo$': ('ZF_ZF_unit_Category_ext$' * 'ZF$') > 'ZF_ZF_bool_fun_fun$').
% 8.43/1.70 tff(func_def_229, type, 'funsignature_abbrev$f': ('ZF_ZF_Expression$' * 'ZF_ZF_ZF_Expression_unit_Signature_ext$') > 'ZF_ZF_bool_fun_fun$').
% 8.43/1.70 tff(func_def_230, type, 'iCategory$e': 'ZF_ZF_ZF_Language_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_unit_Category_ext$').
% 8.43/1.70 tff(func_def_231, type, tlfalse: tlbool).
% 8.43/1.70 tff(func_def_232, type, 'nat$': $int > 'Nat$').
% 8.43/1.70 tff(func_def_233, type, 'tDomain$': 'ZF_ZF_unit_TermEquivClT_ext_ZF_fun$').
% 8.43/1.70 tff(func_def_234, type, 'oppositeCategory$': 'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$').
% 8.43/1.70 tff(func_def_235, type, 'termEquivCl$': ('ZF_ZF_unit_Axioms_ext$' * 'ZF$' * 'ZF_ZF_Expression$') > 'ZF_ZF_fun$').
% 8.43/1.70 tff(func_def_236, type, 'obj$': 'ZF_ZF_unit_Category_ext$' > 'ZF_set$').
% 8.43/1.70 tff(func_def_237, type, 'exprVar$f': 'ZF_ZF_Expression_ZF_Expression$').
% 8.43/1.70 tff(func_def_238, type, 'more$': 'ZF_ZF_unit_Axioms_ext$' > 'Unit$').
% 8.43/1.70 tff(func_def_239, type, 'canonicalCat$': 'ZF_ZF_unit_Axioms_ext$' > 'ZF_ZF_unit_Category_ext$').
% 8.43/1.70 tff(func_def_240, type, 'fun_app$y': ('ZF_ZF_unit_Signature_ext_ZF_ZF_unit_Signature_ext_fun$' * 'ZF_ZF_unit_Signature_ext$') > 'ZF_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_241, type, 'zF2m$': 'ZF_ZF_unit_Axioms_ext$' > 'ZF_ZF_ZF_unit_TermEquivClT_ext_fun$').
% 8.43/1.70 tff(func_def_242, type, 'iFunctions$': 'ZF_ZF_Language_ZF_ZF_Expression_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Expression_ZF_fun$').
% 8.43/1.70 tff(func_def_243, type, 'iSignature$e': 'ZF_ZF_ZF_Language_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_ZF_Language_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_244, type, 't$': 'ZF_ZF_unit_Axioms_ext$').
% 8.43/1.70 tff(func_def_245, type, 'baseFunctions$': 'ZF_ZF_unit_Signature_ext$' > 'ZF_set$').
% 8.43/1.70 tff(func_def_246, type, 'aSignature$': 'ZF_ZF_unit_Axioms_ext$' > 'ZF_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_247, type, 'objIso$': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_bool_fun_fun$').
% 8.43/1.70 tff(func_def_248, type, 'term$c': ('ZF_ZF_Language$' * 'ZF_ZF_Language_ZF_Expression$' * 'ZF_ZF_Language$') > 'ZF_ZF_Language_ZF_Language$').
% 8.43/1.70 tff(func_def_249, type, 'baseTypes$c': 'ZF_ZF_ZF_Expression_unit_Signature_ext$' > 'ZF_set$').
% 8.43/1.70 tff(func_def_250, type, 'fun_app$w': ('ZF_ZF_Expression_ZF_fun$' * 'ZF_ZF_Expression$') > 'ZF$').
% 8.43/1.70 tff(func_def_251, type, 'fun_app$aa': ('ZF_ZF_fun_ZF_ZF_fun_fun$' * 'ZF_ZF_fun$') > 'ZF_ZF_fun$').
% 8.43/1.70 tff(func_def_252, type, 'makeCat$': 'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$').
% 8.43/1.70 tff(func_def_253, type, 'phi$': 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_254, type, 'extensional$': 'ZF_set$' > 'ZF_ZF_fun_set$').
% 8.43/1.70 tff(func_def_255, type, 'sigCod$g': 'ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' > 'ZF_ZF_Expression_ZF_ZF_Language_fun$').
% 8.43/1.70 tff(func_def_256, type, 'signature_ext$d': ('ZF_set$' * 'ZF_ZF_Language_set$' * 'ZF_ZF_Language_ZF_fun$' * 'ZF_ZF_Language_ZF_fun$' * 'Unit$') > 'ZF_ZF_ZF_Language_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_257, type, 'equation$b': ('ZF$' * 'ZF_ZF_ZF_Expression_Expression$' * 'ZF_ZF_ZF_Expression_Expression$' * 'ZF$') > 'ZF_ZF_ZF_Expression_Language$').
% 8.43/1.70 tff(func_def_258, type, 'funsignature_abbrev$d': ('ZF$' * 'ZF_ZF_unit_Signature_ext$') > 'ZF_ZF_bool_fun_fun$').
% 8.43/1.70 tff(func_def_259, type, 'type$b': 'ZF_ZF_Language$' > 'ZF_ZF_Language_ZF_ZF_Language_Language$').
% 8.43/1.70 tff(func_def_260, type, 'uun$': ('ZF_ZF_unit_Axioms_ext$' * 'ZF$') > 'ZF_ZF_bool_fun_fun$').
% 8.43/1.70 tff(func_def_261, type, 'isomorphism$': 'ZF_ZF_unit_Category_ext$' > 'ZF_bool_fun$').
% 8.43/1.70 tff(func_def_262, type, 'funsignature_abbrev$': ('ZF_ZF_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF_ZF_Language_bool_fun$').
% 8.43/1.70 tff(func_def_263, type, 'aSignature_update$': ('ZF_ZF_unit_Signature_ext_ZF_ZF_unit_Signature_ext_fun$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_unit_Axioms_ext$').
% 8.43/1.70 tff(func_def_264, type, 'iTypes$': 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_fun$').
% 8.43/1.70 tff(func_def_265, type, 'collect$e': 'ZF_ZF_Expression_bool_fun$' > 'ZF_ZF_Expression_set$').
% 8.43/1.70 tff(func_def_266, type, 'baseTypes$b': 'ZF_ZF_Language_ZF_unit_Signature_ext$' > 'ZF_ZF_Language_set$').
% 8.43/1.70 tff(func_def_267, type, 'aSignature$a': 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$' > 'ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_268, type, 'top$': 'ZF_ZF_unit_TermEquivClT_ext_set$').
% 8.43/1.70 tff(func_def_269, type, 'canonicalInterpretation$': 'ZF_ZF_unit_Axioms_ext$' > 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$').
% 8.43/1.70 tff(func_def_270, type, 'type$e': 'ZF_ZF_Language$' > 'ZF_ZF_Language_ZF_Language$').
% 8.43/1.70 tff(func_def_271, type, 'cod$': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_fun$').
% 8.43/1.70 tff(func_def_272, type, 'pair$': ('ZF$' * 'ZF$') > 'ZF_ZF_prod$').
% 8.43/1.70 tff(func_def_273, type, 'baseFunctions_update$a': ('ZF_ZF_Language_set_ZF_ZF_Language_set_fun$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_274, type, 'iSignature$d': 'ZF_ZF_ZF_Expression_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_ZF_Expression_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_275, type, 'exprVar$e': 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_276, type, 'map_IType$': ('ZF_ZF_unit_TermEquivClT_ext_ZF_fun$' * 'ZF_ZF_unit_TermEquivClT_ext_ZF_fun$') > 'ZF_ZF_unit_TermEquivClT_ext_ZF_ZF_unit_TermEquivClT_ext_IType_ZF_ZF_IType_fun$').
% 8.43/1.70 tff(func_def_277, type, 'term$e': ('ZF$' * 'ZF_ZF_ZF_Language_Expression$' * 'ZF$') > 'ZF_ZF_ZF_Language_Language$').
% 8.43/1.70 tff(func_def_278, type, 'sigCod$d': ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_279, type, 'sigDom$e': 'ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' > 'ZF_ZF_Language_ZF_ZF_Language_fun$').
% 8.43/1.70 tff(func_def_280, type, 'collect$g': 'ZF_ZF_Language_ZF_ZF_Language_Language_bool_fun$' > 'ZF_ZF_Language_ZF_ZF_Language_Language_set$').
% 8.43/1.70 tff(func_def_281, type, 'type$a': 'ZF$' > 'ZF_ZF_ZF_Expression_Language$').
% 8.43/1.70 tff(func_def_282, type, 'baseFunctions$h': 'ZF_ZF_Expression_ZF_ZF_Expression_unit_Signature_ext$' > 'ZF_ZF_Expression_set$').
% 8.43/1.70 tff(func_def_283, type, 'equation$a': ('ZF_ZF_Language$' * 'ZF_ZF_Language_ZF_Expression$' * 'ZF_ZF_Language_ZF_Expression$' * 'ZF_ZF_Language$') > 'ZF_ZF_Language_ZF_Language$').
% 8.43/1.70 tff(func_def_284, type, 'uuk$': ('ZF_ZF_unit_Axioms_ext$' * 'ZF$' * 'ZF_ZF_Expression$' * 'ZF$') > 'ZF_ZF_Expression_bool_fun$').
% 8.43/1.70 tff(func_def_285, type, 'exprVar$c': 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_286, type, 'iSignature$c': 'ZF_ZF_Language_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Language_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_287, type, 'uuw$': 'ZF_ZF_unit_Axioms_ext$' > 'ZF_ZF_fun$').
% 8.43/1.70 tff(func_def_288, type, 'map_Expression$b': ('ZF_ZF_ZF_unit_TermEquivClT_ext_fun$' * 'ZF_ZF_ZF_unit_TermEquivClT_ext_fun$' * 'ZF_ZF_Expression$') > 'ZF_ZF_unit_TermEquivClT_ext_ZF_ZF_unit_TermEquivClT_ext_Expression$').
% 8.43/1.70 tff(func_def_289, type, 'sigDom$b': 'ZF_ZF_ZF_Expression_unit_Signature_ext$' > 'ZF_ZF_Expression_ZF_fun$').
% 8.43/1.70 tff(func_def_290, type, 'fun_app$u': ('Unit_unit_fun$' * 'Unit$') > 'Unit$').
% 8.43/1.70 tff(func_def_291, type, 'sigCod$i': 'ZF_ZF_fun_ZF_unit_Signature_ext$' > 'ZF_ZF_ZF_fun_fun$').
% 8.43/1.70 tff(func_def_292, type, 'sigCod$h': ('ZF_ZF_Expression_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Expression$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_293, type, 'equation$e': ('ZF_ZF_Expression$' * 'ZF_ZF_Expression_ZF_Expression$' * 'ZF_ZF_Expression_ZF_Expression$' * 'ZF_ZF_Expression$') > 'ZF_ZF_Expression_ZF_Language$').
% 8.43/1.70 tff(func_def_294, type, 'uud$': 'ZF_set$' > 'ZF_bool_fun$').
% 8.43/1.70 tff(func_def_295, type, 'signature_ext$a': ('ZF_ZF_Language_set$' * 'ZF_ZF_Language_set$' * 'ZF_ZF_Language_ZF_ZF_Language_fun$' * 'ZF_ZF_Language_ZF_ZF_Language_fun$' * 'Unit$') > 'ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_296, type, 'aAxioms$b': 'ZF_ZF_ZF_Language_unit_Axioms_ext$' > 'ZF_ZF_ZF_Language_Language_set$').
% 8.43/1.70 tff(func_def_297, type, 'size_IType$': ('ZF_nat_fun$' * 'ZF_nat_fun$' * 'ZF_ZF_IType$') > 'Nat$').
% 8.43/1.70 tff(func_def_298, type, 'sigCod_update$': 'ZF_ZF_fun_ZF_ZF_fun_fun$' > 'ZF_ZF_unit_Signature_ext_ZF_ZF_unit_Signature_ext_fun$').
% 8.43/1.70 tff(func_def_299, type, 'fun_app$z': ('ZF_ZF_Language_set_ZF_ZF_Language_set_fun$' * 'ZF_ZF_Language_set$') > 'ZF_ZF_Language_set$').
% 8.43/1.70 tff(func_def_300, type, 'iSignature_update$': ('ZF_ZF_unit_Signature_ext_ZF_ZF_unit_Signature_ext_fun$' * 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$') > 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$').
% 8.43/1.70 tff(func_def_301, type, 'sigCod$': 'ZF_ZF_unit_Signature_ext$' > 'ZF_ZF_fun$').
% 8.43/1.70 tff(func_def_302, type, 'cLCodomain$': 'ZF_ZF_unit_Axioms_ext$' > 'ZF_ZF_fun$').
% 8.43/1.70 tff(func_def_303, type, 'fun_app$a': ('ZF_ZF_fun$' * 'ZF$') > 'ZF$').
% 8.43/1.70 tff(func_def_304, type, 'iCategory$c': 'ZF_ZF_Language_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_unit_Category_ext$').
% 8.43/1.70 tff(func_def_305, type, 'uuc$': 'ZF_ZF_Language_set$' > 'ZF_ZF_Language_bool_fun$').
% 8.43/1.70 tff(func_def_306, type, 'signature_ext$e': ('ZF_set$' * 'ZF_set$' * 'ZF_ZF_fun$' * 'ZF_ZF_fun$' * 'Unit$') > 'ZF_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_307, type, 'more$d': 'ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' > 'Unit$').
% 8.43/1.70 tff(func_def_308, type, 'iFunctions$e': 'ZF_ZF_Language_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_fun$').
% 8.43/1.70 tff(func_def_309, type, 'tExprSet$': 'ZF_ZF_unit_TermEquivClT_ext$' > 'ZF_ZF_Expression_set$').
% 8.43/1.70 tff(func_def_310, type, 'top$b': 'ZF_ZF_unit_TermEquivClT_ext_ZF_ZF_unit_TermEquivClT_ext_IType_set$').
% 8.43/1.70 tff(func_def_311, type, 'iFunctions$f': 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_fun$').
% 8.43/1.70 tff(func_def_312, type, 'tCodomain$': 'ZF_ZF_unit_TermEquivClT_ext_ZF_fun$').
% 8.43/1.70 tff(func_def_313, type, 'uum$': 'ZF_ZF_unit_Axioms_ext$' > 'ZF_ZF_fun$').
% 8.43/1.70 tff(func_def_314, type, 'fun_app$': ('ZF_nat_fun$' * 'ZF$') > 'Nat$').
% 8.43/1.70 tff(func_def_319, type, sK124: ('ZF_ZF_unit_Category_ext$' * 'ZF_ZF_prod$') > 'ZF$').
% 8.43/1.70 tff(func_def_320, type, sK125: ('ZF_ZF_unit_Category_ext$' * 'ZF_ZF_prod$') > 'ZF$').
% 8.43/1.70 tff(func_def_321, type, sK126: ('ZF_ZF_unit_Axioms_ext$' * 'ZF$') > 'ZF$').
% 8.43/1.70 tff(func_def_322, type, sK127: ('ZF_ZF_unit_Axioms_ext$' * 'ZF$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_323, type, sK128: ('ZF_ZF_unit_Axioms_ext$' * 'ZF$') > 'ZF$').
% 8.43/1.70 tff(func_def_324, type, sK129: ('ZF_ZF_unit_Axioms_ext$' * 'ZF_ZF_unit_TermEquivClT_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_325, type, sK130: ('ZF_ZF_unit_Axioms_ext$' * 'ZF_ZF_unit_TermEquivClT_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_326, type, sK131: ('ZF_ZF_unit_Axioms_ext$' * 'ZF_ZF_unit_TermEquivClT_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_327, type, sK132: ('ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_328, type, sK133: ('ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_329, type, sK134: ('ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_330, type, sK135: ('ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_331, type, sK136: ('ZF_ZF_Language_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_332, type, sK137: ('ZF_ZF_Language_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_333, type, sK138: ('ZF_ZF_Language_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_334, type, sK139: ('ZF_ZF_Language_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_335, type, sK140: ('ZF_ZF_ZF_Expression_unit_Axioms_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_336, type, sK141: ('ZF_ZF_ZF_Expression_unit_Axioms_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_337, type, sK142: ('ZF_ZF_ZF_Expression_unit_Axioms_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF_ZF_ZF_Expression_Expression$').
% 8.43/1.70 tff(func_def_338, type, sK143: ('ZF_ZF_ZF_Expression_unit_Axioms_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF_ZF_ZF_Expression_Expression$').
% 8.43/1.70 tff(func_def_339, type, sK144: ('ZF_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_340, type, sK145: ('ZF_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_341, type, sK146: ('ZF_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_342, type, sK147: ('ZF_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_343, type, sK148: ('ZF_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_344, type, sK149: ('ZF_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_345, type, sK150: ('ZF_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_346, type, sK151: ('ZF_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_347, type, sK152: ('ZF_ZF_unit_Signature_ext$' * 'Nat$' * 'ZF_ZF_Expression$') > 'ZF$').
% 8.43/1.70 tff(func_def_348, type, sK153: ('ZF_ZF_unit_Signature_ext$' * 'Nat$' * 'ZF_ZF_Expression$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_349, type, sK154: ('ZF_ZF_unit_Axioms_ext$' * 'ZF$' * 'ZF$' * 'ZF$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_350, type, sK155: ('ZF_ZF_unit_Axioms_ext$' * 'ZF$' * 'ZF$' * 'ZF$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_351, type, sK156: 'ZF_ZF_unit_Axioms_ext$' > 'ZF_ZF_Language_set$').
% 8.43/1.70 tff(func_def_352, type, sK157: 'ZF_ZF_unit_Axioms_ext$' > 'ZF_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_353, type, sK158: 'ZF_ZF_unit_Axioms_ext$' > 'Unit$').
% 8.43/1.70 tff(func_def_354, type, sK159: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF$' * 'ZF_ZF_Expression$' * 'ZF$') > 'ZF_ZF_IType$').
% 8.43/1.70 tff(func_def_355, type, sK160: 'ZF_ZF_Language$' > 'ZF$').
% 8.43/1.70 tff(func_def_356, type, sK161: 'ZF_ZF_Language$' > 'ZF$').
% 8.43/1.70 tff(func_def_357, type, sK162: 'ZF_ZF_Language$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_358, type, sK163: 'ZF_ZF_Language$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_359, type, sK164: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_360, type, sK165: ('ZF_ZF_unit_Axioms_ext$' * 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_361, type, sK166: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF$' * 'ZF_ZF_Expression$' * 'ZF$') > 'ZF$').
% 8.43/1.70 tff(func_def_362, type, sK167: ('ZF_ZF_Language_bool_fun$' * 'ZF_ZF_Language_bool_fun$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_363, type, sK168: ('ZF_ZF_prod_bool_fun$' * 'ZF_ZF_prod_bool_fun$') > 'ZF_ZF_prod$').
% 8.43/1.70 tff(func_def_364, type, sK169: ('ZF_bool_fun$' * 'ZF_bool_fun$') > 'ZF$').
% 8.43/1.70 tff(func_def_365, type, sK170: ('ZF_ZF_Expression_bool_fun$' * 'ZF_ZF_Expression_bool_fun$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_366, type, sK171: ('ZF_ZF_unit_TermEquivClT_ext_bool_fun$' * 'ZF_ZF_unit_TermEquivClT_ext_bool_fun$') > 'ZF_ZF_unit_TermEquivClT_ext$').
% 8.43/1.70 tff(func_def_367, type, sK172: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF$' * 'ZF_ZF_Expression$' * 'ZF_ZF_Expression$' * 'ZF$') > 'ZF$').
% 8.43/1.70 tff(func_def_368, type, sK173: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF$' * 'ZF_ZF_Expression$' * 'ZF_ZF_Expression$' * 'ZF$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_369, type, sK174: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF$' * 'ZF_ZF_Expression$' * 'ZF_ZF_Expression$' * 'ZF$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_370, type, sK175: ('Unit$' * 'Unit_unit_fun$' * 'Unit_unit_fun$') > 'Unit$').
% 8.43/1.70 tff(func_def_371, type, sK176: ('Unit$' * 'Unit_unit_fun$' * 'Unit_unit_fun$') > 'Unit$').
% 8.43/1.70 tff(func_def_372, type, sK177: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF$' * 'ZF$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_373, type, sK178: ('ZF_ZF_unit_Axioms_ext$' * 'ZF$' * 'ZF$' * 'ZF$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_374, type, sK179: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression$') > 'Nat$').
% 8.43/1.70 tff(func_def_375, type, sK180: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_376, type, sK181: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_377, type, sK182: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_378, type, sK183: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_379, type, sK184: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_380, type, sK185: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_381, type, sK186: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_382, type, sK187: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_383, type, sK188: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_384, type, sK189: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_385, type, sK190: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_386, type, sK191: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_387, type, sK192: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_388, type, sK193: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_389, type, sK194: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_390, type, sK195: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_391, type, sK196: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_392, type, sK197: ('ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language_ZF_ZF_Language_Language$').
% 8.43/1.70 tff(func_def_393, type, sK198: ('ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_394, type, sK199: ('ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_395, type, sK200: ('ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_396, type, sK201: ('ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_397, type, sK202: ('ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_398, type, sK203: ('ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_399, type, sK204: ('ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_400, type, sK205: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_401, type, sK206: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_402, type, sK207: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_403, type, sK208: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_404, type, sK209: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_405, type, sK210: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_406, type, sK211: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_407, type, sK212: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_408, type, sK213: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_409, type, sK214: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_410, type, sK215: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_411, type, sK216: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_412, type, sK217: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_413, type, sK218: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_414, type, sK219: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_415, type, sK220: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_416, type, sK221: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_417, type, sK222: ('ZF_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF_ZF_ZF_Language_Language$').
% 8.43/1.70 tff(func_def_418, type, sK223: ('ZF_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_419, type, sK224: ('ZF_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_420, type, sK225: ('ZF_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_421, type, sK226: ('ZF_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_422, type, sK227: ('ZF_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_423, type, sK228: ('ZF_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_424, type, sK229: ('ZF_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_425, type, sK230: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_426, type, sK231: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_427, type, sK232: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_428, type, sK233: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_429, type, sK234: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_430, type, sK235: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_431, type, sK236: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_432, type, sK237: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_433, type, sK238: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_434, type, sK239: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_435, type, sK240: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_436, type, sK241: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_437, type, sK242: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_438, type, sK243: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_439, type, sK244: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_440, type, sK245: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_441, type, sK246: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_442, type, sK247: ('ZF_ZF_Language_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language_ZF_Language$').
% 8.43/1.70 tff(func_def_443, type, sK248: ('ZF_ZF_Language_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_444, type, sK249: ('ZF_ZF_Language_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_445, type, sK250: ('ZF_ZF_Language_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_446, type, sK251: ('ZF_ZF_Language_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_447, type, sK252: ('ZF_ZF_Language_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_448, type, sK253: ('ZF_ZF_Language_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_449, type, sK254: ('ZF_ZF_Language_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_450, type, sK255: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_451, type, sK256: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_452, type, sK257: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_453, type, sK258: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_454, type, sK259: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_455, type, sK260: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_456, type, sK261: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_457, type, sK262: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_458, type, sK263: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_459, type, sK264: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_460, type, sK265: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_461, type, sK266: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_462, type, sK267: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_463, type, sK268: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_464, type, sK269: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_465, type, sK270: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_466, type, sK271: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_467, type, sK272: ('ZF_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_468, type, sK273: ('ZF_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_469, type, sK274: ('ZF_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_470, type, sK275: ('ZF_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_471, type, sK276: ('ZF_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_472, type, sK277: ('ZF_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_473, type, sK278: ('ZF_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_474, type, sK279: ('ZF_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_475, type, sK280: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Language$').
% 8.43/1.70 tff(func_def_476, type, sK281: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_477, type, sK282: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_478, type, sK283: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_479, type, sK284: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_480, type, sK285: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_481, type, sK286: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_482, type, sK287: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_483, type, sK288: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_484, type, sK289: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_485, type, sK290: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_486, type, sK291: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_487, type, sK292: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_488, type, sK293: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_489, type, sK294: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_490, type, sK295: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_491, type, sK296: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_492, type, sK297: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_493, type, sK298: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_494, type, sK299: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_495, type, sK300: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_496, type, sK301: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_497, type, sK302: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_498, type, sK303: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_499, type, sK304: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_500, type, sK305: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Language$').
% 8.43/1.70 tff(func_def_501, type, sK306: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_502, type, sK307: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_503, type, sK308: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_504, type, sK309: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_505, type, sK310: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_506, type, sK311: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_507, type, sK312: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_508, type, sK313: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_509, type, sK314: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_510, type, sK315: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_511, type, sK316: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_512, type, sK317: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_513, type, sK318: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_514, type, sK319: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_515, type, sK320: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_516, type, sK321: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_517, type, sK322: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_518, type, sK323: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_519, type, sK324: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_520, type, sK325: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_521, type, sK326: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_522, type, sK327: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_523, type, sK328: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_524, type, sK329: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_525, type, sK330: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Language$').
% 8.43/1.70 tff(func_def_526, type, sK331: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_527, type, sK332: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_528, type, sK333: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_529, type, sK334: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_530, type, sK335: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_531, type, sK336: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_532, type, sK337: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_533, type, sK338: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_534, type, sK339: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_535, type, sK340: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_536, type, sK341: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_537, type, sK342: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_538, type, sK343: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_539, type, sK344: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_540, type, sK345: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_541, type, sK346: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_542, type, sK347: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_543, type, sK348: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_544, type, sK349: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_545, type, sK350: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_546, type, sK351: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_547, type, sK352: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_548, type, sK353: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_549, type, sK354: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_550, type, sK355: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_551, type, sK356: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_552, type, sK357: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_553, type, sK358: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_554, type, sK359: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_555, type, sK360: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_556, type, sK361: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_557, type, sK362: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_558, type, sK363: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_559, type, sK364: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_560, type, sK365: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_561, type, sK366: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_562, type, sK367: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_563, type, sK368: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_564, type, sK369: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_565, type, sK370: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_566, type, sK371: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_567, type, sK372: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_568, type, sK373: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_569, type, sK374: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_570, type, sK375: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_571, type, sK376: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_572, type, sK377: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_573, type, sK378: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_574, type, sK379: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_575, type, sK380: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_Expression$' * 'ZF_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_576, type, sK381: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF$' * 'ZF_ZF_Language$' * 'ZF_ZF_ZF_Language_Expression$' * 'ZF$') > 'ZF$').
% 8.43/1.70 tff(func_def_577, type, sK382: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression$' * 'ZF$' * 'ZF_ZF_Expression_ZF_Expression$' * 'ZF_ZF_Expression$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_578, type, sK383: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$' * 'ZF$' * 'ZF_ZF_Language_ZF_Expression$' * 'ZF_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_579, type, sK384: ('ZF_ZF_unit_Signature_ext$' * 'ZF$' * 'ZF$' * 'ZF_ZF_Expression$' * 'ZF$') > 'ZF$').
% 8.43/1.70 tff(func_def_580, type, sK385: 'ZF_ZF_Expression$' > 'ZF$').
% 8.43/1.70 tff(func_def_581, type, sK386: 'ZF_ZF_Expression$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_582, type, sK387: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Language$').
% 8.43/1.70 tff(func_def_583, type, sK388: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_584, type, sK389: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_585, type, sK390: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_586, type, sK391: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_587, type, sK392: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_588, type, sK393: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_589, type, sK394: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_590, type, sK395: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_591, type, sK396: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_592, type, sK397: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_593, type, sK398: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_594, type, sK399: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_595, type, sK400: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_596, type, sK401: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_597, type, sK402: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_598, type, sK403: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_599, type, sK404: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_600, type, sK405: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_601, type, sK406: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_602, type, sK407: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_603, type, sK408: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_604, type, sK409: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_605, type, sK410: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_606, type, sK411: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_607, type, sK412: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Language$').
% 8.43/1.70 tff(func_def_608, type, sK413: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_609, type, sK414: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_610, type, sK415: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_611, type, sK416: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_612, type, sK417: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_613, type, sK418: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_614, type, sK419: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_615, type, sK420: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_616, type, sK421: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_617, type, sK422: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_618, type, sK423: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_619, type, sK424: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_620, type, sK425: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_621, type, sK426: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_622, type, sK427: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_623, type, sK428: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_624, type, sK429: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_625, type, sK430: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_626, type, sK431: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_627, type, sK432: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_628, type, sK433: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_629, type, sK434: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_630, type, sK435: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_631, type, sK436: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_632, type, sK437: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Language$').
% 8.43/1.70 tff(func_def_633, type, sK438: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_634, type, sK439: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_635, type, sK440: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_636, type, sK441: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_637, type, sK442: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_638, type, sK443: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_639, type, sK444: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_640, type, sK445: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_641, type, sK446: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_642, type, sK447: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_643, type, sK448: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_644, type, sK449: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_645, type, sK450: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_646, type, sK451: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_647, type, sK452: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_648, type, sK453: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_649, type, sK454: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_650, type, sK455: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_651, type, sK456: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_652, type, sK457: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_653, type, sK458: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_654, type, sK459: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_655, type, sK460: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_656, type, sK461: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_657, type, sK462: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_658, type, sK463: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_659, type, sK464: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_660, type, sK465: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_661, type, sK466: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_662, type, sK467: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_663, type, sK468: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_664, type, sK469: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_665, type, sK470: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_666, type, sK471: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_667, type, sK472: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_668, type, sK473: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_669, type, sK474: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_670, type, sK475: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_671, type, sK476: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_672, type, sK477: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_673, type, sK478: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_674, type, sK479: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_675, type, sK480: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_676, type, sK481: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_677, type, sK482: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_678, type, sK483: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_679, type, sK484: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_680, type, sK485: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_681, type, sK486: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_682, type, sK487: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_683, type, sK488: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_684, type, sK489: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_685, type, sK490: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_686, type, sK491: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_687, type, sK492: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_688, type, sK493: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_689, type, sK494: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_690, type, sK495: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_691, type, sK496: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_692, type, sK497: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_693, type, sK498: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_694, type, sK499: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_695, type, sK500: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_696, type, sK501: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_697, type, sK502: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_698, type, sK503: ('ZF_ZF_Language_ZF_ZF_Language_Language$' * 'ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_699, type, sK504: ('ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language_ZF_ZF_Language_Language$').
% 8.43/1.70 tff(func_def_700, type, sK505: ('ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_701, type, sK506: ('ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_702, type, sK507: ('ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_703, type, sK508: ('ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_704, type, sK509: ('ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_705, type, sK510: ('ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_706, type, sK511: ('ZF_ZF_Language_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_707, type, sK512: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_708, type, sK513: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_709, type, sK514: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_710, type, sK515: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_711, type, sK516: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_712, type, sK517: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_713, type, sK518: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_714, type, sK519: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_715, type, sK520: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_716, type, sK521: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_717, type, sK522: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_718, type, sK523: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_719, type, sK524: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_720, type, sK525: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_721, type, sK526: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_722, type, sK527: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_723, type, sK528: ('ZF_ZF_ZF_Language_Language$' * 'ZF_ZF_ZF_Language_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_724, type, sK529: ('ZF_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF_ZF_ZF_Language_Language$').
% 8.43/1.70 tff(func_def_725, type, sK530: ('ZF_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_726, type, sK531: ('ZF_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_727, type, sK532: ('ZF_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_728, type, sK533: ('ZF_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_729, type, sK534: ('ZF_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_730, type, sK535: ('ZF_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_731, type, sK536: ('ZF_ZF_ZF_Language_unit_Axioms_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_732, type, sK537: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_733, type, sK538: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_734, type, sK539: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_735, type, sK540: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_736, type, sK541: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_737, type, sK542: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_738, type, sK543: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_739, type, sK544: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_740, type, sK545: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_741, type, sK546: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_742, type, sK547: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_743, type, sK548: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_744, type, sK549: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_745, type, sK550: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_746, type, sK551: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_747, type, sK552: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_748, type, sK553: ('ZF_ZF_Language_ZF_Language$' * 'ZF_ZF_Language_ZF_unit_Axioms_ext$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_749, type, sK554: ('ZF_ZF_Language_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language_ZF_Language$').
% 8.43/1.70 tff(func_def_750, type, sK555: ('ZF_ZF_Language_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_751, type, sK556: ('ZF_ZF_Language_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_752, type, sK557: ('ZF_ZF_Language_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_753, type, sK558: ('ZF_ZF_Language_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_754, type, sK559: ('ZF_ZF_Language_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_755, type, sK560: ('ZF_ZF_Language_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_756, type, sK561: ('ZF_ZF_Language_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_757, type, sK562: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_758, type, sK563: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_759, type, sK564: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_760, type, sK565: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_761, type, sK566: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_762, type, sK567: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_763, type, sK568: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_764, type, sK569: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_765, type, sK570: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_766, type, sK571: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_767, type, sK572: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_768, type, sK573: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_769, type, sK574: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_770, type, sK575: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_771, type, sK576: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_772, type, sK577: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_773, type, sK578: ('ZF_ZF_Language$' * 'ZF_ZF_unit_Axioms_ext$') > 'ZF$').
% 8.43/1.70 tff(func_def_774, type, sK579: ('ZF_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_775, type, sK580: ('ZF_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_776, type, sK581: ('ZF_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_777, type, sK582: ('ZF_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_778, type, sK583: ('ZF_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_779, type, sK584: ('ZF_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_780, type, sK585: ('ZF_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_781, type, sK586: ('ZF_ZF_unit_Axioms_ext$' * 'ZF_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_782, type, sK587: 'ZF_ZF_Language_ZF_ZF_Expression_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_783, type, sK588: 'ZF_ZF_Language_ZF_ZF_Expression_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_784, type, sK589: 'ZF_ZF_Language_ZF_ZF_Expression_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_785, type, sK590: 'ZF_ZF_Language_ZF_ZF_Expression_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_786, type, sK591: 'ZF_ZF_ZF_Expression_ZF_ZF_unit_Interpretation_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_787, type, sK592: 'ZF_ZF_ZF_Expression_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_788, type, sK593: 'ZF_ZF_ZF_Expression_ZF_ZF_unit_Interpretation_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_789, type, sK594: 'ZF_ZF_ZF_Expression_ZF_ZF_unit_Interpretation_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_790, type, sK595: 'ZF_ZF_Language_ZF_ZF_Language_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_791, type, sK596: 'ZF_ZF_Language_ZF_ZF_Language_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_792, type, sK597: 'ZF_ZF_Language_ZF_ZF_Language_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_793, type, sK598: 'ZF_ZF_Language_ZF_ZF_Language_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_794, type, sK599: 'ZF_ZF_ZF_Language_ZF_ZF_unit_Interpretation_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_795, type, sK600: 'ZF_ZF_ZF_Language_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_796, type, sK601: 'ZF_ZF_ZF_Language_ZF_ZF_unit_Interpretation_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_797, type, sK602: 'ZF_ZF_ZF_Language_ZF_ZF_unit_Interpretation_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_798, type, sK603: 'ZF_ZF_Expression_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_799, type, sK604: 'ZF_ZF_Expression_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_800, type, sK605: 'ZF_ZF_Expression_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_801, type, sK606: 'ZF_ZF_Expression_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_802, type, sK607: 'ZF_ZF_Language_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_803, type, sK608: 'ZF_ZF_Language_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_804, type, sK609: 'ZF_ZF_Language_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_805, type, sK610: 'ZF_ZF_Language_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_806, type, sK611: 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_807, type, sK612: 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_808, type, sK613: 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_809, type, sK614: 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_810, type, sK615: 'ZF_ZF_Language_ZF_ZF_Expression_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_811, type, sK616: 'ZF_ZF_Language_ZF_ZF_Expression_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_812, type, sK617: 'ZF_ZF_Language_ZF_ZF_Expression_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_813, type, sK618: 'ZF_ZF_Language_ZF_ZF_Expression_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_814, type, sK619: 'ZF_ZF_ZF_Expression_ZF_ZF_unit_Interpretation_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_815, type, sK620: 'ZF_ZF_ZF_Expression_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_816, type, sK621: 'ZF_ZF_ZF_Expression_ZF_ZF_unit_Interpretation_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_817, type, sK622: 'ZF_ZF_ZF_Expression_ZF_ZF_unit_Interpretation_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_818, type, sK623: 'ZF_ZF_Language_ZF_ZF_Language_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_819, type, sK624: 'ZF_ZF_Language_ZF_ZF_Language_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_820, type, sK625: 'ZF_ZF_Language_ZF_ZF_Language_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_821, type, sK626: 'ZF_ZF_Language_ZF_ZF_Language_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_822, type, sK627: 'ZF_ZF_ZF_Language_ZF_ZF_unit_Interpretation_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_823, type, sK628: 'ZF_ZF_ZF_Language_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_824, type, sK629: 'ZF_ZF_ZF_Language_ZF_ZF_unit_Interpretation_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_825, type, sK630: 'ZF_ZF_ZF_Language_ZF_ZF_unit_Interpretation_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_826, type, sK631: 'ZF_ZF_Expression_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_827, type, sK632: 'ZF_ZF_Expression_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_828, type, sK633: 'ZF_ZF_Expression_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_829, type, sK634: 'ZF_ZF_Expression_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_830, type, sK635: 'ZF_ZF_Language_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_831, type, sK636: 'ZF_ZF_Language_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_832, type, sK637: 'ZF_ZF_Language_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_833, type, sK638: 'ZF_ZF_Language_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_834, type, sK639: 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_835, type, sK640: 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_836, type, sK641: 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_837, type, sK642: 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_838, type, sK643: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF$' * 'ZF$' * 'ZF_ZF_Expression$' * 'ZF$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_839, type, sK644: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF$' * 'ZF$' * 'ZF_ZF_Expression$' * 'ZF$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_840, type, sK645: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_841, type, sK646: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_842, type, sK647: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_843, type, sK648: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_844, type, sK649: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language_ZF_ZF_Expression_Expression$').
% 8.43/1.70 tff(func_def_845, type, sK650: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_846, type, sK651: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_847, type, sK652: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_848, type, sK653: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_849, type, sK654: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_850, type, sK655: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language_ZF_ZF_Expression_Expression$').
% 8.43/1.70 tff(func_def_851, type, sK656: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_852, type, sK657: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language_ZF_ZF_Expression_Expression$').
% 8.43/1.70 tff(func_def_853, type, sK658: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_854, type, sK659: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_855, type, sK660: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF_ZF_ZF_Expression_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_856, type, sK661: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_857, type, sK662: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF_ZF_ZF_Expression_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_858, type, sK663: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_859, type, sK664: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF_ZF_ZF_Expression_Expression$').
% 8.43/1.70 tff(func_def_860, type, sK665: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_861, type, sK666: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_862, type, sK667: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_863, type, sK668: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF_ZF_ZF_Expression_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_864, type, sK669: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_865, type, sK670: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF_ZF_ZF_Expression_Expression$').
% 8.43/1.70 tff(func_def_866, type, sK671: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_867, type, sK672: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF_ZF_ZF_Expression_Expression$').
% 8.43/1.70 tff(func_def_868, type, sK673: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_869, type, sK674: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF_ZF_ZF_Expression_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_870, type, sK675: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_871, type, sK676: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_872, type, sK677: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_873, type, sK678: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_874, type, sK679: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_875, type, sK680: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_876, type, sK681: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_877, type, sK682: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_878, type, sK683: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_879, type, sK684: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_880, type, sK685: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_881, type, sK686: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_882, type, sK687: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_883, type, sK688: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_884, type, sK689: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_885, type, sK690: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF_ZF_ZF_Language_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_886, type, sK691: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_887, type, sK692: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF_ZF_ZF_Language_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_888, type, sK693: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_889, type, sK694: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_890, type, sK695: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_891, type, sK696: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_892, type, sK697: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_893, type, sK698: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF_ZF_ZF_Language_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_894, type, sK699: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_895, type, sK700: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_896, type, sK701: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_897, type, sK702: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_898, type, sK703: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_899, type, sK704: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF_ZF_ZF_Language_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_900, type, sK705: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_901, type, sK706: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_902, type, sK707: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_903, type, sK708: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_904, type, sK709: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression_ZF_Expression$').
% 8.43/1.70 tff(func_def_905, type, sK710: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_906, type, sK711: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_907, type, sK712: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_908, type, sK713: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_909, type, sK714: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_910, type, sK715: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression_ZF_Expression$').
% 8.43/1.70 tff(func_def_911, type, sK716: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_912, type, sK717: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression_ZF_Expression$').
% 8.43/1.70 tff(func_def_913, type, sK718: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_914, type, sK719: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_915, type, sK720: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_916, type, sK721: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_917, type, sK722: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_918, type, sK723: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_919, type, sK724: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_920, type, sK725: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_921, type, sK726: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_922, type, sK727: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_923, type, sK728: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_924, type, sK729: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_925, type, sK730: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_926, type, sK731: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_927, type, sK732: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_928, type, sK733: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_929, type, sK734: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_930, type, sK735: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_931, type, sK736: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_932, type, sK737: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_933, type, sK738: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_934, type, sK739: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_935, type, sK740: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_936, type, sK741: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_937, type, sK742: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_938, type, sK743: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_939, type, sK744: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_940, type, sK745: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_941, type, sK746: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_942, type, sK747: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_943, type, sK748: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_944, type, sK749: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_945, type, sK750: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_946, type, sK751: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_947, type, sK752: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_948, type, sK753: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_949, type, sK754: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language_ZF_ZF_Expression_Expression$').
% 8.43/1.70 tff(func_def_950, type, sK755: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_951, type, sK756: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_952, type, sK757: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_953, type, sK758: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_954, type, sK759: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_955, type, sK760: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language_ZF_ZF_Expression_Expression$').
% 8.43/1.70 tff(func_def_956, type, sK761: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_957, type, sK762: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language_ZF_ZF_Expression_Expression$').
% 8.43/1.70 tff(func_def_958, type, sK763: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_959, type, sK764: ('ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Expression_Language$') > 'ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_960, type, sK765: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF_ZF_ZF_Expression_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_961, type, sK766: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_962, type, sK767: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF_ZF_ZF_Expression_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_963, type, sK768: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_964, type, sK769: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF_ZF_ZF_Expression_Expression$').
% 8.43/1.70 tff(func_def_965, type, sK770: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_966, type, sK771: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_967, type, sK772: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_968, type, sK773: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF_ZF_ZF_Expression_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_969, type, sK774: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_970, type, sK775: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF_ZF_ZF_Expression_Expression$').
% 8.43/1.70 tff(func_def_971, type, sK776: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_972, type, sK777: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF_ZF_ZF_Expression_Expression$').
% 8.43/1.70 tff(func_def_973, type, sK778: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_974, type, sK779: ('ZF_ZF_ZF_Expression_unit_Signature_ext$' * 'ZF_ZF_ZF_Expression_Language$') > 'ZF_ZF_ZF_Expression_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_975, type, sK780: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_976, type, sK781: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_977, type, sK782: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_978, type, sK783: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_979, type, sK784: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_980, type, sK785: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_981, type, sK786: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_982, type, sK787: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_983, type, sK788: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_984, type, sK789: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_985, type, sK790: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_986, type, sK791: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_987, type, sK792: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_988, type, sK793: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_989, type, sK794: ('ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_ZF_Language_Language$') > 'ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_990, type, sK795: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF_ZF_ZF_Language_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_991, type, sK796: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_992, type, sK797: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF_ZF_ZF_Language_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_993, type, sK798: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_994, type, sK799: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_995, type, sK800: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_996, type, sK801: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_997, type, sK802: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_998, type, sK803: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF_ZF_ZF_Language_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_999, type, sK804: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_1000, type, sK805: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_1001, type, sK806: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_1002, type, sK807: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF_ZF_ZF_Language_Expression$').
% 8.43/1.70 tff(func_def_1003, type, sK808: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_1004, type, sK809: ('ZF_ZF_ZF_Language_unit_Signature_ext$' * 'ZF_ZF_ZF_Language_Language$') > 'ZF_ZF_ZF_Language_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_1005, type, sK810: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_1006, type, sK811: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1007, type, sK812: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_1008, type, sK813: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1009, type, sK814: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression_ZF_Expression$').
% 8.43/1.70 tff(func_def_1010, type, sK815: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1011, type, sK816: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_1012, type, sK817: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1013, type, sK818: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_1014, type, sK819: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1015, type, sK820: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression_ZF_Expression$').
% 8.43/1.70 tff(func_def_1016, type, sK821: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1017, type, sK822: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression_ZF_Expression$').
% 8.43/1.70 tff(func_def_1018, type, sK823: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1019, type, sK824: ('ZF_ZF_Expression_ZF_unit_Signature_ext$' * 'ZF_ZF_Expression_ZF_Language$') > 'ZF_ZF_Expression_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_1020, type, sK825: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_1021, type, sK826: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_1022, type, sK827: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_1023, type, sK828: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_1024, type, sK829: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_1025, type, sK830: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_1026, type, sK831: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_1027, type, sK832: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_1028, type, sK833: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_1029, type, sK834: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_1030, type, sK835: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_1031, type, sK836: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_1032, type, sK837: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language_ZF_Expression$').
% 8.43/1.70 tff(func_def_1033, type, sK838: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_1034, type, sK839: ('ZF_ZF_Language_ZF_unit_Signature_ext$' * 'ZF_ZF_Language_ZF_Language$') > 'ZF_ZF_Language_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_1035, type, sK840: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_1036, type, sK841: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_1037, type, sK842: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_1038, type, sK843: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_1039, type, sK844: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1040, type, sK845: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_1041, type, sK846: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_1042, type, sK847: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_1043, type, sK848: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_1044, type, sK849: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_1045, type, sK850: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1046, type, sK851: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_1047, type, sK852: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1048, type, sK853: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF$').
% 8.43/1.70 tff(func_def_1049, type, sK854: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_Language$') > 'ZF_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_1050, type, sK855: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$').
% 8.43/1.70 tff(func_def_1051, type, sK856: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1052, type, sK857: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1053, type, sK858: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$').
% 8.43/1.70 tff(func_def_1054, type, sK859: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1055, type, sK860: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1056, type, sK861: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1057, type, sK862: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1058, type, sK863: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1059, type, sK864: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1060, type, sK865: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$').
% 8.43/1.70 tff(func_def_1061, type, sK866: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1062, type, sK867: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1063, type, sK868: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1064, type, sK869: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1065, type, sK870: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1066, type, sK871: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1067, type, sK872: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$').
% 8.43/1.70 tff(func_def_1068, type, sK873: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1069, type, sK874: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$').
% 8.43/1.70 tff(func_def_1070, type, sK875: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1071, type, sK876: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1072, type, sK877: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$').
% 8.43/1.70 tff(func_def_1073, type, sK878: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1074, type, sK879: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1075, type, sK880: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1076, type, sK881: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1077, type, sK882: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1078, type, sK883: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1079, type, sK884: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$').
% 8.43/1.70 tff(func_def_1080, type, sK885: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1081, type, sK886: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1082, type, sK887: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1083, type, sK888: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1084, type, sK889: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1085, type, sK890: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1086, type, sK891: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$').
% 8.43/1.70 tff(func_def_1087, type, sK892: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF_ZF_Language$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1088, type, sK893: ('ZF_ZF_ZF_ZF_unit_Interpretation_ext$' * 'ZF$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1089, type, sK894: 'ZF_ZF_Language$' > 'ZF$').
% 8.43/1.70 tff(func_def_1090, type, sK895: 'ZF_ZF_Language$' > 'ZF$').
% 8.43/1.70 tff(func_def_1091, type, sK896: 'ZF_ZF_Language$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1092, type, sK897: 'ZF_ZF_Language$' > 'ZF$').
% 8.43/1.70 tff(func_def_1093, type, sK898: 'ZF_ZF_Language$' > 'ZF$').
% 8.43/1.70 tff(func_def_1094, type, sK899: 'ZF_ZF_Language$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1095, type, sK900: 'ZF_ZF_Language$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1096, type, sK901: 'ZF_ZF_Language$' > 'ZF$').
% 8.43/1.70 tff(func_def_1097, type, sK902: 'ZF_ZF_IType$' > 'ZF$').
% 8.43/1.70 tff(func_def_1098, type, sK903: 'ZF_ZF_IType$' > 'ZF$').
% 8.43/1.70 tff(func_def_1099, type, sK904: 'ZF_ZF_IType$' > tlbool).
% 8.43/1.70 tff(func_def_1100, type, sK905: 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_1101, type, sK906: 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_unit_Category_ext$').
% 8.43/1.70 tff(func_def_1102, type, sK907: 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_fun$').
% 8.43/1.70 tff(func_def_1103, type, sK908: 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_fun$').
% 8.43/1.70 tff(func_def_1104, type, sK909: 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$' > 'Unit$').
% 8.43/1.70 tff(func_def_1105, type, sK910: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1106, type, sK911: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1107, type, sK912: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1108, type, sK913: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1109, type, sK914: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1110, type, sK915: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1111, type, sK916: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1112, type, sK917: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1113, type, sK918: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1114, type, sK919: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1115, type, sK920: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1116, type, sK921: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1117, type, sK922: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1118, type, sK923: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1119, type, sK924: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1120, type, sK925: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1121, type, sK926: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1122, type, sK927: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1123, type, sK928: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1124, type, sK929: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1125, type, sK930: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1126, type, sK931: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1127, type, sK932: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1128, type, sK933: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1129, type, sK934: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1130, type, sK935: 'ZF_ZF_unit_Category_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1131, type, sK936: ('ZF_ZF_unit_Category_ext$' * 'ZF$') > 'ZF$').
% 8.43/1.70 tff(func_def_1132, type, sK937: ('ZF_ZF_unit_Category_ext$' * 'ZF$' * 'ZF$') > 'ZF$').
% 8.43/1.70 tff(func_def_1133, type, sK938: ('Unit$' * 'Unit_unit_fun$' * 'Unit_unit_fun$') > 'Unit$').
% 8.43/1.70 tff(func_def_1134, type, sK939: ('Unit$' * 'Unit_unit_fun$' * 'Unit_unit_fun$') > 'Unit$').
% 8.43/1.70 tff(func_def_1135, type, sK940: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_unit_Signature_ext_ZF_ZF_unit_Signature_ext_fun$' * 'ZF_ZF_unit_Signature_ext_ZF_ZF_unit_Signature_ext_fun$') > 'ZF_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_1136, type, sK941: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_unit_Signature_ext_ZF_ZF_unit_Signature_ext_fun$' * 'ZF_ZF_unit_Signature_ext_ZF_ZF_unit_Signature_ext_fun$') > 'ZF_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_1137, type, sK942: ('ZF_ZF_Language_set$' * 'ZF_ZF_Language_set_ZF_ZF_Language_set_fun$' * 'ZF_ZF_Language_set_ZF_ZF_Language_set_fun$') > 'ZF_ZF_Language_set$').
% 8.43/1.70 tff(func_def_1138, type, sK943: ('ZF_ZF_Language_set$' * 'ZF_ZF_Language_set_ZF_ZF_Language_set_fun$' * 'ZF_ZF_Language_set_ZF_ZF_Language_set_fun$') > 'ZF_ZF_Language_set$').
% 8.43/1.70 tff(func_def_1139, type, sK944: 'ZF_ZF_IType_ZF_ZF_IType_bool_fun_fun$' > tlbool).
% 8.43/1.70 tff(func_def_1140, type, sK945: 'ZF_ZF_IType_ZF_ZF_IType_bool_fun_fun$' > tlbool).
% 8.43/1.70 tff(func_def_1141, type, sK946: ('ZF_ZF_bool_fun_fun$' * 'ZF_ZF_IType_ZF_ZF_IType_bool_fun_fun$') > 'ZF$').
% 8.43/1.70 tff(func_def_1142, type, sK947: ('ZF_ZF_bool_fun_fun$' * 'ZF_ZF_IType_ZF_ZF_IType_bool_fun_fun$') > 'ZF$').
% 8.43/1.70 tff(func_def_1143, type, sK948: ('ZF_ZF_bool_fun_fun$' * 'ZF_ZF_IType_ZF_ZF_IType_bool_fun_fun$') > 'ZF$').
% 8.43/1.70 tff(func_def_1144, type, sK949: ('ZF_ZF_bool_fun_fun$' * 'ZF_ZF_IType_ZF_ZF_IType_bool_fun_fun$') > 'ZF$').
% 8.43/1.70 tff(func_def_1145, type, sK950: ('ZF_ZF_IType$' * 'ZF_ZF_IType$' * 'ZF_ZF_bool_fun_fun$') > 'ZF$').
% 8.43/1.70 tff(func_def_1146, type, sK951: ('ZF_ZF_IType$' * 'ZF_ZF_IType$' * 'ZF_ZF_bool_fun_fun$') > 'ZF$').
% 8.43/1.70 tff(func_def_1147, type, sK952: ('ZF_ZF_IType$' * 'ZF_ZF_IType$') > tlbool).
% 8.43/1.70 tff(func_def_1148, type, sK953: ('ZF_ZF_IType$' * 'ZF_ZF_IType$') > tlbool).
% 8.43/1.70 tff(func_def_1149, type, sK954: ('ZF_ZF_bool_fun_fun$' * 'ZF_ZF_IType$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1150, type, sK955: ('ZF_ZF_bool_fun_fun$' * 'ZF_ZF_IType$' * 'ZF_ZF_IType$') > 'ZF$').
% 8.43/1.70 tff(func_def_1151, type, sK956: ('ZF_ZF_fun$' * 'ZF_ZF_fun_ZF_ZF_fun_fun$' * 'ZF_ZF_fun_ZF_ZF_fun_fun$') > 'ZF_ZF_fun$').
% 8.43/1.70 tff(func_def_1152, type, sK957: ('ZF_ZF_fun$' * 'ZF_ZF_fun_ZF_ZF_fun_fun$' * 'ZF_ZF_fun_ZF_ZF_fun_fun$') > 'ZF_ZF_fun$').
% 8.43/1.70 tff(func_def_1153, type, sK958: 'ZF_ZF_bool_fun_fun$' > 'ZF$').
% 8.43/1.70 tff(func_def_1154, type, sK959: 'ZF_ZF_bool_fun_fun$' > 'ZF$').
% 8.43/1.70 tff(func_def_1155, type, sK960: 'ZF_ZF_unit_Axioms_ext$' > 'ZF_ZF_Language_set$').
% 8.43/1.70 tff(func_def_1156, type, sK961: 'ZF_ZF_unit_Axioms_ext$' > 'ZF_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_1157, type, sK962: 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_1158, type, sK963: 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_unit_Category_ext$').
% 8.43/1.70 tff(func_def_1159, type, sK964: 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_fun$').
% 8.43/1.70 tff(func_def_1160, type, sK965: 'ZF_ZF_ZF_ZF_unit_Interpretation_ext$' > 'ZF_ZF_fun$').
% 8.43/1.70 tff(func_def_1161, type, sK966: ('ZF_ZF_unit_Category_ext$' * 'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$' * 'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$') > 'ZF_ZF_unit_Category_ext$').
% 8.43/1.70 tff(func_def_1162, type, sK967: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_unit_Signature_ext_ZF_ZF_unit_Signature_ext_fun$' * 'ZF_ZF_unit_Signature_ext_ZF_ZF_unit_Signature_ext_fun$') > 'ZF_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_1163, type, sK968: ('ZF_ZF_unit_Signature_ext$' * 'ZF_ZF_unit_Signature_ext_ZF_ZF_unit_Signature_ext_fun$' * 'ZF_ZF_unit_Signature_ext_ZF_ZF_unit_Signature_ext_fun$') > 'ZF_ZF_unit_Signature_ext$').
% 8.43/1.70 tff(func_def_1164, type, sK969: ('ZF_ZF_unit_Category_ext$' * 'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$' * 'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$') > 'ZF_ZF_unit_Category_ext$').
% 8.43/1.70 tff(func_def_1165, type, sK970: 'ZF_ZF_unit_Signature_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1166, type, sK971: 'ZF_ZF_unit_Signature_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1167, type, sK972: 'ZF_ZF_ZF_Language_unit_Signature_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_1168, type, sK973: 'ZF_ZF_ZF_Language_unit_Signature_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_1169, type, sK974: 'ZF_ZF_ZF_Expression_unit_Signature_ext$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1170, type, sK975: 'ZF_ZF_ZF_Expression_unit_Signature_ext$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1171, type, sK976: 'ZF_ZF_Language_ZF_unit_Signature_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1172, type, sK977: 'ZF_ZF_Language_ZF_unit_Signature_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1173, type, sK978: 'ZF_ZF_Expression_ZF_unit_Signature_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1174, type, sK979: 'ZF_ZF_Expression_ZF_unit_Signature_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1175, type, sK980: 'ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_1176, type, sK981: 'ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_1177, type, sK982: 'ZF_ZF_Expression_ZF_ZF_Language_unit_Signature_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_1178, type, sK983: 'ZF_ZF_Expression_ZF_ZF_Language_unit_Signature_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_1179, type, sK984: 'ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1180, type, sK985: 'ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1181, type, sK986: 'ZF_ZF_Expression_ZF_ZF_Expression_unit_Signature_ext$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1182, type, sK987: 'ZF_ZF_Expression_ZF_ZF_Expression_unit_Signature_ext$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1183, type, sK988: 'ZF_ZF_fun_ZF_unit_Signature_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1184, type, sK989: 'ZF_ZF_fun_ZF_unit_Signature_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1185, type, sK990: 'ZF_ZF_unit_Signature_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1186, type, sK991: 'ZF_ZF_unit_Signature_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1187, type, sK992: 'ZF_ZF_ZF_Language_unit_Signature_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_1188, type, sK993: 'ZF_ZF_ZF_Language_unit_Signature_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_1189, type, sK994: 'ZF_ZF_ZF_Expression_unit_Signature_ext$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1190, type, sK995: 'ZF_ZF_ZF_Expression_unit_Signature_ext$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1191, type, sK996: 'ZF_ZF_Language_ZF_unit_Signature_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1192, type, sK997: 'ZF_ZF_Language_ZF_unit_Signature_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1193, type, sK998: 'ZF_ZF_Expression_ZF_unit_Signature_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1194, type, sK999: 'ZF_ZF_Expression_ZF_unit_Signature_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1195, type, sK1000: 'ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_1196, type, sK1001: 'ZF_ZF_Language_ZF_ZF_Language_unit_Signature_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_1197, type, sK1002: 'ZF_ZF_Expression_ZF_ZF_Language_unit_Signature_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_1198, type, sK1003: 'ZF_ZF_Expression_ZF_ZF_Language_unit_Signature_ext$' > 'ZF_ZF_Language$').
% 8.43/1.70 tff(func_def_1199, type, sK1004: 'ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1200, type, sK1005: 'ZF_ZF_Language_ZF_ZF_Expression_unit_Signature_ext$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1201, type, sK1006: 'ZF_ZF_Expression_ZF_ZF_Expression_unit_Signature_ext$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1202, type, sK1007: 'ZF_ZF_Expression_ZF_ZF_Expression_unit_Signature_ext$' > 'ZF_ZF_Expression$').
% 8.43/1.70 tff(func_def_1203, type, sK1008: 'ZF_ZF_fun_ZF_unit_Signature_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1204, type, sK1009: 'ZF_ZF_fun_ZF_unit_Signature_ext$' > 'ZF$').
% 8.43/1.70 tff(func_def_1205, type, sK1010: ('ZF_ZF_Expression_set$' * 'ZF_ZF_Expression_set_ZF_ZF_Expression_set_fun$' * 'ZF_ZF_Expression_set_ZF_ZF_Expression_set_fun$') > 'ZF_ZF_Expression_set$').
% 8.43/1.70 tff(func_def_1206, type, sK1011: ('ZF_ZF_Language_set$' * 'ZF_ZF_Language_set_ZF_ZF_Language_set_fun$' * 'ZF_ZF_Language_set_ZF_ZF_Language_set_fun$') > 'ZF_ZF_Language_set$').
% 8.43/1.70 tff(func_def_1207, type, sK1012: ('ZF_set$' * 'ZF_set_ZF_set_fun$' * 'ZF_set_ZF_set_fun$') > 'ZF_set$').
% 8.43/1.70 tff(func_def_1208, type, sK1013: ('ZF_ZF_Expression_set$' * 'ZF_ZF_Expression_set_ZF_ZF_Expression_set_fun$' * 'ZF_ZF_Expression_set_ZF_ZF_Expression_set_fun$') > 'ZF_ZF_Expression_set$').
% 8.43/1.70 tff(func_def_1209, type, sK1014: ('ZF_ZF_Language_set$' * 'ZF_ZF_Language_set_ZF_ZF_Language_set_fun$' * 'ZF_ZF_Language_set_ZF_ZF_Language_set_fun$') > 'ZF_ZF_Language_set$').
% 8.43/1.70 tff(func_def_1210, type, sK1015: ('ZF_set$' * 'ZF_set_ZF_set_fun$' * 'ZF_set_ZF_set_fun$') > 'ZF_set$').
% 8.43/1.70 tff(func_def_1211, type, sK1016: ('ZF_ZF_Expression_set$' * 'ZF_ZF_Expression_set_ZF_ZF_Expression_set_fun$' * 'ZF_ZF_Expression_set_ZF_ZF_Expression_set_fun$') > 'ZF_ZF_Expression_set$').
% 8.43/1.70 tff(func_def_1212, type, sK1017: ('ZF_ZF_Language_set$' * 'ZF_ZF_Language_set_ZF_ZF_Language_set_fun$' * 'ZF_ZF_Language_set_ZF_ZF_Language_set_fun$') > 'ZF_ZF_Language_set$').
% 8.43/1.70 tff(func_def_1213, type, sK1018: ('ZF_set$' * 'ZF_set_ZF_set_fun$' * 'ZF_set_ZF_set_fun$') > 'ZF_set$').
% 8.43/1.70 tff(func_def_1214, type, sK1019: ('ZF_ZF_Expression_set$' * 'ZF_ZF_Expression_set_ZF_ZF_Expression_set_fun$' * 'ZF_ZF_Expression_set_ZF_ZF_Expression_set_fun$') > 'ZF_ZF_Expression_set$').
% 8.43/1.70 tff(func_def_1215, type, sK1020: ('ZF_ZF_Language_set$' * 'ZF_ZF_Language_set_ZF_ZF_Language_set_fun$' * 'ZF_ZF_Language_set_ZF_ZF_Language_set_fun$') > 'ZF_ZF_Language_set$').
% 8.43/1.70 tff(func_def_1216, type, sK1021: ('ZF_set$' * 'ZF_set_ZF_set_fun$' * 'ZF_set_ZF_set_fun$') > 'ZF_set$').
% 8.43/1.70 tff(func_def_1217, type, sK1022: 'ZF_ZF_unit_Signature_ext$' > 'ZF_set$').
% 8.43/1.70 tff(func_def_1218, type, sK1023: 'ZF_ZF_unit_Signature_ext$' > 'ZF_set$').
% 8.43/1.70 tff(func_def_1219, type, sK1024: 'ZF_ZF_unit_Signature_ext$' > 'ZF_ZF_fun$').
% 8.43/1.70 tff(func_def_1220, type, sK1025: 'ZF_ZF_unit_Signature_ext$' > 'ZF_ZF_fun$').
% 8.43/1.70 tff(func_def_1221, type, sK1026: 'ZF_ZF_unit_Signature_ext$' > 'Unit$').
% 8.43/1.70 tff(func_def_1222, type, sK1027: 'ZF_ZF_unit_Signature_ext$' > 'ZF_set$').
% 8.43/1.70 tff(func_def_1223, type, sK1028: 'ZF_ZF_unit_Signature_ext$' > 'ZF_set$').
% 8.43/1.70 tff(func_def_1224, type, sK1029: 'ZF_ZF_unit_Signature_ext$' > 'ZF_ZF_fun$').
% 8.43/1.70 tff(func_def_1225, type, sK1030: 'ZF_ZF_unit_Signature_ext$' > 'ZF_ZF_fun$').
% 8.43/1.70 tff(func_def_1226, type, sK1031: ('ZF_ZF_fun$' * 'ZF_ZF_fun_ZF_ZF_fun_fun$' * 'ZF_ZF_fun_ZF_ZF_fun_fun$') > 'ZF_ZF_fun$').
% 8.43/1.70 tff(func_def_1227, type, sK1032: ('ZF_ZF_fun$' * 'ZF_ZF_fun_ZF_ZF_fun_fun$' * 'ZF_ZF_fun_ZF_ZF_fun_fun$') > 'ZF_ZF_fun$').
% 8.43/1.70 tff(func_def_1228, type, sK1033: ('ZF_ZF_fun$' * 'ZF_ZF_fun_ZF_ZF_fun_fun$' * 'ZF_ZF_fun_ZF_ZF_fun_fun$') > 'ZF_ZF_fun$').
% 8.43/1.70 tff(func_def_1229, type, sK1034: ('ZF_ZF_fun$' * 'ZF_ZF_fun_ZF_ZF_fun_fun$' * 'ZF_ZF_fun_ZF_ZF_fun_fun$') > 'ZF_ZF_fun$').
% 8.43/1.70 tff(func_def_1230, type, sK1035: ('ZF_set$' * 'ZF_set_ZF_set_fun$' * 'ZF_set_ZF_set_fun$') > 'ZF_set$').
% 8.43/1.70 tff(func_def_1231, type, sK1036: ('ZF_set$' * 'ZF_set_ZF_set_fun$' * 'ZF_set_ZF_set_fun$') > 'ZF_set$').
% 8.43/1.70 tff(func_def_1232, type, sK1037: ('ZF_set$' * 'ZF_set_ZF_set_fun$' * 'ZF_set_ZF_set_fun$') > 'ZF_set$').
% 8.43/1.70 tff(func_def_1233, type, sK1038: ('ZF_set$' * 'ZF_set_ZF_set_fun$' * 'ZF_set_ZF_set_fun$') > 'ZF_set$').
% 8.43/1.70 tff(func_def_1234, type, sK1039: ('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$').
% 8.43/1.70 tff(func_def_1235, type, sK1040: ('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$').
% 8.43/1.70 tff(func_def_1236, type, sK1041: ('ZF$' * 'ZF_ZF_fun$' * 'ZF_ZF_fun$') > 'ZF$').
% 8.43/1.70 tff(func_def_1237, type, sK1042: ('ZF$' * 'ZF_ZF_fun$' * 'ZF_ZF_fun$') > 'ZF$').
% 8.43/1.70 tff(func_def_1238, type, sK1043: ('ZF$' * 'ZF_ZF_fun$' * 'ZF_ZF_fun$') > 'ZF$').
% 8.43/1.70 tff(func_def_1239, type, sK1044: ('ZF$' * 'ZF_ZF_fun$' * 'ZF_ZF_fun$') > 'ZF$').
% 8.43/1.70 tff(f30,axiom,(
% 8.43/1.70 'zFAxioms$'('t$')),
% 8.43/1.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom28)).
% 8.43/1.70
% 8.43/1.70 tff(f31,axiom,(
% 8.43/1.70 ! [X0 : 'ZF_ZF_unit_Axioms_ext$'] : ('zFAxioms$'(X0) => 'interpretation$'('canonicalInterpretation$'(X0)))),
% 8.43/1.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom29)).
% 8.43/1.70
% 8.43/1.70 tff(f315,axiom,(
% 8.43/1.70 ! [X0 : 'ZF_ZF_unit_Axioms_ext$'] : 'canonicalCat$a'(X0) = 'fun_app$x'('makeCat$','canonicalCat$'(X0))),
% 8.43/1.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom313)).
% 8.43/1.70
% 8.43/1.70 tff(f379,axiom,(
% 8.43/1.70 ! [X0 : 'ZF_ZF_unit_Axioms_ext$'] : 'canonicalCat$'(X0) = 'category_ext$'('baseTypes$e'('aSignature$'(X0)),'collect$d'('uul$'(X0)),'cLDomain$'(X0),'cLCodomain$'(X0),'uum$'(X0),'canonicalComp$'(X0),'unity$')),
% 8.43/1.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom377)).
% 8.43/1.70
% 8.43/1.70 tff(f398,axiom,(
% 8.43/1.70 ! [X0 : 'ZF_ZF_unit_Axioms_ext$'] : 'canonicalInterpretation$'(X0) = 'interpretation_ext$'('aSignature$'(X0),'canonicalCat$a'(X0),'uuv$','uuw$'(X0),'unity$')),
% 8.43/1.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom396)).
% 8.43/1.70
% 8.43/1.70 tff(f530,axiom,(
% 8.43/1.70 ! [X0 : 'ZF_ZF_unit_Axioms_ext$'] : 'zF2m$'(X0) = 'inv_into$'('collect$f'('uuy$'(X0)),'m2ZF$')),
% 8.43/1.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom528)).
% 8.43/1.70
% 8.43/1.70 tff(f535,axiom,(
% 8.43/1.70 ! [X0 : 'ZF_ZF_unit_Axioms_ext$'] : 'cLDomain$'(X0) = 'comp$a'('tDomain$','zF2m$'(X0))),
% 8.43/1.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom533)).
% 8.43/1.70
% 8.43/1.70 tff(f536,axiom,(
% 8.43/1.70 ! [X0 : 'ZF_ZF_unit_Axioms_ext$'] : 'cLCodomain$'(X0) = 'comp$a'('tCodomain$','zF2m$'(X0))),
% 8.43/1.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom534)).
% 8.43/1.70
% 8.43/1.70 tff(f745,plain,(
% 8.43/1.70 ! [X0 : 'ZF_ZF_unit_Axioms_ext$'] : ('interpretation$'('canonicalInterpretation$'(X0)) | ~'zFAxioms$'(X0))),
% 8.43/1.70 inference(ennf_transformation,[],[f31])).
% 8.43/1.70
% 8.43/1.70 tff(f2241,plain,(
% 8.43/1.70 ~'interpretation$'('canonicalInterpretation$'('t$'))),
% 8.43/1.70 inference(cnf_transformation,[],[f584])).
% 8.43/1.70
% 8.43/1.70 tff(f2242,plain,(
% 8.43/1.70 'zFAxioms$'('t$')),
% 8.43/1.70 inference(cnf_transformation,[],[f30])).
% 8.43/1.70
% 8.43/1.70 tff(f2243,plain,(
% 8.43/1.70 ( ! [X0 : 'ZF_ZF_unit_Axioms_ext$'] : ('interpretation$'('canonicalInterpretation$'(X0)) | ~'zFAxioms$'(X0)) )),
% 8.43/1.70 inference(cnf_transformation,[],[f745])).
% 8.43/1.70
% 8.43/1.70 tff(f3345,plain,(
% 8.43/1.70 ( ! [X0 : 'ZF_ZF_unit_Axioms_ext$'] : ('canonicalCat$a'(X0) = 'fun_app$x'('makeCat$','canonicalCat$'(X0))) )),
% 8.43/1.70 inference(cnf_transformation,[],[f315])).
% 8.43/1.70
% 8.43/1.70 tff(f3442,plain,(
% 8.43/1.70 ( ! [X0 : 'ZF_ZF_unit_Axioms_ext$'] : ('canonicalCat$'(X0) = 'category_ext$'('baseTypes$e'('aSignature$'(X0)),'collect$d'('uul$'(X0)),'cLDomain$'(X0),'cLCodomain$'(X0),'uum$'(X0),'canonicalComp$'(X0),'unity$')) )),
% 8.43/1.70 inference(cnf_transformation,[],[f379])).
% 8.43/1.70
% 8.43/1.70 tff(f3475,plain,(
% 8.43/1.70 ( ! [X0 : 'ZF_ZF_unit_Axioms_ext$'] : ('canonicalInterpretation$'(X0) = 'interpretation_ext$'('aSignature$'(X0),'canonicalCat$a'(X0),'uuv$','uuw$'(X0),'unity$')) )),
% 8.43/1.70 inference(cnf_transformation,[],[f398])).
% 8.43/1.70
% 8.43/1.70 tff(f3827,plain,(
% 8.43/1.70 ( ! [X0 : 'ZF_ZF_unit_Axioms_ext$'] : ('zF2m$'(X0) = 'inv_into$'('collect$f'('uuy$'(X0)),'m2ZF$')) )),
% 8.43/1.70 inference(cnf_transformation,[],[f530])).
% 8.43/1.70
% 8.43/1.70 tff(f3836,plain,(
% 8.43/1.70 ( ! [X0 : 'ZF_ZF_unit_Axioms_ext$'] : ('cLDomain$'(X0) = 'comp$a'('tDomain$','zF2m$'(X0))) )),
% 8.43/1.70 inference(cnf_transformation,[],[f535])).
% 8.43/1.70
% 8.43/1.70 tff(f3837,plain,(
% 8.43/1.70 ( ! [X0 : 'ZF_ZF_unit_Axioms_ext$'] : ('cLCodomain$'(X0) = 'comp$a'('tCodomain$','zF2m$'(X0))) )),
% 8.43/1.70 inference(cnf_transformation,[],[f536])).
% 8.43/1.70
% 8.43/1.70 tff(f3873,plain,(
% 8.43/1.70 ( ! [X0 : 'ZF_ZF_unit_Axioms_ext$'] : ('cLCodomain$'(X0) = 'comp$a'('tCodomain$','inv_into$'('collect$f'('uuy$'(X0)),'m2ZF$'))) )),
% 8.43/1.70 inference(definition_unfolding,[],[f3837,f3827])).
% 8.43/1.70
% 8.43/1.70 tff(f3874,plain,(
% 8.43/1.70 ( ! [X0 : 'ZF_ZF_unit_Axioms_ext$'] : ('cLDomain$'(X0) = 'comp$a'('tDomain$','inv_into$'('collect$f'('uuy$'(X0)),'m2ZF$'))) )),
% 8.43/1.70 inference(definition_unfolding,[],[f3836,f3827])).
% 8.43/1.70
% 8.43/1.70 tff(f3875,plain,(
% 8.43/1.70 ( ! [X0 : 'ZF_ZF_unit_Axioms_ext$'] : ('canonicalCat$'(X0) = 'category_ext$'('baseTypes$e'('aSignature$'(X0)),'collect$d'('uul$'(X0)),'comp$a'('tDomain$','inv_into$'('collect$f'('uuy$'(X0)),'m2ZF$')),'comp$a'('tCodomain$','inv_into$'('collect$f'('uuy$'(X0)),'m2ZF$')),'uum$'(X0),'canonicalComp$'(X0),'unity$')) )),
% 8.43/1.70 inference(definition_unfolding,[],[f3442,f3874,f3873])).
% 8.43/1.70
% 8.43/1.70 tff(f3876,plain,(
% 8.43/1.70 ( ! [X0 : 'ZF_ZF_unit_Axioms_ext$'] : ('canonicalCat$a'(X0) = 'fun_app$x'('makeCat$','category_ext$'('baseTypes$e'('aSignature$'(X0)),'collect$d'('uul$'(X0)),'comp$a'('tDomain$','inv_into$'('collect$f'('uuy$'(X0)),'m2ZF$')),'comp$a'('tCodomain$','inv_into$'('collect$f'('uuy$'(X0)),'m2ZF$')),'uum$'(X0),'canonicalComp$'(X0),'unity$'))) )),
% 8.43/1.70 inference(definition_unfolding,[],[f3345,f3875])).
% 8.43/1.70
% 8.43/1.70 tff(f3877,plain,(
% 8.43/1.70 ( ! [X0 : 'ZF_ZF_unit_Axioms_ext$'] : ('canonicalInterpretation$'(X0) = 'interpretation_ext$'('aSignature$'(X0),'fun_app$x'('makeCat$','category_ext$'('baseTypes$e'('aSignature$'(X0)),'collect$d'('uul$'(X0)),'comp$a'('tDomain$','inv_into$'('collect$f'('uuy$'(X0)),'m2ZF$')),'comp$a'('tCodomain$','inv_into$'('collect$f'('uuy$'(X0)),'m2ZF$')),'uum$'(X0),'canonicalComp$'(X0),'unity$')),'uuv$','uuw$'(X0),'unity$')) )),
% 8.43/1.70 inference(definition_unfolding,[],[f3475,f3876])).
% 8.43/1.70
% 8.43/1.70 tff(f3882,plain,(
% 8.43/1.70 ~'interpretation$'('interpretation_ext$'('aSignature$'('t$'),'fun_app$x'('makeCat$','category_ext$'('baseTypes$e'('aSignature$'('t$')),'collect$d'('uul$'('t$')),'comp$a'('tDomain$','inv_into$'('collect$f'('uuy$'('t$')),'m2ZF$')),'comp$a'('tCodomain$','inv_into$'('collect$f'('uuy$'('t$')),'m2ZF$')),'uum$'('t$'),'canonicalComp$'('t$'),'unity$')),'uuv$','uuw$'('t$'),'unity$'))),
% 8.43/1.70 inference(definition_unfolding,[],[f2241,f3877])).
% 8.43/1.70
% 8.43/1.70 tff(f3883,plain,(
% 8.43/1.70 ( ! [X0 : 'ZF_ZF_unit_Axioms_ext$'] : ('interpretation$'('interpretation_ext$'('aSignature$'(X0),'fun_app$x'('makeCat$','category_ext$'('baseTypes$e'('aSignature$'(X0)),'collect$d'('uul$'(X0)),'comp$a'('tDomain$','inv_into$'('collect$f'('uuy$'(X0)),'m2ZF$')),'comp$a'('tCodomain$','inv_into$'('collect$f'('uuy$'(X0)),'m2ZF$')),'uum$'(X0),'canonicalComp$'(X0),'unity$')),'uuv$','uuw$'(X0),'unity$')) | ~'zFAxioms$'(X0)) )),
% 8.43/1.70 inference(definition_unfolding,[],[f2243,f3877])).
% 8.43/1.70
% 8.43/1.70 tcf(c_120,negated_conjecture,
% 8.43/1.70 (~'interpretation$'('interpretation_ext$'('aSignature$'('t$'),'fun_app$x'('makeCat$','category_ext$'('baseTypes$e'('aSignature$'('t$')),'collect$d'('uul$'('t$')),'comp$a'('tDomain$','inv_into$'('collect$f'('uuy$'('t$')),'m2ZF$')),'comp$a'('tCodomain$','inv_into$'('collect$f'('uuy$'('t$')),'m2ZF$')),'uum$'('t$'),'canonicalComp$'('t$'),'unity$')),'uuv$','uuw$'('t$'),'unity$'))),
% 8.43/1.70 inference(cnf_transformation,[],[f3882])).
% 8.43/1.70
% 8.43/1.70 tcf(c_121,negated_conjecture,
% 8.43/1.70 ('zFAxioms$'('t$')),
% 8.43/1.70 inference(cnf_transformation,[],[f2242])).
% 8.43/1.70
% 8.43/1.70 tcf(c_122,plain,![X0_'ZF_ZF_unit_Axioms_ext':'ZF_ZF_unit_Axioms_ext$']:
% 8.43/1.70 (~'zFAxioms$'(X0_'ZF_ZF_unit_Axioms_ext')|'interpretation$'('interpretation_ext$'('aSignature$'(X0_'ZF_ZF_unit_Axioms_ext'),'fun_app$x'('makeCat$','category_ext$'('baseTypes$e'('aSignature$'(X0_'ZF_ZF_unit_Axioms_ext')),'collect$d'('uul$'(X0_'ZF_ZF_unit_Axioms_ext')),'comp$a'('tDomain$','inv_into$'('collect$f'('uuy$'(X0_'ZF_ZF_unit_Axioms_ext')),'m2ZF$')),'comp$a'('tCodomain$','inv_into$'('collect$f'('uuy$'(X0_'ZF_ZF_unit_Axioms_ext')),'m2ZF$')),'uum$'(X0_'ZF_ZF_unit_Axioms_ext'),'canonicalComp$'(X0_'ZF_ZF_unit_Axioms_ext'),'unity$')),'uuv$','uuw$'(X0_'ZF_ZF_unit_Axioms_ext'),'unity$'))),
% 8.43/1.70 inference(cnf_transformation,[],[f3883])).
% 8.43/1.70
% 8.43/1.70 tcf(c_3056,plain,
% 8.43/1.70 (~'zFAxioms$'('t$')|'interpretation$'('interpretation_ext$'('aSignature$'('t$'),'fun_app$x'('makeCat$','category_ext$'('baseTypes$e'('aSignature$'('t$')),'collect$d'('uul$'('t$')),'comp$a'('tDomain$','inv_into$'('collect$f'('uuy$'('t$')),'m2ZF$')),'comp$a'('tCodomain$','inv_into$'('collect$f'('uuy$'('t$')),'m2ZF$')),'uum$'('t$'),'canonicalComp$'('t$'),'unity$')),'uuv$','uuw$'('t$'),'unity$'))),
% 8.43/1.70 inference(instantiation,[status(thm)],[c_122])).
% 8.43/1.70
% 8.43/1.70 tcf(c_3057,plain,
% 8.43/1.70 ($false),
% 8.43/1.70 inference(prop_impl_just,[status(thm)],[c_3056,c_120,c_121])).
% 8.43/1.70
% 8.43/1.70
% 8.43/1.70 % SZS output end CNFRefutation for theBenchmark.p
% 8.43/1.70
% 8.43/1.70
%------------------------------------------------------------------------------