include('Axioms/words_2.ax').
tff(tp_ty_2Etoto_2Enum__dt,type,( ty_2Etoto_2Enum__dt: del )).
tff(tp_ty_2Etoto_2Etoto,type,( ty_2Etoto_2Etoto: del > del )).
tff(tp_c_2Etoto_2EListOrd,type,(c_2Etoto_2EListOrd:del > $i)).
tff(mem_c_2Etoto_2EListOrd,axiom,( ! [A_27a:del] : mem(c_2Etoto_2EListOrd(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2EternaryComparisons_2Eordering)))))).
tff(tp_c_2Etoto_2EStrongLinearOrder__of__TO,type,(c_2Etoto_2EStrongLinearOrder__of__TO:del > $i)).
tff(mem_c_2Etoto_2EStrongLinearOrder__of__TO,axiom,( ! [A_27a:del] : mem(c_2Etoto_2EStrongLinearOrder__of__TO(A_27a),arr(arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering)),arr(A_27a,arr(A_27a,bool)))))).
tff(tp_c_2Etoto_2ETO,type,(c_2Etoto_2ETO:del > $i)).
tff(mem_c_2Etoto_2ETO,axiom,( ! [A_27a:del] : mem(c_2Etoto_2ETO(A_27a),arr(arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering)),ty_2Etoto_2Etoto(A_27a))))).
tff(tp_c_2Etoto_2ETO__inv,type,(c_2Etoto_2ETO__inv:del > $i)).
tff(mem_c_2Etoto_2ETO__inv,axiom,( ! [A_27a:del] : mem(c_2Etoto_2ETO__inv(A_27a),arr(arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering)),arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering)))))).
tff(tp_c_2Etoto_2ETO__of__LinearOrder,type,(c_2Etoto_2ETO__of__LinearOrder:del > $i)).
tff(mem_c_2Etoto_2ETO__of__LinearOrder,axiom,( ! [A_27a:del] : mem(c_2Etoto_2ETO__of__LinearOrder(A_27a),arr(arr(A_27a,arr(A_27a,bool)),arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering)))))).
tff(tp_c_2Etoto_2ETotOrd,type,(c_2Etoto_2ETotOrd:del > $i)).
tff(mem_c_2Etoto_2ETotOrd,axiom,( ! [A_27a:del] : mem(c_2Etoto_2ETotOrd(A_27a),arr(arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering)),bool)))).
tff(tp_c_2Etoto_2EWeakLinearOrder__of__TO,type,(c_2Etoto_2EWeakLinearOrder__of__TO:del > $i)).
tff(mem_c_2Etoto_2EWeakLinearOrder__of__TO,axiom,( ! [A_27a:del] : mem(c_2Etoto_2EWeakLinearOrder__of__TO(A_27a),arr(arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering)),arr(A_27a,arr(A_27a,bool)))))).
tff(tp_c_2Etoto_2Eapto,type,(c_2Etoto_2Eapto:del > $i)).
tff(mem_c_2Etoto_2Eapto,axiom,( ! [A_27a:del] : mem(c_2Etoto_2Eapto(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering)))))).
tff(stp_ty_2Etoto_2Enum__dt,type,(tp__ty_2Etoto_2Enum__dt : $tType)).
tff(stp_inj_ty_2Etoto_2Enum__dt,type,(inj__ty_2Etoto_2Enum__dt : tp__ty_2Etoto_2Enum__dt > $i)).
tff(stp_surj_ty_2Etoto_2Enum__dt,type,(surj__ty_2Etoto_2Enum__dt : $i > tp__ty_2Etoto_2Enum__dt)).
tff(stp_inj_surj_ty_2Etoto_2Enum__dt,axiom,( ! [X:tp__ty_2Etoto_2Enum__dt] : (surj__ty_2Etoto_2Enum__dt(inj__ty_2Etoto_2Enum__dt(X)) = X))).
tff(stp_inj_mem_ty_2Etoto_2Enum__dt,axiom,( ! [X:tp__ty_2Etoto_2Enum__dt] : (mem(inj__ty_2Etoto_2Enum__dt(X),ty_2Etoto_2Enum__dt)))).
tff(stp_iso_mem_ty_2Etoto_2Enum__dt,axiom,( ! [X:$i] : (mem(X,ty_2Etoto_2Enum__dt) => (X = inj__ty_2Etoto_2Enum__dt(surj__ty_2Etoto_2Enum__dt(X)))))).
tff(tp_c_2Etoto_2Ebit1,type,(c_2Etoto_2Ebit1:$i)).
tff(mem_c_2Etoto_2Ebit1,axiom,mem(c_2Etoto_2Ebit1,arr(ty_2Etoto_2Enum__dt,ty_2Etoto_2Enum__dt))).
tff(stp_fo_c_2Etoto_2Ebit1,type,(fo__c_2Etoto_2Ebit1:(tp__ty_2Etoto_2Enum__dt) > tp__ty_2Etoto_2Enum__dt)).
tff(stp_eq_fo_c_2Etoto_2Ebit1,axiom,( ! [X0:tp__ty_2Etoto_2Enum__dt] : (inj__ty_2Etoto_2Enum__dt(fo__c_2Etoto_2Ebit1(X0)) = ap(c_2Etoto_2Ebit1,inj__ty_2Etoto_2Enum__dt(X0))))).
tff(tp_c_2Etoto_2Ebit2,type,(c_2Etoto_2Ebit2:$i)).
tff(mem_c_2Etoto_2Ebit2,axiom,mem(c_2Etoto_2Ebit2,arr(ty_2Etoto_2Enum__dt,ty_2Etoto_2Enum__dt))).
tff(stp_fo_c_2Etoto_2Ebit2,type,(fo__c_2Etoto_2Ebit2:(tp__ty_2Etoto_2Enum__dt) > tp__ty_2Etoto_2Enum__dt)).
tff(stp_eq_fo_c_2Etoto_2Ebit2,axiom,( ! [X0:tp__ty_2Etoto_2Enum__dt] : (inj__ty_2Etoto_2Enum__dt(fo__c_2Etoto_2Ebit2(X0)) = ap(c_2Etoto_2Ebit2,inj__ty_2Etoto_2Enum__dt(X0))))).
tff(tp_c_2Etoto_2EcharOrd,type,(c_2Etoto_2EcharOrd:$i)).
tff(mem_c_2Etoto_2EcharOrd,axiom,mem(c_2Etoto_2EcharOrd,arr(ty_2Estring_2Echar,arr(ty_2Estring_2Echar,ty_2EternaryComparisons_2Eordering)))).
tff(stp_fo_c_2Etoto_2EcharOrd,type,(fo__c_2Etoto_2EcharOrd:(tp__ty_2Estring_2Echar * tp__ty_2Estring_2Echar) > tp__ty_2EternaryComparisons_2Eordering)).
tff(stp_eq_fo_c_2Etoto_2EcharOrd,axiom,( ! [X0:tp__ty_2Estring_2Echar] : ( ! [X1:tp__ty_2Estring_2Echar] : (inj__ty_2EternaryComparisons_2Eordering(fo__c_2Etoto_2EcharOrd(X0,X1)) = ap(ap(c_2Etoto_2EcharOrd,inj__ty_2Estring_2Echar(X0)),inj__ty_2Estring_2Echar(X1)))))).
tff(stp_c_ty_2Etoto_2Etoto_ty_2Estring_2Echar,type,(tp__c_ty_2Etoto_2Etoto_ty_2Estring_2Echar : $tType)).
tff(stp_inj_c_ty_2Etoto_2Etoto_ty_2Estring_2Echar,type,(inj__c_ty_2Etoto_2Etoto_ty_2Estring_2Echar : tp__c_ty_2Etoto_2Etoto_ty_2Estring_2Echar > $i)).
tff(stp_surj_c_ty_2Etoto_2Etoto_ty_2Estring_2Echar,type,(surj__c_ty_2Etoto_2Etoto_ty_2Estring_2Echar : $i > tp__c_ty_2Etoto_2Etoto_ty_2Estring_2Echar)).
tff(stp_inj_surj_c_ty_2Etoto_2Etoto_ty_2Estring_2Echar,axiom,( ! [X:tp__c_ty_2Etoto_2Etoto_ty_2Estring_2Echar] : (surj__c_ty_2Etoto_2Etoto_ty_2Estring_2Echar(inj__c_ty_2Etoto_2Etoto_ty_2Estring_2Echar(X)) = X))).
tff(stp_inj_mem_c_ty_2Etoto_2Etoto_ty_2Estring_2Echar,axiom,( ! [X:tp__c_ty_2Etoto_2Etoto_ty_2Estring_2Echar] : (mem(inj__c_ty_2Etoto_2Etoto_ty_2Estring_2Echar(X),ty_2Etoto_2Etoto(ty_2Estring_2Echar))))).
tff(stp_iso_mem_c_ty_2Etoto_2Etoto_ty_2Estring_2Echar,axiom,( ! [X:$i] : (mem(X,ty_2Etoto_2Etoto(ty_2Estring_2Echar)) => (X = inj__c_ty_2Etoto_2Etoto_ty_2Estring_2Echar(surj__c_ty_2Etoto_2Etoto_ty_2Estring_2Echar(X)))))).
tff(tp_c_2Etoto_2Echarto,type,(c_2Etoto_2Echarto:$i)).
tff(mem_c_2Etoto_2Echarto,axiom,mem(c_2Etoto_2Echarto,ty_2Etoto_2Etoto(ty_2Estring_2Echar))).
tff(tp_c_2Etoto_2EimageOrd,type,(c_2Etoto_2EimageOrd:(del * del) > $i)).
tff(mem_c_2Etoto_2EimageOrd,axiom,( ! [A_27a:del] : ( ! [A_27c:del] : mem(c_2Etoto_2EimageOrd(A_27a,A_27c),arr(arr(A_27a,A_27c),arr(arr(A_27c,arr(A_27c,ty_2EternaryComparisons_2Eordering)),arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering)))))))).
tff(tp_c_2Etoto_2ElexTO,type,(c_2Etoto_2ElexTO:(del * del) > $i)).
tff(mem_c_2Etoto_2ElexTO,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Etoto_2ElexTO(A_27a,A_27b),arr(arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering)),arr(arr(A_27b,arr(A_27b,ty_2EternaryComparisons_2Eordering)),arr(ty_2Epair_2Eprod(A_27a,A_27b),arr(ty_2Epair_2Eprod(A_27a,A_27b),ty_2EternaryComparisons_2Eordering)))))))).
tff(tp_c_2Etoto_2Elextoto,type,(c_2Etoto_2Elextoto:(del * del) > $i)).
tff(mem_c_2Etoto_2Elextoto,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Etoto_2Elextoto(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Etoto_2Etoto(A_27b),ty_2Etoto_2Etoto(ty_2Epair_2Eprod(A_27a,A_27b)))))))).
tff(tp_c_2Etoto_2Elistorder,type,(c_2Etoto_2Elistorder:del > $i)).
tff(mem_c_2Etoto_2Elistorder,axiom,( ! [A_27a:del] : mem(c_2Etoto_2Elistorder(A_27a),arr(arr(A_27a,arr(A_27a,bool)),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Elist_2Elist(A_27a),bool)))))).
tff(tp_c_2Etoto_2Elistoto,type,(c_2Etoto_2Elistoto:del > $i)).
tff(mem_c_2Etoto_2Elistoto,axiom,( ! [A_27a:del] : mem(c_2Etoto_2Elistoto(A_27a),arr(ty_2Etoto_2Etoto(A_27a),ty_2Etoto_2Etoto(ty_2Elist_2Elist(A_27a)))))).
tff(tp_c_2Etoto_2EnumOrd,type,(c_2Etoto_2EnumOrd:$i)).
tff(mem_c_2Etoto_2EnumOrd,axiom,mem(c_2Etoto_2EnumOrd,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2EternaryComparisons_2Eordering)))).
tff(stp_fo_c_2Etoto_2EnumOrd,type,(fo__c_2Etoto_2EnumOrd:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2EternaryComparisons_2Eordering)).
tff(stp_eq_fo_c_2Etoto_2EnumOrd,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2EternaryComparisons_2Eordering(fo__c_2Etoto_2EnumOrd(X0,X1)) = ap(ap(c_2Etoto_2EnumOrd,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Etoto_2Enum__dtOrd,type,(c_2Etoto_2Enum__dtOrd:$i)).
tff(mem_c_2Etoto_2Enum__dtOrd,axiom,mem(c_2Etoto_2Enum__dtOrd,arr(ty_2Etoto_2Enum__dt,arr(ty_2Etoto_2Enum__dt,ty_2EternaryComparisons_2Eordering)))).
tff(stp_fo_c_2Etoto_2Enum__dtOrd,type,(fo__c_2Etoto_2Enum__dtOrd:(tp__ty_2Etoto_2Enum__dt * tp__ty_2Etoto_2Enum__dt) > tp__ty_2EternaryComparisons_2Eordering)).
tff(stp_eq_fo_c_2Etoto_2Enum__dtOrd,axiom,( ! [X0:tp__ty_2Etoto_2Enum__dt] : ( ! [X1:tp__ty_2Etoto_2Enum__dt] : (inj__ty_2EternaryComparisons_2Eordering(fo__c_2Etoto_2Enum__dtOrd(X0,X1)) = ap(ap(c_2Etoto_2Enum__dtOrd,inj__ty_2Etoto_2Enum__dt(X0)),inj__ty_2Etoto_2Enum__dt(X1)))))).
tff(tp_c_2Etoto_2Enum__dt__CASE,type,(c_2Etoto_2Enum__dt__CASE:del > $i)).
tff(mem_c_2Etoto_2Enum__dt__CASE,axiom,( ! [A_27a:del] : mem(c_2Etoto_2Enum__dt__CASE(A_27a),arr(ty_2Etoto_2Enum__dt,arr(A_27a,arr(arr(ty_2Etoto_2Enum__dt,A_27a),arr(arr(ty_2Etoto_2Enum__dt,A_27a),A_27a))))))).
tff(tp_c_2Etoto_2Enum__dt__size,type,(c_2Etoto_2Enum__dt__size:$i)).
tff(mem_c_2Etoto_2Enum__dt__size,axiom,mem(c_2Etoto_2Enum__dt__size,arr(ty_2Etoto_2Enum__dt,ty_2Enum_2Enum))).
tff(stp_fo_c_2Etoto_2Enum__dt__size,type,(fo__c_2Etoto_2Enum__dt__size:(tp__ty_2Etoto_2Enum__dt) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Etoto_2Enum__dt__size,axiom,( ! [X0:tp__ty_2Etoto_2Enum__dt] : (inj__ty_2Enum_2Enum(fo__c_2Etoto_2Enum__dt__size(X0)) = ap(c_2Etoto_2Enum__dt__size,inj__ty_2Etoto_2Enum__dt(X0))))).
tff(tp_c_2Etoto_2Enum__to__dt,type,(c_2Etoto_2Enum__to__dt:$i)).
tff(mem_c_2Etoto_2Enum__to__dt,axiom,mem(c_2Etoto_2Enum__to__dt,arr(ty_2Enum_2Enum,ty_2Etoto_2Enum__dt))).
tff(stp_fo_c_2Etoto_2Enum__to__dt,type,(fo__c_2Etoto_2Enum__to__dt:(tp__ty_2Enum_2Enum) > tp__ty_2Etoto_2Enum__dt)).
tff(stp_eq_fo_c_2Etoto_2Enum__to__dt,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Etoto_2Enum__dt(fo__c_2Etoto_2Enum__to__dt(X0)) = ap(c_2Etoto_2Enum__to__dt,inj__ty_2Enum_2Enum(X0))))).
tff(stp_c_ty_2Etoto_2Etoto_ty_2Enum_2Enum,type,(tp__c_ty_2Etoto_2Etoto_ty_2Enum_2Enum : $tType)).
tff(stp_inj_c_ty_2Etoto_2Etoto_ty_2Enum_2Enum,type,(inj__c_ty_2Etoto_2Etoto_ty_2Enum_2Enum : tp__c_ty_2Etoto_2Etoto_ty_2Enum_2Enum > $i)).
tff(stp_surj_c_ty_2Etoto_2Etoto_ty_2Enum_2Enum,type,(surj__c_ty_2Etoto_2Etoto_ty_2Enum_2Enum : $i > tp__c_ty_2Etoto_2Etoto_ty_2Enum_2Enum)).
tff(stp_inj_surj_c_ty_2Etoto_2Etoto_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Etoto_2Etoto_ty_2Enum_2Enum] : (surj__c_ty_2Etoto_2Etoto_ty_2Enum_2Enum(inj__c_ty_2Etoto_2Etoto_ty_2Enum_2Enum(X)) = X))).
tff(stp_inj_mem_c_ty_2Etoto_2Etoto_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Etoto_2Etoto_ty_2Enum_2Enum] : (mem(inj__c_ty_2Etoto_2Etoto_ty_2Enum_2Enum(X),ty_2Etoto_2Etoto(ty_2Enum_2Enum))))).
tff(stp_iso_mem_c_ty_2Etoto_2Etoto_ty_2Enum_2Enum,axiom,( ! [X:$i] : (mem(X,ty_2Etoto_2Etoto(ty_2Enum_2Enum)) => (X = inj__c_ty_2Etoto_2Etoto_ty_2Enum_2Enum(surj__c_ty_2Etoto_2Etoto_ty_2Enum_2Enum(X)))))).
tff(tp_c_2Etoto_2Enumto,type,(c_2Etoto_2Enumto:$i)).
tff(mem_c_2Etoto_2Enumto,axiom,mem(c_2Etoto_2Enumto,ty_2Etoto_2Etoto(ty_2Enum_2Enum))).
tff(tp_c_2Etoto_2Eqk__numOrd,type,(c_2Etoto_2Eqk__numOrd:$i)).
tff(mem_c_2Etoto_2Eqk__numOrd,axiom,mem(c_2Etoto_2Eqk__numOrd,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2EternaryComparisons_2Eordering)))).
tff(stp_fo_c_2Etoto_2Eqk__numOrd,type,(fo__c_2Etoto_2Eqk__numOrd:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2EternaryComparisons_2Eordering)).
tff(stp_eq_fo_c_2Etoto_2Eqk__numOrd,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2EternaryComparisons_2Eordering(fo__c_2Etoto_2Eqk__numOrd(X0,X1)) = ap(ap(c_2Etoto_2Eqk__numOrd,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Etoto_2Eqk__numto,type,(c_2Etoto_2Eqk__numto:$i)).
tff(mem_c_2Etoto_2Eqk__numto,axiom,mem(c_2Etoto_2Eqk__numto,ty_2Etoto_2Etoto(ty_2Enum_2Enum))).
tff(stp_c_ty_2Etoto_2Etoto_c_ty_2Elist_2Elist_ty_2Estring_2Echar,type,(tp__c_ty_2Etoto_2Etoto_c_ty_2Elist_2Elist_ty_2Estring_2Echar : $tType)).
tff(stp_inj_c_ty_2Etoto_2Etoto_c_ty_2Elist_2Elist_ty_2Estring_2Echar,type,(inj__c_ty_2Etoto_2Etoto_c_ty_2Elist_2Elist_ty_2Estring_2Echar : tp__c_ty_2Etoto_2Etoto_c_ty_2Elist_2Elist_ty_2Estring_2Echar > $i)).
tff(stp_surj_c_ty_2Etoto_2Etoto_c_ty_2Elist_2Elist_ty_2Estring_2Echar,type,(surj__c_ty_2Etoto_2Etoto_c_ty_2Elist_2Elist_ty_2Estring_2Echar : $i > tp__c_ty_2Etoto_2Etoto_c_ty_2Elist_2Elist_ty_2Estring_2Echar)).
tff(stp_inj_surj_c_ty_2Etoto_2Etoto_c_ty_2Elist_2Elist_ty_2Estring_2Echar,axiom,( ! [X:tp__c_ty_2Etoto_2Etoto_c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__c_ty_2Etoto_2Etoto_c_ty_2Elist_2Elist_ty_2Estring_2Echar(inj__c_ty_2Etoto_2Etoto_c_ty_2Elist_2Elist_ty_2Estring_2Echar(X)) = X))).
tff(stp_inj_mem_c_ty_2Etoto_2Etoto_c_ty_2Elist_2Elist_ty_2Estring_2Echar,axiom,( ! [X:tp__c_ty_2Etoto_2Etoto_c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (mem(inj__c_ty_2Etoto_2Etoto_c_ty_2Elist_2Elist_ty_2Estring_2Echar(X),ty_2Etoto_2Etoto(ty_2Elist_2Elist(ty_2Estring_2Echar)))))).
tff(stp_iso_mem_c_ty_2Etoto_2Etoto_c_ty_2Elist_2Elist_ty_2Estring_2Echar,axiom,( ! [X:$i] : (mem(X,ty_2Etoto_2Etoto(ty_2Elist_2Elist(ty_2Estring_2Echar))) => (X = inj__c_ty_2Etoto_2Etoto_c_ty_2Elist_2Elist_ty_2Estring_2Echar(surj__c_ty_2Etoto_2Etoto_c_ty_2Elist_2Elist_ty_2Estring_2Echar(X)))))).
tff(tp_c_2Etoto_2Estringto,type,(c_2Etoto_2Estringto:$i)).
tff(mem_c_2Etoto_2Estringto,axiom,mem(c_2Etoto_2Estringto,ty_2Etoto_2Etoto(ty_2Elist_2Elist(ty_2Estring_2Echar)))).
tff(tp_c_2Etoto_2Etoto__inv,type,(c_2Etoto_2Etoto__inv:del > $i)).
tff(mem_c_2Etoto_2Etoto__inv,axiom,( ! [A_27a:del] : mem(c_2Etoto_2Etoto__inv(A_27a),arr(ty_2Etoto_2Etoto(A_27a),ty_2Etoto_2Etoto(A_27a))))).
tff(tp_c_2Etoto_2Etoto__of__LinearOrder,type,(c_2Etoto_2Etoto__of__LinearOrder:del > $i)).
tff(mem_c_2Etoto_2Etoto__of__LinearOrder,axiom,( ! [A_27a:del] : mem(c_2Etoto_2Etoto__of__LinearOrder(A_27a),arr(arr(A_27a,arr(A_27a,bool)),ty_2Etoto_2Etoto(A_27a))))).
tff(tp_c_2Etoto_2Ezer,type,(c_2Etoto_2Ezer:$i)).
tff(mem_c_2Etoto_2Ezer,axiom,mem(c_2Etoto_2Ezer,ty_2Etoto_2Enum__dt)).
tff(stp_fo_c_2Etoto_2Ezer,type,(fo__c_2Etoto_2Ezer:tp__ty_2Etoto_2Enum__dt)).
tff(stp_eq_fo_c_2Etoto_2Ezer,axiom,(inj__ty_2Etoto_2Enum__dt(fo__c_2Etoto_2Ezer) = c_2Etoto_2Ezer)).
tff(conj_thm_2Etoto_2EStrongLinearOrderExists,lemma,(( ! [A_27a:del]: (? [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27a,bool))) & p(ap(c_2Erelation_2EStrongLinearOrder(A_27a),V0R))))))).
tff(ax_thm_2Etoto_2ETotOrd,axiom,( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering))) => (p(ap(c_2Etoto_2ETotOrd(A_27a),V0c)) <=> (( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(V0c,V1x),V2y)) = fo__c_2EternaryComparisons_2EEQUAL) <=> (V1x = V2y)))))) & (( ! [V3x:$i] : (mem(V3x,A_27a) => ( ! [V4y:$i] : (mem(V4y,A_27a) => ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(V0c,V3x),V4y)) = fo__c_2EternaryComparisons_2EGREATER) <=> (surj__ty_2EternaryComparisons_2Eordering(ap(ap(V0c,V4y),V3x)) = fo__c_2EternaryComparisons_2ELESS)))))) & ( ! [V5x:$i] : (mem(V5x,A_27a) => ( ! [V6y:$i] : (mem(V6y,A_27a) => ( ! [V7z:$i] : (mem(V7z,A_27a) => (((surj__ty_2EternaryComparisons_2Eordering(ap(ap(V0c,V5x),V6y)) = fo__c_2EternaryComparisons_2ELESS) & (surj__ty_2EternaryComparisons_2Eordering(ap(ap(V0c,V6y),V7z)) = fo__c_2EternaryComparisons_2ELESS)) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(V0c,V5x),V7z)) = fo__c_2EternaryComparisons_2ELESS))))))))))))))).
tff(ax_thm_2Etoto_2ETO__of__LinearOrder,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(A_27a,arr(A_27a,bool))) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2ETO__of__LinearOrder(A_27a),V0r),V1x),V2y)) = surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Ebool_2ECOND(ty_2EternaryComparisons_2Eordering),ap(ap(c_2Emin_2E_3D(A_27a),V1x),V2y)),inj__ty_2EternaryComparisons_2Eordering(fo__c_2EternaryComparisons_2EEQUAL)),ap(ap(ap(c_2Ebool_2ECOND(ty_2EternaryComparisons_2Eordering),ap(ap(V0r,V1x),V2y)),inj__ty_2EternaryComparisons_2Eordering(fo__c_2EternaryComparisons_2ELESS)),inj__ty_2EternaryComparisons_2Eordering(fo__c_2EternaryComparisons_2EGREATER))))))))))))).
tff(conj_thm_2Etoto_2Etrichotomous__ALT,lemma,(( ! [A_27a:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27a,bool))) => (p(ap(c_2Erelation_2Etrichotomous(A_27a),V0R)) <=> ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => (((~~ p(ap(ap(V0R,V1x),V2y))) & (~~ p(ap(ap(V0R,V2y),V1x)))) => (V1x = V2y)))))))))))).
tff(conj_thm_2Etoto_2ETotOrd__TO__of__LO,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(A_27a,arr(A_27a,bool))) => (p(ap(c_2Erelation_2ELinearOrder(A_27a),V0r)) => p(ap(c_2Etoto_2ETotOrd(A_27a),ap(c_2Etoto_2ETO__of__LinearOrder(A_27a),V0r))))))))).
tff(conj_thm_2Etoto_2ESPLIT__PAIRS,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,ty_2Epair_2Eprod(A_27a,A_27b)) => ( ! [V1y:$i] : (mem(V1y,ty_2Epair_2Eprod(A_27a,A_27b)) => ((V0x = V1y) <=> ((ap(c_2Epair_2EFST(A_27a,A_27b),V0x) = ap(c_2Epair_2EFST(A_27a,A_27b),V1y)) & (ap(c_2Epair_2ESND(A_27a,A_27b),V0x) = ap(c_2Epair_2ESND(A_27a,A_27b),V1y)))))))))))).
tff(conj_thm_2Etoto_2Eall__cpn__distinct,lemma,((((~~ (fo__c_2EternaryComparisons_2ELESS = fo__c_2EternaryComparisons_2EEQUAL)) & ((~~ (fo__c_2EternaryComparisons_2ELESS = fo__c_2EternaryComparisons_2EGREATER)) & (~~ (fo__c_2EternaryComparisons_2EEQUAL = fo__c_2EternaryComparisons_2EGREATER)))) & ((~~ (fo__c_2EternaryComparisons_2EEQUAL = fo__c_2EternaryComparisons_2ELESS)) & ((~~ (fo__c_2EternaryComparisons_2EGREATER = fo__c_2EternaryComparisons_2ELESS)) & (~~ (fo__c_2EternaryComparisons_2EGREATER = fo__c_2EternaryComparisons_2EEQUAL))))))).
tff(conj_thm_2Etoto_2ETO__exists,lemma,(( ! [A_27a:del]: (? [V0x:$i] : (mem(V0x,arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering))) & p(ap(c_2Etoto_2ETotOrd(A_27a),V0x))))))).
tff(ax_thm_2Etoto_2Etoto__TY__DEF,axiom,( ! [A_27a:del]: (? [V0rep:$i] : (mem(V0rep,arr(ty_2Etoto_2Etoto(A_27a),arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering)))) & p(ap(ap(c_2Ebool_2ETYPE__DEFINITION(arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering)),ty_2Etoto_2Etoto(A_27a)),c_2Etoto_2ETotOrd(A_27a)),V0rep)))))).
tff(ax_thm_2Etoto_2Eto__bij,axiom,( ! [A_27a:del]: (( ! [V0a:$i] : (mem(V0a,ty_2Etoto_2Etoto(A_27a)) => (ap(c_2Etoto_2ETO(A_27a),ap(c_2Etoto_2Eapto(A_27a),V0a)) = V0a))) & ( ! [V1r:$i] : (mem(V1r,arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering))) => (p(ap(c_2Etoto_2ETotOrd(A_27a),V1r)) <=> (ap(c_2Etoto_2Eapto(A_27a),ap(c_2Etoto_2ETO(A_27a),V1r)) = V1r))))))).
tff(conj_thm_2Etoto_2ETO__apto__ID,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Etoto_2Etoto(A_27a)) => (ap(c_2Etoto_2ETO(A_27a),ap(c_2Etoto_2Eapto(A_27a),V0a)) = V0a)))))).
tff(conj_thm_2Etoto_2ETO__apto__TO__ID,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering))) => (p(ap(c_2Etoto_2ETotOrd(A_27a),V0r)) <=> (ap(c_2Etoto_2Eapto(A_27a),ap(c_2Etoto_2ETO(A_27a),V0r)) = V0r))))))).
tff(conj_thm_2Etoto_2ETO__11,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering))) => ( ! [V1r_27:$i] : (mem(V1r_27,arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering))) => (p(ap(c_2Etoto_2ETotOrd(A_27a),V0r)) => (p(ap(c_2Etoto_2ETotOrd(A_27a),V1r_27)) => ((ap(c_2Etoto_2ETO(A_27a),V0r) = ap(c_2Etoto_2ETO(A_27a),V1r_27)) <=> (V0r = V1r_27))))))))))).
tff(conj_thm_2Etoto_2Eonto__apto,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering))) => (p(ap(c_2Etoto_2ETotOrd(A_27a),V0r)) <=> (? [V1a:$i] : (mem(V1a,ty_2Etoto_2Etoto(A_27a)) & (V0r = ap(c_2Etoto_2Eapto(A_27a),V1a)))))))))).
tff(conj_thm_2Etoto_2ETO__onto,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Etoto_2Etoto(A_27a)) => (? [V1r:$i] : (mem(V1r,arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering))) & ((V0a = ap(c_2Etoto_2ETO(A_27a),V1r)) & p(ap(c_2Etoto_2ETotOrd(A_27a),V1r)))))))))).
tff(conj_thm_2Etoto_2ETotOrd__apto,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => p(ap(c_2Etoto_2ETotOrd(A_27a),ap(c_2Etoto_2Eapto(A_27a),V0c)))))))).
tff(conj_thm_2Etoto_2ETO__apto__TO__IMP,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering))) => (p(ap(c_2Etoto_2ETotOrd(A_27a),V0r)) => (ap(c_2Etoto_2Eapto(A_27a),ap(c_2Etoto_2ETO(A_27a),V0r)) = V0r))))))).
tff(conj_thm_2Etoto_2Etoto__thm,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => (( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V1x),V2y)) = fo__c_2EternaryComparisons_2EEQUAL) <=> (V1x = V2y)))))) & (( ! [V3x:$i] : (mem(V3x,A_27a) => ( ! [V4y:$i] : (mem(V4y,A_27a) => ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V3x),V4y)) = fo__c_2EternaryComparisons_2EGREATER) <=> (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V4y),V3x)) = fo__c_2EternaryComparisons_2ELESS)))))) & ( ! [V5x:$i] : (mem(V5x,A_27a) => ( ! [V6y:$i] : (mem(V6y,A_27a) => ( ! [V7z:$i] : (mem(V7z,A_27a) => (((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V5x),V6y)) = fo__c_2EternaryComparisons_2ELESS) & (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V6y),V7z)) = fo__c_2EternaryComparisons_2ELESS)) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V5x),V7z)) = fo__c_2EternaryComparisons_2ELESS))))))))))))))).
tff(conj_thm_2Etoto_2ETO__equal__eq,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering))) => (p(ap(c_2Etoto_2ETotOrd(A_27a),V0c)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(V0c,V1x),V2y)) = fo__c_2EternaryComparisons_2EEQUAL) <=> (V1x = V2y)))))))))))).
tff(conj_thm_2Etoto_2Etoto__equal__eq,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V1x),V2y)) = fo__c_2EternaryComparisons_2EEQUAL) <=> (V1x = V2y))))))))))).
tff(conj_thm_2Etoto_2Etoto__equal__imp__eq,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V1x),V2y)) = fo__c_2EternaryComparisons_2EEQUAL) => (V1x = V2y))))))))))).
tff(conj_thm_2Etoto_2ETO__refl,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering))) => (p(ap(c_2Etoto_2ETotOrd(A_27a),V0c)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(V0c,V1x),V1x)) = fo__c_2EternaryComparisons_2EEQUAL))))))))).
tff(conj_thm_2Etoto_2Etoto__refl,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V1x),V1x)) = fo__c_2EternaryComparisons_2EEQUAL)))))))).
tff(conj_thm_2Etoto_2Etoto__equal__sym,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V1x),V2y)) = fo__c_2EternaryComparisons_2EEQUAL) <=> (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V2y),V1x)) = fo__c_2EternaryComparisons_2EEQUAL))))))))))).
tff(conj_thm_2Etoto_2ETO__antisym,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering))) => (p(ap(c_2Etoto_2ETotOrd(A_27a),V0c)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(V0c,V1x),V2y)) = fo__c_2EternaryComparisons_2EGREATER) <=> (surj__ty_2EternaryComparisons_2Eordering(ap(ap(V0c,V2y),V1x)) = fo__c_2EternaryComparisons_2ELESS)))))))))))).
tff(conj_thm_2Etoto_2Etoto__antisym,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V1x),V2y)) = fo__c_2EternaryComparisons_2EGREATER) <=> (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V2y),V1x)) = fo__c_2EternaryComparisons_2ELESS))))))))))).
tff(conj_thm_2Etoto_2Etoto__not__less__refl,lemma,(( ! [A_27a:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1h:$i] : (mem(V1h,A_27a) => ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0cmp),V1h),V1h)) = fo__c_2EternaryComparisons_2ELESS) <=> $false)))))))).
tff(conj_thm_2Etoto_2Etoto__swap__cases,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V2y),V1x)) = surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(ap(c_2EternaryComparisons_2Eordering__CASE(ty_2EternaryComparisons_2Eordering),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V1x),V2y)),inj__ty_2EternaryComparisons_2Eordering(fo__c_2EternaryComparisons_2EGREATER)),inj__ty_2EternaryComparisons_2Eordering(fo__c_2EternaryComparisons_2EEQUAL)),inj__ty_2EternaryComparisons_2Eordering(fo__c_2EternaryComparisons_2ELESS))))))))))))).
tff(conj_thm_2Etoto_2Etoto__glneq,lemma,(( ! [A_27a:del]: (( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V1x),V2y)) = fo__c_2EternaryComparisons_2ELESS) => (~~ (V1x = V2y))))))))) & ( ! [V3c:$i] : (mem(V3c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V4x:$i] : (mem(V4x,A_27a) => ( ! [V5y:$i] : (mem(V5y,A_27a) => ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V3c),V4x),V5y)) = fo__c_2EternaryComparisons_2EGREATER) => (~~ (V4x = V5y))))))))))))).
tff(conj_thm_2Etoto_2Etoto__cpn__eqn,lemma,(( ! [A_27a:del]: (( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V1x),V2y)) = fo__c_2EternaryComparisons_2EEQUAL) => (V1x = V2y)))))))) & (( ! [V3c:$i] : (mem(V3c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V4x:$i] : (mem(V4x,A_27a) => ( ! [V5y:$i] : (mem(V5y,A_27a) => ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V3c),V4x),V5y)) = fo__c_2EternaryComparisons_2ELESS) => (~~ (V4x = V5y))))))))) & ( ! [V6c:$i] : (mem(V6c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V7x:$i] : (mem(V7x,A_27a) => ( ! [V8y:$i] : (mem(V8y,A_27a) => ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V6c),V7x),V8y)) = fo__c_2EternaryComparisons_2EGREATER) => (~~ (V7x = V8y)))))))))))))).
tff(conj_thm_2Etoto_2ETO__cpn__eqn,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering))) => (p(ap(c_2Etoto_2ETotOrd(A_27a),V0c)) => (( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(V0c,V1x),V2y)) = fo__c_2EternaryComparisons_2ELESS) => (~~ (V1x = V2y))))))) & (( ! [V3x:$i] : (mem(V3x,A_27a) => ( ! [V4y:$i] : (mem(V4y,A_27a) => ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(V0c,V3x),V4y)) = fo__c_2EternaryComparisons_2EGREATER) => (~~ (V3x = V4y))))))) & ( ! [V5x:$i] : (mem(V5x,A_27a) => ( ! [V6y:$i] : (mem(V6y,A_27a) => ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(V0c,V5x),V6y)) = fo__c_2EternaryComparisons_2EEQUAL) => (V5x = V6y)))))))))))))).
tff(conj_thm_2Etoto_2ENOT__EQ__LESS__IMP,lemma,(( ! [A_27a:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ((~~ (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0cmp),V1x),V2y)) = fo__c_2EternaryComparisons_2ELESS)) => ((V1x = V2y) | (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0cmp),V2y),V1x)) = fo__c_2EternaryComparisons_2ELESS)))))))))))).
tff(conj_thm_2Etoto_2EtotoEEtrans,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ( ! [V3z:$i] : (mem(V3z,A_27a) => ((((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V1x),V2y)) = fo__c_2EternaryComparisons_2EEQUAL) & (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V2y),V3z)) = fo__c_2EternaryComparisons_2EEQUAL)) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V1x),V3z)) = fo__c_2EternaryComparisons_2EEQUAL)) & (((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V1x),V2y)) = fo__c_2EternaryComparisons_2EEQUAL) & (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V3z),V2y)) = fo__c_2EternaryComparisons_2EEQUAL)) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V1x),V3z)) = fo__c_2EternaryComparisons_2EEQUAL)))))))))))))).
tff(conj_thm_2Etoto_2EtotoLLtrans,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ( ! [V3z:$i] : (mem(V3z,A_27a) => (((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V1x),V2y)) = fo__c_2EternaryComparisons_2ELESS) & (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V2y),V3z)) = fo__c_2EternaryComparisons_2ELESS)) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V1x),V3z)) = fo__c_2EternaryComparisons_2ELESS))))))))))))).
tff(conj_thm_2Etoto_2EtotoLGtrans,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ( ! [V3z:$i] : (mem(V3z,A_27a) => (((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V1x),V2y)) = fo__c_2EternaryComparisons_2ELESS) & (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V3z),V2y)) = fo__c_2EternaryComparisons_2EGREATER)) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V1x),V3z)) = fo__c_2EternaryComparisons_2ELESS))))))))))))).
tff(conj_thm_2Etoto_2EtotoGGtrans,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ( ! [V3z:$i] : (mem(V3z,A_27a) => (((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V2y),V1x)) = fo__c_2EternaryComparisons_2EGREATER) & (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V3z),V2y)) = fo__c_2EternaryComparisons_2EGREATER)) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V1x),V3z)) = fo__c_2EternaryComparisons_2ELESS))))))))))))).
tff(conj_thm_2Etoto_2EtotoGLtrans,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ( ! [V3z:$i] : (mem(V3z,A_27a) => (((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V2y),V1x)) = fo__c_2EternaryComparisons_2EGREATER) & (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V2y),V3z)) = fo__c_2EternaryComparisons_2ELESS)) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V1x),V3z)) = fo__c_2EternaryComparisons_2ELESS))))))))))))).
tff(conj_thm_2Etoto_2EtotoLEtrans,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ( ! [V3z:$i] : (mem(V3z,A_27a) => (((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V1x),V2y)) = fo__c_2EternaryComparisons_2ELESS) & (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V2y),V3z)) = fo__c_2EternaryComparisons_2EEQUAL)) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V1x),V3z)) = fo__c_2EternaryComparisons_2ELESS))))))))))))).
tff(conj_thm_2Etoto_2EtotoELtrans,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ( ! [V3z:$i] : (mem(V3z,A_27a) => (((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V1x),V2y)) = fo__c_2EternaryComparisons_2EEQUAL) & (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V2y),V3z)) = fo__c_2EternaryComparisons_2ELESS)) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V1x),V3z)) = fo__c_2EternaryComparisons_2ELESS))))))))))))).
tff(conj_thm_2Etoto_2Etoto__trans__less,lemma,(( ! [A_27a:del]: (( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ( ! [V3z:$i] : (mem(V3z,A_27a) => (((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V1x),V2y)) = fo__c_2EternaryComparisons_2ELESS) & (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V2y),V3z)) = fo__c_2EternaryComparisons_2ELESS)) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V1x),V3z)) = fo__c_2EternaryComparisons_2ELESS)))))))))) & (( ! [V4c:$i] : (mem(V4c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V5x:$i] : (mem(V5x,A_27a) => ( ! [V6y:$i] : (mem(V6y,A_27a) => ( ! [V7z:$i] : (mem(V7z,A_27a) => (((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4c),V5x),V6y)) = fo__c_2EternaryComparisons_2ELESS) & (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4c),V7z),V6y)) = fo__c_2EternaryComparisons_2EGREATER)) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4c),V5x),V7z)) = fo__c_2EternaryComparisons_2ELESS)))))))))) & (( ! [V8c:$i] : (mem(V8c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V9x:$i] : (mem(V9x,A_27a) => ( ! [V10y:$i] : (mem(V10y,A_27a) => ( ! [V11z:$i] : (mem(V11z,A_27a) => (((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V8c),V10y),V9x)) = fo__c_2EternaryComparisons_2EGREATER) & (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V8c),V11z),V10y)) = fo__c_2EternaryComparisons_2EGREATER)) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V8c),V9x),V11z)) = fo__c_2EternaryComparisons_2ELESS)))))))))) & (( ! [V12c:$i] : (mem(V12c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V13x:$i] : (mem(V13x,A_27a) => ( ! [V14y:$i] : (mem(V14y,A_27a) => ( ! [V15z:$i] : (mem(V15z,A_27a) => (((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V12c),V14y),V13x)) = fo__c_2EternaryComparisons_2EGREATER) & (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V12c),V14y),V15z)) = fo__c_2EternaryComparisons_2ELESS)) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V12c),V13x),V15z)) = fo__c_2EternaryComparisons_2ELESS)))))))))) & (( ! [V16c:$i] : (mem(V16c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V17x:$i] : (mem(V17x,A_27a) => ( ! [V18y:$i] : (mem(V18y,A_27a) => ( ! [V19z:$i] : (mem(V19z,A_27a) => (((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V16c),V17x),V18y)) = fo__c_2EternaryComparisons_2ELESS) & (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V16c),V18y),V19z)) = fo__c_2EternaryComparisons_2EEQUAL)) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V16c),V17x),V19z)) = fo__c_2EternaryComparisons_2ELESS)))))))))) & ( ! [V20c:$i] : (mem(V20c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V21x:$i] : (mem(V21x,A_27a) => ( ! [V22y:$i] : (mem(V22y,A_27a) => ( ! [V23z:$i] : (mem(V23z,A_27a) => (((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V20c),V21x),V22y)) = fo__c_2EternaryComparisons_2EEQUAL) & (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V20c),V22y),V23z)) = fo__c_2EternaryComparisons_2ELESS)) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V20c),V21x),V23z)) = fo__c_2EternaryComparisons_2ELESS)))))))))))))))))).
tff(ax_thm_2Etoto_2EWeakLinearOrder__of__TO,axiom,( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering))) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => (p(ap(ap(ap(c_2Etoto_2EWeakLinearOrder__of__TO(A_27a),V0c),V1x),V2y)) <=> p(ap(ap(ap(ap(c_2EternaryComparisons_2Eordering__CASE(bool),ap(ap(V0c,V1x),V2y)),inj__o(fo__c_2Ebool_2ET)),inj__o(fo__c_2Ebool_2ET)),inj__o(fo__c_2Ebool_2EF)))))))))))).
tff(ax_thm_2Etoto_2EStrongLinearOrder__of__TO,axiom,( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering))) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => (p(ap(ap(ap(c_2Etoto_2EStrongLinearOrder__of__TO(A_27a),V0c),V1x),V2y)) <=> p(ap(ap(ap(ap(c_2EternaryComparisons_2Eordering__CASE(bool),ap(ap(V0c,V1x),V2y)),inj__o(fo__c_2Ebool_2ET)),inj__o(fo__c_2Ebool_2EF)),inj__o(fo__c_2Ebool_2EF)))))))))))).
tff(ax_thm_2Etoto_2Etoto__of__LinearOrder,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(A_27a,arr(A_27a,bool))) => (ap(c_2Etoto_2Etoto__of__LinearOrder(A_27a),V0r) = ap(c_2Etoto_2ETO(A_27a),ap(c_2Etoto_2ETO__of__LinearOrder(A_27a),V0r))))))).
tff(conj_thm_2Etoto_2EWeak__Weak__of,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => p(ap(c_2Erelation_2EWeakLinearOrder(A_27a),ap(c_2Etoto_2EWeakLinearOrder__of__TO(A_27a),ap(c_2Etoto_2Eapto(A_27a),V0c))))))))).
tff(conj_thm_2Etoto_2ESTRORD__SLO,lemma,(( ! [A_27a:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27a,bool))) => (p(ap(c_2Erelation_2EWeakLinearOrder(A_27a),V0R)) => p(ap(c_2Erelation_2EStrongLinearOrder(A_27a),ap(c_2Erelation_2ESTRORD(A_27a),V0R))))))))).
tff(conj_thm_2Etoto_2EStrongof__toto__STRORD,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => (ap(c_2Etoto_2EStrongLinearOrder__of__TO(A_27a),ap(c_2Etoto_2Eapto(A_27a),V0c)) = ap(c_2Erelation_2ESTRORD(A_27a),ap(c_2Etoto_2EWeakLinearOrder__of__TO(A_27a),ap(c_2Etoto_2Eapto(A_27a),V0c))))))))).
tff(conj_thm_2Etoto_2EStrong__Strong__of,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => p(ap(c_2Erelation_2EStrongLinearOrder(A_27a),ap(c_2Etoto_2EStrongLinearOrder__of__TO(A_27a),ap(c_2Etoto_2Eapto(A_27a),V0c))))))))).
tff(conj_thm_2Etoto_2EStrong__Strong__of__TO,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering))) => (p(ap(c_2Etoto_2ETotOrd(A_27a),V0c)) => p(ap(c_2Erelation_2EStrongLinearOrder(A_27a),ap(c_2Etoto_2EStrongLinearOrder__of__TO(A_27a),V0c))))))))).
tff(conj_thm_2Etoto_2ETotOrd__TO__of__Weak,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(A_27a,arr(A_27a,bool))) => (p(ap(c_2Erelation_2EWeakLinearOrder(A_27a),V0r)) => p(ap(c_2Etoto_2ETotOrd(A_27a),ap(c_2Etoto_2ETO__of__LinearOrder(A_27a),V0r))))))))).
tff(conj_thm_2Etoto_2ETotOrd__TO__of__Strong,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(A_27a,arr(A_27a,bool))) => (p(ap(c_2Erelation_2EStrongLinearOrder(A_27a),V0r)) => p(ap(c_2Etoto_2ETotOrd(A_27a),ap(c_2Etoto_2ETO__of__LinearOrder(A_27a),V0r))))))))).
tff(conj_thm_2Etoto_2Etoto__Weak__thm,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => (ap(c_2Etoto_2Etoto__of__LinearOrder(A_27a),ap(c_2Etoto_2EWeakLinearOrder__of__TO(A_27a),ap(c_2Etoto_2Eapto(A_27a),V0c))) = V0c)))))).
tff(conj_thm_2Etoto_2Etoto__Strong__thm,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => (ap(c_2Etoto_2Etoto__of__LinearOrder(A_27a),ap(c_2Etoto_2EStrongLinearOrder__of__TO(A_27a),ap(c_2Etoto_2Eapto(A_27a),V0c))) = V0c)))))).
tff(conj_thm_2Etoto_2EWeak__toto__thm,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(A_27a,arr(A_27a,bool))) => (p(ap(c_2Erelation_2EWeakLinearOrder(A_27a),V0r)) => (ap(c_2Etoto_2EWeakLinearOrder__of__TO(A_27a),ap(c_2Etoto_2Eapto(A_27a),ap(c_2Etoto_2Etoto__of__LinearOrder(A_27a),V0r))) = V0r))))))).
tff(conj_thm_2Etoto_2EStrong__toto__thm,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(A_27a,arr(A_27a,bool))) => (p(ap(c_2Erelation_2EStrongLinearOrder(A_27a),V0r)) => (ap(c_2Etoto_2EStrongLinearOrder__of__TO(A_27a),ap(c_2Etoto_2Eapto(A_27a),ap(c_2Etoto_2Etoto__of__LinearOrder(A_27a),V0r))) = V0r))))))).
tff(ax_thm_2Etoto_2ETO__inv,axiom,( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering))) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2ETO__inv(A_27a),V0c),V1x),V2y)) = surj__ty_2EternaryComparisons_2Eordering(ap(ap(V0c,V2y),V1x))))))))))).
tff(conj_thm_2Etoto_2ETotOrd__inv,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering))) => (p(ap(c_2Etoto_2ETotOrd(A_27a),V0c)) => p(ap(c_2Etoto_2ETotOrd(A_27a),ap(c_2Etoto_2ETO__inv(A_27a),V0c))))))))).
tff(ax_thm_2Etoto_2Etoto__inv,axiom,( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => (ap(c_2Etoto_2Etoto__inv(A_27a),V0c) = ap(c_2Etoto_2ETO(A_27a),ap(c_2Etoto_2ETO__inv(A_27a),ap(c_2Etoto_2Eapto(A_27a),V0c)))))))).
tff(conj_thm_2Etoto_2Einv__TO,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering))) => (p(ap(c_2Etoto_2ETotOrd(A_27a),V0r)) => (ap(c_2Etoto_2Etoto__inv(A_27a),ap(c_2Etoto_2ETO(A_27a),V0r)) = ap(c_2Etoto_2ETO(A_27a),ap(c_2Etoto_2ETO__inv(A_27a),V0r))))))))).
tff(conj_thm_2Etoto_2Eapto__inv,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => (ap(c_2Etoto_2Eapto(A_27a),ap(c_2Etoto_2Etoto__inv(A_27a),V0c)) = ap(c_2Etoto_2ETO__inv(A_27a),ap(c_2Etoto_2Eapto(A_27a),V0c)))))))).
tff(conj_thm_2Etoto_2EWeak__toto__inv,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => (ap(c_2Etoto_2EWeakLinearOrder__of__TO(A_27a),ap(c_2Etoto_2Eapto(A_27a),ap(c_2Etoto_2Etoto__inv(A_27a),V0c))) = ap(c_2Erelation_2Einv(A_27a,A_27a),ap(c_2Etoto_2EWeakLinearOrder__of__TO(A_27a),ap(c_2Etoto_2Eapto(A_27a),V0c))))))))).
tff(conj_thm_2Etoto_2EStrong__toto__inv,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => (ap(c_2Etoto_2EStrongLinearOrder__of__TO(A_27a),ap(c_2Etoto_2Eapto(A_27a),ap(c_2Etoto_2Etoto__inv(A_27a),V0c))) = ap(c_2Erelation_2Einv(A_27a,A_27a),ap(c_2Etoto_2EStrongLinearOrder__of__TO(A_27a),ap(c_2Etoto_2Eapto(A_27a),V0c))))))))).
tff(conj_thm_2Etoto_2ETO__inv__TO__inv,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering))) => (ap(c_2Etoto_2ETO__inv(A_27a),ap(c_2Etoto_2ETO__inv(A_27a),V0c)) = V0c)))))).
tff(conj_thm_2Etoto_2Etoto__inv__toto__inv,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => (ap(c_2Etoto_2Etoto__inv(A_27a),ap(c_2Etoto_2Etoto__inv(A_27a),V0c)) = V0c)))))).
tff(conj_thm_2Etoto_2ETO__inv__Ord,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(A_27a,arr(A_27a,bool))) => (ap(c_2Etoto_2ETO__of__LinearOrder(A_27a),ap(c_2Erelation_2Einv(A_27a,A_27a),V0r)) = ap(c_2Etoto_2ETO__inv(A_27a),ap(c_2Etoto_2ETO__of__LinearOrder(A_27a),V0r)))))))).
tff(conj_thm_2Etoto_2ETO__of__less__rel,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(A_27a,arr(A_27a,bool))) => (p(ap(c_2Erelation_2EStrongLinearOrder(A_27a),V0r)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2ETO__of__LinearOrder(A_27a),V0r),V1x),V2y)) = fo__c_2EternaryComparisons_2ELESS) <=> p(ap(ap(V0r,V1x),V2y))))))))))))).
tff(conj_thm_2Etoto_2ETO__of__greater__ler,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(A_27a,arr(A_27a,bool))) => (p(ap(c_2Erelation_2EStrongLinearOrder(A_27a),V0r)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2ETO__of__LinearOrder(A_27a),V0r),V1x),V2y)) = fo__c_2EternaryComparisons_2EGREATER) <=> p(ap(ap(V0r,V2y),V1x))))))))))))).
tff(conj_thm_2Etoto_2Etoto__equal__imp,lemma,(( ! [A_27a:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1phi:$i] : (mem(V1phi,arr(A_27a,arr(A_27a,bool))) => ((p(ap(c_2Erelation_2ELinearOrder(A_27a),V1phi)) & (V0cmp = ap(c_2Etoto_2Etoto__of__LinearOrder(A_27a),V1phi))) => ( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27a) => (((V2x = V3y) <=> $true) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0cmp),V2x),V3y)) = fo__c_2EternaryComparisons_2EEQUAL)))))))))))))).
tff(conj_thm_2Etoto_2Etoto__unequal__imp,lemma,(( ! [A_27a:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1phi:$i] : (mem(V1phi,arr(A_27a,arr(A_27a,bool))) => ((p(ap(c_2Erelation_2ELinearOrder(A_27a),V1phi)) & (V0cmp = ap(c_2Etoto_2Etoto__of__LinearOrder(A_27a),V1phi))) => ( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27a) => (((V2x = V3y) <=> $false) => p(ap(ap(ap(c_2Ebool_2ECOND(bool),ap(ap(V1phi,V2x),V3y)),ap(ap(c_2Emin_2E_3D(ty_2EternaryComparisons_2Eordering),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0cmp),V2x),V3y)),inj__ty_2EternaryComparisons_2Eordering(fo__c_2EternaryComparisons_2ELESS))),ap(ap(c_2Emin_2E_3D(ty_2EternaryComparisons_2Eordering),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0cmp),V2x),V3y)),inj__ty_2EternaryComparisons_2Eordering(fo__c_2EternaryComparisons_2EGREATER))))))))))))))))).
tff(conj_thm_2Etoto_2EStrongOrder__ALT,lemma,(( ! [A_27a:del]: ( ! [V0Z:$i] : (mem(V0Z,arr(A_27a,arr(A_27a,bool))) => (p(ap(c_2Erelation_2EStrongOrder(A_27a),V0Z)) <=> (p(ap(c_2Erelation_2Eirreflexive(A_27a),V0Z)) & p(ap(c_2Erelation_2Etransitive(A_27a),V0Z))))))))).
tff(conj_thm_2Etoto_2ELEX__ALT,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27a,bool))) => ( ! [V1U:$i] : (mem(V1U,arr(A_27b,arr(A_27b,bool))) => ( ! [V2c:$i] : (mem(V2c,ty_2Epair_2Eprod(A_27a,A_27b)) => ( ! [V3d:$i] : (mem(V3d,ty_2Epair_2Eprod(A_27a,A_27b)) => (p(ap(ap(ap(ap(c_2Epair_2ELEX(A_27a,A_27b),V0R),V1U),V2c),V3d)) <=> (p(ap(ap(V0R,ap(c_2Epair_2EFST(A_27a,A_27b),V2c)),ap(c_2Epair_2EFST(A_27a,A_27b),V3d))) | ((ap(c_2Epair_2EFST(A_27a,A_27b),V2c) = ap(c_2Epair_2EFST(A_27a,A_27b),V3d)) & p(ap(ap(V1U,ap(c_2Epair_2ESND(A_27a,A_27b),V2c)),ap(c_2Epair_2ESND(A_27a,A_27b),V3d)))))))))))))))))).
tff(conj_thm_2Etoto_2ESLO__LEX,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27a,bool))) => ( ! [V1V:$i] : (mem(V1V,arr(A_27b,arr(A_27b,bool))) => ((p(ap(c_2Erelation_2EStrongLinearOrder(A_27a),V0R)) & p(ap(c_2Erelation_2EStrongLinearOrder(A_27b),V1V))) => p(ap(c_2Erelation_2EStrongLinearOrder(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2ELEX(A_27a,A_27b),V0R),V1V)))))))))))).
tff(ax_thm_2Etoto_2ElexTO,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering))) => ( ! [V1V:$i] : (mem(V1V,arr(A_27b,arr(A_27b,ty_2EternaryComparisons_2Eordering))) => (ap(ap(c_2Etoto_2ElexTO(A_27a,A_27b),V0R),V1V) = ap(c_2Etoto_2ETO__of__LinearOrder(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2ELEX(A_27a,A_27b),ap(c_2Etoto_2EStrongLinearOrder__of__TO(A_27a),V0R)),ap(c_2Etoto_2EStrongLinearOrder__of__TO(A_27b),V1V))))))))))).
tff(ax_thm_2Etoto_2Elextoto,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1v:$i] : (mem(V1v,ty_2Etoto_2Etoto(A_27b)) => (ap(ap(c_2Etoto_2Elextoto(A_27a,A_27b),V0c),V1v) = ap(c_2Etoto_2ETO(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Etoto_2ElexTO(A_27a,A_27b),ap(c_2Etoto_2Eapto(A_27a),V0c)),ap(c_2Etoto_2Eapto(A_27b),V1v))))))))))).
tff(conj_thm_2Etoto_2ElexTO__thm,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering))) => ( ! [V1V:$i] : (mem(V1V,arr(A_27b,arr(A_27b,ty_2EternaryComparisons_2Eordering))) => ((p(ap(c_2Etoto_2ETotOrd(A_27a),V0R)) & p(ap(c_2Etoto_2ETotOrd(A_27b),V1V))) => ( ! [V2x:$i] : (mem(V2x,ty_2Epair_2Eprod(A_27a,A_27b)) => ( ! [V3y:$i] : (mem(V3y,ty_2Epair_2Eprod(A_27a,A_27b)) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(ap(c_2Etoto_2ElexTO(A_27a,A_27b),V0R),V1V),V2x),V3y)) = surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(ap(c_2EternaryComparisons_2Eordering__CASE(ty_2EternaryComparisons_2Eordering),ap(ap(V0R,ap(c_2Epair_2EFST(A_27a,A_27b),V2x)),ap(c_2Epair_2EFST(A_27a,A_27b),V3y))),inj__ty_2EternaryComparisons_2Eordering(fo__c_2EternaryComparisons_2ELESS)),ap(ap(V1V,ap(c_2Epair_2ESND(A_27a,A_27b),V2x)),ap(c_2Epair_2ESND(A_27a,A_27b),V3y))),inj__ty_2EternaryComparisons_2Eordering(fo__c_2EternaryComparisons_2EGREATER))))))))))))))))).
tff(conj_thm_2Etoto_2ElexTO__ALT,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering))) => ( ! [V1V:$i] : (mem(V1V,arr(A_27b,arr(A_27b,ty_2EternaryComparisons_2Eordering))) => ((p(ap(c_2Etoto_2ETotOrd(A_27a),V0R)) & p(ap(c_2Etoto_2ETotOrd(A_27b),V1V))) => p(ap(c_2Ebool_2E_21(ty_2Epair_2Eprod(A_27a,A_27b)),ap(c_2Epair_2EUNCURRY(A_27a,A_27b,bool),f2262(A_27b,A_27a,V1V,V0R))))))))))))).
tff(conj_thm_2Etoto_2ETO__lexTO,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27a,ty_2EternaryComparisons_2Eordering))) => ( ! [V1V:$i] : (mem(V1V,arr(A_27b,arr(A_27b,ty_2EternaryComparisons_2Eordering))) => ((p(ap(c_2Etoto_2ETotOrd(A_27a),V0R)) & p(ap(c_2Etoto_2ETotOrd(A_27b),V1V))) => p(ap(c_2Etoto_2ETotOrd(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Etoto_2ElexTO(A_27a,A_27b),V0R),V1V)))))))))))).
tff(conj_thm_2Etoto_2Epre__aplextoto,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1v:$i] : (mem(V1v,ty_2Etoto_2Etoto(A_27b)) => ( ! [V2x:$i] : (mem(V2x,ty_2Epair_2Eprod(A_27a,A_27b)) => ( ! [V3y:$i] : (mem(V3y,ty_2Epair_2Eprod(A_27a,A_27b)) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Etoto_2Elextoto(A_27a,A_27b),V0c),V1v)),V2x),V3y)) = surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(ap(c_2EternaryComparisons_2Eordering__CASE(ty_2EternaryComparisons_2Eordering),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),ap(c_2Epair_2EFST(A_27a,A_27b),V2x)),ap(c_2Epair_2EFST(A_27a,A_27b),V3y))),inj__ty_2EternaryComparisons_2Eordering(fo__c_2EternaryComparisons_2ELESS)),ap(ap(ap(c_2Etoto_2Eapto(A_27b),V1v),ap(c_2Epair_2ESND(A_27a,A_27b),V2x)),ap(c_2Epair_2ESND(A_27a,A_27b),V3y))),inj__ty_2EternaryComparisons_2Eordering(fo__c_2EternaryComparisons_2EGREATER)))))))))))))))).
tff(conj_thm_2Etoto_2Eaplextoto,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1v:$i] : (mem(V1v,ty_2Etoto_2Etoto(A_27b)) => ( ! [V2x1:$i] : (mem(V2x1,A_27a) => ( ! [V3x2:$i] : (mem(V3x2,A_27b) => ( ! [V4y1:$i] : (mem(V4y1,A_27a) => ( ! [V5y2:$i] : (mem(V5y2,A_27b) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Etoto_2Elextoto(A_27a,A_27b),V0c),V1v)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2x1),V3x2)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V4y1),V5y2))) = surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(ap(c_2EternaryComparisons_2Eordering__CASE(ty_2EternaryComparisons_2Eordering),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0c),V2x1),V4y1)),inj__ty_2EternaryComparisons_2Eordering(fo__c_2EternaryComparisons_2ELESS)),ap(ap(ap(c_2Etoto_2Eapto(A_27b),V1v),V3x2),V5y2)),inj__ty_2EternaryComparisons_2Eordering(fo__c_2EternaryComparisons_2EGREATER)))))))))))))))))))).
tff(conj_thm_2Etoto_2EStrongLinearOrder__LESS,lemma,(p(ap(c_2Erelation_2EStrongLinearOrder(ty_2Enum_2Enum),c_2Eprim__rec_2E_3C)))).
tff(ax_thm_2Etoto_2EnumOrd,axiom,(c_2Etoto_2EnumOrd = ap(c_2Etoto_2ETO__of__LinearOrder(ty_2Enum_2Enum),c_2Eprim__rec_2E_3C))).
tff(conj_thm_2Etoto_2ETO__numOrd,lemma,(p(ap(c_2Etoto_2ETotOrd(ty_2Enum_2Enum),c_2Etoto_2EnumOrd)))).
tff(ax_thm_2Etoto_2Enumto,axiom,(surj__c_ty_2Etoto_2Etoto_ty_2Enum_2Enum(c_2Etoto_2Enumto) = surj__c_ty_2Etoto_2Etoto_ty_2Enum_2Enum(ap(c_2Etoto_2ETO(ty_2Enum_2Enum),c_2Etoto_2EnumOrd)))).
tff(conj_thm_2Etoto_2Eapnumto__thm,lemma,((ap(c_2Etoto_2Eapto(ty_2Enum_2Enum),c_2Etoto_2Enumto) = c_2Etoto_2EnumOrd))).
tff(conj_thm_2Etoto_2EnumeralOrd,lemma,(( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1y:tp__ty_2Enum_2Enum] : ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2EnumOrd,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))) = fo__c_2EternaryComparisons_2EEQUAL) & ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2EnumOrd,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1y)))) = fo__c_2EternaryComparisons_2ELESS) & ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2EnumOrd,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1y)))) = fo__c_2EternaryComparisons_2ELESS) & ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2EnumOrd,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0x))),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))) = fo__c_2EternaryComparisons_2EGREATER) & ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2EnumOrd,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0x))),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))) = fo__c_2EternaryComparisons_2EGREATER) & ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2EnumOrd,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0x))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1y)))) = surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2EnumOrd,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1y)))) & ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2EnumOrd,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0x))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1y)))) = surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2EnumOrd,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1y)))) & ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2EnumOrd,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0x))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1y)))) = surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(ap(c_2EternaryComparisons_2Eordering__CASE(ty_2EternaryComparisons_2Eordering),ap(ap(c_2Etoto_2EnumOrd,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1y))),inj__ty_2EternaryComparisons_2Eordering(fo__c_2EternaryComparisons_2ELESS)),inj__ty_2EternaryComparisons_2Eordering(fo__c_2EternaryComparisons_2ELESS)),inj__ty_2EternaryComparisons_2Eordering(fo__c_2EternaryComparisons_2EGREATER)))) & (surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2EnumOrd,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0x))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1y)))) = surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(ap(c_2EternaryComparisons_2Eordering__CASE(ty_2EternaryComparisons_2Eordering),ap(ap(c_2Etoto_2EnumOrd,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1y))),inj__ty_2EternaryComparisons_2Eordering(fo__c_2EternaryComparisons_2ELESS)),inj__ty_2EternaryComparisons_2Eordering(fo__c_2EternaryComparisons_2EGREATER)),inj__ty_2EternaryComparisons_2Eordering(fo__c_2EternaryComparisons_2EGREATER)))))))))))))))).
tff(ax_thm_2Etoto_2Enum__dt__TY__DEF,axiom,(? [V0rep:$i] : (mem(V0rep,arr(ty_2Etoto_2Enum__dt,ty_2Eind__type_2Erecspace(bool))) & p(ap(ap(c_2Ebool_2ETYPE__DEFINITION(ty_2Eind__type_2Erecspace(bool),ty_2Etoto_2Enum__dt),f2269),V0rep))))).
tff(ax_thm_2Etoto_2Enum__dt__case__def,axiom,( ! [A_27a:del]: (( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1f:$i] : (mem(V1f,arr(ty_2Etoto_2Enum__dt,A_27a)) => ( ! [V2f1:$i] : (mem(V2f1,arr(ty_2Etoto_2Enum__dt,A_27a)) => (ap(ap(ap(ap(c_2Etoto_2Enum__dt__CASE(A_27a),inj__ty_2Etoto_2Enum__dt(fo__c_2Etoto_2Ezer)),V0v),V1f),V2f1) = V0v))))))) & (( ! [V3a:tp__ty_2Etoto_2Enum__dt] : ( ! [V4v:$i] : (mem(V4v,A_27a) => ( ! [V5f:$i] : (mem(V5f,arr(ty_2Etoto_2Enum__dt,A_27a)) => ( ! [V6f1:$i] : (mem(V6f1,arr(ty_2Etoto_2Enum__dt,A_27a)) => (ap(ap(ap(ap(c_2Etoto_2Enum__dt__CASE(A_27a),ap(c_2Etoto_2Ebit1,inj__ty_2Etoto_2Enum__dt(V3a))),V4v),V5f),V6f1) = ap(V5f,inj__ty_2Etoto_2Enum__dt(V3a)))))))))) & ( ! [V7a:tp__ty_2Etoto_2Enum__dt] : ( ! [V8v:$i] : (mem(V8v,A_27a) => ( ! [V9f:$i] : (mem(V9f,arr(ty_2Etoto_2Enum__dt,A_27a)) => ( ! [V10f1:$i] : (mem(V10f1,arr(ty_2Etoto_2Enum__dt,A_27a)) => (ap(ap(ap(ap(c_2Etoto_2Enum__dt__CASE(A_27a),ap(c_2Etoto_2Ebit2,inj__ty_2Etoto_2Enum__dt(V7a))),V8v),V9f),V10f1) = ap(V10f1,inj__ty_2Etoto_2Enum__dt(V7a)))))))))))))).
tff(ax_thm_2Etoto_2Enum__dt__size__def,axiom,((surj__ty_2Enum_2Enum(ap(c_2Etoto_2Enum__dt__size,inj__ty_2Etoto_2Enum__dt(fo__c_2Etoto_2Ezer))) = fo__c_2Enum_2E0) & (( ! [V0a:tp__ty_2Etoto_2Enum__dt] : (surj__ty_2Enum_2Enum(ap(c_2Etoto_2Enum__dt__size,ap(c_2Etoto_2Ebit1,inj__ty_2Etoto_2Enum__dt(V0a)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Etoto_2Enum__dt__size,inj__ty_2Etoto_2Enum__dt(V0a)))))) & ( ! [V1a:tp__ty_2Etoto_2Enum__dt] : (surj__ty_2Enum_2Enum(ap(c_2Etoto_2Enum__dt__size,ap(c_2Etoto_2Ebit2,inj__ty_2Etoto_2Enum__dt(V1a)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Etoto_2Enum__dt__size,inj__ty_2Etoto_2Enum__dt(V1a))))))))).
tff(conj_thm_2Etoto_2Edatatype__num__dt,lemma,(( ! [V0num__dt:$i] : (mem(V0num__dt,arr(ty_2Etoto_2Enum__dt,arr(arr(ty_2Etoto_2Enum__dt,ty_2Etoto_2Enum__dt),arr(arr(ty_2Etoto_2Enum__dt,ty_2Etoto_2Enum__dt),bool)))) => p(ap(c_2Ebool_2EDATATYPE(bool),ap(ap(ap(V0num__dt,inj__ty_2Etoto_2Enum__dt(fo__c_2Etoto_2Ezer)),c_2Etoto_2Ebit1),c_2Etoto_2Ebit2))))))).
tff(conj_thm_2Etoto_2Enum__dt__11,lemma,((( ! [V0a:tp__ty_2Etoto_2Enum__dt] : ( ! [V1a_27:tp__ty_2Etoto_2Enum__dt] : ((surj__ty_2Etoto_2Enum__dt(ap(c_2Etoto_2Ebit1,inj__ty_2Etoto_2Enum__dt(V0a))) = surj__ty_2Etoto_2Enum__dt(ap(c_2Etoto_2Ebit1,inj__ty_2Etoto_2Enum__dt(V1a_27)))) <=> (V0a = V1a_27)))) & ( ! [V2a:tp__ty_2Etoto_2Enum__dt] : ( ! [V3a_27:tp__ty_2Etoto_2Enum__dt] : ((surj__ty_2Etoto_2Enum__dt(ap(c_2Etoto_2Ebit2,inj__ty_2Etoto_2Enum__dt(V2a))) = surj__ty_2Etoto_2Enum__dt(ap(c_2Etoto_2Ebit2,inj__ty_2Etoto_2Enum__dt(V3a_27)))) <=> (V2a = V3a_27))))))).
tff(conj_thm_2Etoto_2Enum__dt__distinct,lemma,((( ! [V0a:tp__ty_2Etoto_2Enum__dt] : (~~ (fo__c_2Etoto_2Ezer = surj__ty_2Etoto_2Enum__dt(ap(c_2Etoto_2Ebit1,inj__ty_2Etoto_2Enum__dt(V0a)))))) & (( ! [V1a:tp__ty_2Etoto_2Enum__dt] : (~~ (fo__c_2Etoto_2Ezer = surj__ty_2Etoto_2Enum__dt(ap(c_2Etoto_2Ebit2,inj__ty_2Etoto_2Enum__dt(V1a)))))) & ( ! [V2a_27:tp__ty_2Etoto_2Enum__dt] : ( ! [V3a:tp__ty_2Etoto_2Enum__dt] : (~~ (surj__ty_2Etoto_2Enum__dt(ap(c_2Etoto_2Ebit1,inj__ty_2Etoto_2Enum__dt(V3a))) = surj__ty_2Etoto_2Enum__dt(ap(c_2Etoto_2Ebit2,inj__ty_2Etoto_2Enum__dt(V2a_27))))))))))).
tff(conj_thm_2Etoto_2Enum__dt__nchotomy,lemma,(( ! [V0nn:tp__ty_2Etoto_2Enum__dt] : ((V0nn = fo__c_2Etoto_2Ezer) | ((? [V1n:tp__ty_2Etoto_2Enum__dt] : (V0nn = surj__ty_2Etoto_2Enum__dt(ap(c_2Etoto_2Ebit1,inj__ty_2Etoto_2Enum__dt(V1n))))) | (? [V2n:tp__ty_2Etoto_2Enum__dt] : (V0nn = surj__ty_2Etoto_2Enum__dt(ap(c_2Etoto_2Ebit2,inj__ty_2Etoto_2Enum__dt(V2n)))))))))).
tff(conj_thm_2Etoto_2Enum__dt__Axiom,lemma,(( ! [A_27a:del]: ( ! [V0f0:$i] : (mem(V0f0,A_27a) => ( ! [V1f1:$i] : (mem(V1f1,arr(ty_2Etoto_2Enum__dt,arr(A_27a,A_27a))) => ( ! [V2f2:$i] : (mem(V2f2,arr(ty_2Etoto_2Enum__dt,arr(A_27a,A_27a))) => (? [V3fn:$i] : (mem(V3fn,arr(ty_2Etoto_2Enum__dt,A_27a)) & ((ap(V3fn,inj__ty_2Etoto_2Enum__dt(fo__c_2Etoto_2Ezer)) = V0f0) & (( ! [V4a:tp__ty_2Etoto_2Enum__dt] : (ap(V3fn,ap(c_2Etoto_2Ebit1,inj__ty_2Etoto_2Enum__dt(V4a))) = ap(ap(V1f1,inj__ty_2Etoto_2Enum__dt(V4a)),ap(V3fn,inj__ty_2Etoto_2Enum__dt(V4a))))) & ( ! [V5a:tp__ty_2Etoto_2Enum__dt] : (ap(V3fn,ap(c_2Etoto_2Ebit2,inj__ty_2Etoto_2Enum__dt(V5a))) = ap(ap(V2f2,inj__ty_2Etoto_2Enum__dt(V5a)),ap(V3fn,inj__ty_2Etoto_2Enum__dt(V5a)))))))))))))))))).
tff(conj_thm_2Etoto_2Enum__dt__induction,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2Etoto_2Enum__dt,bool)) => ((p(ap(V0P,inj__ty_2Etoto_2Enum__dt(fo__c_2Etoto_2Ezer))) & (( ! [V1n:tp__ty_2Etoto_2Enum__dt] : (p(ap(V0P,inj__ty_2Etoto_2Enum__dt(V1n))) => p(ap(V0P,ap(c_2Etoto_2Ebit1,inj__ty_2Etoto_2Enum__dt(V1n)))))) & ( ! [V2n:tp__ty_2Etoto_2Enum__dt] : (p(ap(V0P,inj__ty_2Etoto_2Enum__dt(V2n))) => p(ap(V0P,ap(c_2Etoto_2Ebit2,inj__ty_2Etoto_2Enum__dt(V2n)))))))) => ( ! [V3n:tp__ty_2Etoto_2Enum__dt] : p(ap(V0P,inj__ty_2Etoto_2Enum__dt(V3n))))))))).
tff(conj_thm_2Etoto_2Enum__dt__case__cong,lemma,(( ! [A_27a:del]: ( ! [V0v_27:$i] : (mem(V0v_27,A_27a) => ( ! [V1f_27:$i] : (mem(V1f_27,arr(ty_2Etoto_2Enum__dt,A_27a)) => ( ! [V2f1_27:$i] : (mem(V2f1_27,arr(ty_2Etoto_2Enum__dt,A_27a)) => ( ! [V3M:tp__ty_2Etoto_2Enum__dt] : ( ! [V4M_27:tp__ty_2Etoto_2Enum__dt] : ( ! [V5v:$i] : (mem(V5v,A_27a) => ( ! [V6f:$i] : (mem(V6f,arr(ty_2Etoto_2Enum__dt,A_27a)) => ( ! [V7f1:$i] : (mem(V7f1,arr(ty_2Etoto_2Enum__dt,A_27a)) => (((V3M = V4M_27) & (((V4M_27 = fo__c_2Etoto_2Ezer) => (V5v = V0v_27)) & (( ! [V8a:tp__ty_2Etoto_2Enum__dt] : ((V4M_27 = surj__ty_2Etoto_2Enum__dt(ap(c_2Etoto_2Ebit1,inj__ty_2Etoto_2Enum__dt(V8a)))) => (ap(V6f,inj__ty_2Etoto_2Enum__dt(V8a)) = ap(V1f_27,inj__ty_2Etoto_2Enum__dt(V8a))))) & ( ! [V9a:tp__ty_2Etoto_2Enum__dt] : ((V4M_27 = surj__ty_2Etoto_2Enum__dt(ap(c_2Etoto_2Ebit2,inj__ty_2Etoto_2Enum__dt(V9a)))) => (ap(V7f1,inj__ty_2Etoto_2Enum__dt(V9a)) = ap(V2f1_27,inj__ty_2Etoto_2Enum__dt(V9a)))))))) => (ap(ap(ap(ap(c_2Etoto_2Enum__dt__CASE(A_27a),inj__ty_2Etoto_2Enum__dt(V3M)),V5v),V6f),V7f1) = ap(ap(ap(ap(c_2Etoto_2Enum__dt__CASE(A_27a),inj__ty_2Etoto_2Enum__dt(V4M_27)),V0v_27),V1f_27),V2f1_27)))))))))))))))))))).
tff(conj_thm_2Etoto_2Enum__dt__case__eq,lemma,(( ! [A_27a:del]: ( ! [V0x:tp__ty_2Etoto_2Enum__dt] : ( ! [V1v:$i] : (mem(V1v,A_27a) => ( ! [V2f:$i] : (mem(V2f,arr(ty_2Etoto_2Enum__dt,A_27a)) => ( ! [V3f1:$i] : (mem(V3f1,arr(ty_2Etoto_2Enum__dt,A_27a)) => ( ! [V4v_27:$i] : (mem(V4v_27,A_27a) => ((ap(ap(ap(ap(c_2Etoto_2Enum__dt__CASE(A_27a),inj__ty_2Etoto_2Enum__dt(V0x)),V1v),V2f),V3f1) = V4v_27) <=> (((V0x = fo__c_2Etoto_2Ezer) & (V1v = V4v_27)) | ((? [V5n:tp__ty_2Etoto_2Enum__dt] : ((V0x = surj__ty_2Etoto_2Enum__dt(ap(c_2Etoto_2Ebit1,inj__ty_2Etoto_2Enum__dt(V5n)))) & (ap(V2f,inj__ty_2Etoto_2Enum__dt(V5n)) = V4v_27))) | (? [V6n:tp__ty_2Etoto_2Enum__dt] : ((V0x = surj__ty_2Etoto_2Enum__dt(ap(c_2Etoto_2Ebit2,inj__ty_2Etoto_2Enum__dt(V6n)))) & (ap(V3f1,inj__ty_2Etoto_2Enum__dt(V6n)) = V4v_27)))))))))))))))))).
tff(ax_thm_2Etoto_2Enum__to__dt__primitive,axiom,(c_2Etoto_2Enum__to__dt = ap(ap(c_2Erelation_2EWFREC(ty_2Enum_2Enum,ty_2Etoto_2Enum__dt),ap(c_2Emin_2E_40(arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))),f2272)),f2274))).
tff(conj_thm_2Etoto_2Enum__dtOrd__ind,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2Etoto_2Enum__dt,arr(ty_2Etoto_2Enum__dt,bool))) => ((p(ap(ap(V0P,inj__ty_2Etoto_2Enum__dt(fo__c_2Etoto_2Ezer)),inj__ty_2Etoto_2Enum__dt(fo__c_2Etoto_2Ezer))) & (( ! [V1x:tp__ty_2Etoto_2Enum__dt] : p(ap(ap(V0P,inj__ty_2Etoto_2Enum__dt(fo__c_2Etoto_2Ezer)),ap(c_2Etoto_2Ebit1,inj__ty_2Etoto_2Enum__dt(V1x))))) & (( ! [V2x:tp__ty_2Etoto_2Enum__dt] : p(ap(ap(V0P,inj__ty_2Etoto_2Enum__dt(fo__c_2Etoto_2Ezer)),ap(c_2Etoto_2Ebit2,inj__ty_2Etoto_2Enum__dt(V2x))))) & (( ! [V3x:tp__ty_2Etoto_2Enum__dt] : p(ap(ap(V0P,ap(c_2Etoto_2Ebit1,inj__ty_2Etoto_2Enum__dt(V3x))),inj__ty_2Etoto_2Enum__dt(fo__c_2Etoto_2Ezer)))) & (( ! [V4x:tp__ty_2Etoto_2Enum__dt] : p(ap(ap(V0P,ap(c_2Etoto_2Ebit2,inj__ty_2Etoto_2Enum__dt(V4x))),inj__ty_2Etoto_2Enum__dt(fo__c_2Etoto_2Ezer)))) & (( ! [V5x:tp__ty_2Etoto_2Enum__dt] : ( ! [V6y:tp__ty_2Etoto_2Enum__dt] : p(ap(ap(V0P,ap(c_2Etoto_2Ebit1,inj__ty_2Etoto_2Enum__dt(V5x))),ap(c_2Etoto_2Ebit2,inj__ty_2Etoto_2Enum__dt(V6y)))))) & (( ! [V7x:tp__ty_2Etoto_2Enum__dt] : ( ! [V8y:tp__ty_2Etoto_2Enum__dt] : p(ap(ap(V0P,ap(c_2Etoto_2Ebit2,inj__ty_2Etoto_2Enum__dt(V7x))),ap(c_2Etoto_2Ebit1,inj__ty_2Etoto_2Enum__dt(V8y)))))) & (( ! [V9x:tp__ty_2Etoto_2Enum__dt] : ( ! [V10y:tp__ty_2Etoto_2Enum__dt] : (p(ap(ap(V0P,inj__ty_2Etoto_2Enum__dt(V9x)),inj__ty_2Etoto_2Enum__dt(V10y))) => p(ap(ap(V0P,ap(c_2Etoto_2Ebit1,inj__ty_2Etoto_2Enum__dt(V9x))),ap(c_2Etoto_2Ebit1,inj__ty_2Etoto_2Enum__dt(V10y))))))) & ( ! [V11x:tp__ty_2Etoto_2Enum__dt] : ( ! [V12y:tp__ty_2Etoto_2Enum__dt] : (p(ap(ap(V0P,inj__ty_2Etoto_2Enum__dt(V11x)),inj__ty_2Etoto_2Enum__dt(V12y))) => p(ap(ap(V0P,ap(c_2Etoto_2Ebit2,inj__ty_2Etoto_2Enum__dt(V11x))),ap(c_2Etoto_2Ebit2,inj__ty_2Etoto_2Enum__dt(V12y))))))))))))))) => ( ! [V13v:tp__ty_2Etoto_2Enum__dt] : ( ! [V14v1:tp__ty_2Etoto_2Enum__dt] : p(ap(ap(V0P,inj__ty_2Etoto_2Enum__dt(V13v)),inj__ty_2Etoto_2Enum__dt(V14v1)))))))))).
tff(conj_thm_2Etoto_2Enum__dtOrd,lemma,(((surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2Enum__dtOrd,inj__ty_2Etoto_2Enum__dt(fo__c_2Etoto_2Ezer)),inj__ty_2Etoto_2Enum__dt(fo__c_2Etoto_2Ezer))) = fo__c_2EternaryComparisons_2EEQUAL) & (( ! [V0x:tp__ty_2Etoto_2Enum__dt] : (surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2Enum__dtOrd,inj__ty_2Etoto_2Enum__dt(fo__c_2Etoto_2Ezer)),ap(c_2Etoto_2Ebit1,inj__ty_2Etoto_2Enum__dt(V0x)))) = fo__c_2EternaryComparisons_2ELESS)) & (( ! [V1x:tp__ty_2Etoto_2Enum__dt] : (surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2Enum__dtOrd,inj__ty_2Etoto_2Enum__dt(fo__c_2Etoto_2Ezer)),ap(c_2Etoto_2Ebit2,inj__ty_2Etoto_2Enum__dt(V1x)))) = fo__c_2EternaryComparisons_2ELESS)) & (( ! [V2x:tp__ty_2Etoto_2Enum__dt] : (surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2Enum__dtOrd,ap(c_2Etoto_2Ebit1,inj__ty_2Etoto_2Enum__dt(V2x))),inj__ty_2Etoto_2Enum__dt(fo__c_2Etoto_2Ezer))) = fo__c_2EternaryComparisons_2EGREATER)) & (( ! [V3x:tp__ty_2Etoto_2Enum__dt] : (surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2Enum__dtOrd,ap(c_2Etoto_2Ebit2,inj__ty_2Etoto_2Enum__dt(V3x))),inj__ty_2Etoto_2Enum__dt(fo__c_2Etoto_2Ezer))) = fo__c_2EternaryComparisons_2EGREATER)) & (( ! [V4y:tp__ty_2Etoto_2Enum__dt] : ( ! [V5x:tp__ty_2Etoto_2Enum__dt] : (surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2Enum__dtOrd,ap(c_2Etoto_2Ebit1,inj__ty_2Etoto_2Enum__dt(V5x))),ap(c_2Etoto_2Ebit2,inj__ty_2Etoto_2Enum__dt(V4y)))) = fo__c_2EternaryComparisons_2ELESS))) & (( ! [V6y:tp__ty_2Etoto_2Enum__dt] : ( ! [V7x:tp__ty_2Etoto_2Enum__dt] : (surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2Enum__dtOrd,ap(c_2Etoto_2Ebit2,inj__ty_2Etoto_2Enum__dt(V7x))),ap(c_2Etoto_2Ebit1,inj__ty_2Etoto_2Enum__dt(V6y)))) = fo__c_2EternaryComparisons_2EGREATER))) & (( ! [V8y:tp__ty_2Etoto_2Enum__dt] : ( ! [V9x:tp__ty_2Etoto_2Enum__dt] : (surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2Enum__dtOrd,ap(c_2Etoto_2Ebit1,inj__ty_2Etoto_2Enum__dt(V9x))),ap(c_2Etoto_2Ebit1,inj__ty_2Etoto_2Enum__dt(V8y)))) = surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2Enum__dtOrd,inj__ty_2Etoto_2Enum__dt(V9x)),inj__ty_2Etoto_2Enum__dt(V8y)))))) & ( ! [V10y:tp__ty_2Etoto_2Enum__dt] : ( ! [V11x:tp__ty_2Etoto_2Enum__dt] : (surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2Enum__dtOrd,ap(c_2Etoto_2Ebit2,inj__ty_2Etoto_2Enum__dt(V11x))),ap(c_2Etoto_2Ebit2,inj__ty_2Etoto_2Enum__dt(V10y)))) = surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2Enum__dtOrd,inj__ty_2Etoto_2Enum__dt(V11x)),inj__ty_2Etoto_2Enum__dt(V10y)))))))))))))))).
tff(ax_thm_2Etoto_2Eqk__numOrd__def,axiom,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2Eqk__numOrd,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2Enum__dtOrd,ap(c_2Etoto_2Enum__to__dt,inj__ty_2Enum_2Enum(V0m))),ap(c_2Etoto_2Enum__to__dt,inj__ty_2Enum_2Enum(V1n)))))))).
tff(conj_thm_2Etoto_2ETO__qk__numOrd,lemma,(p(ap(c_2Etoto_2ETotOrd(ty_2Enum_2Enum),c_2Etoto_2Eqk__numOrd)))).
tff(conj_thm_2Etoto_2Eqk__numeralOrd,lemma,(( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1y:tp__ty_2Enum_2Enum] : ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2Eqk__numOrd,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))) = fo__c_2EternaryComparisons_2EEQUAL) & ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2Eqk__numOrd,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1y)))) = fo__c_2EternaryComparisons_2ELESS) & ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2Eqk__numOrd,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1y)))) = fo__c_2EternaryComparisons_2ELESS) & ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2Eqk__numOrd,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0x))),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))) = fo__c_2EternaryComparisons_2EGREATER) & ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2Eqk__numOrd,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0x))),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))) = fo__c_2EternaryComparisons_2EGREATER) & ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2Eqk__numOrd,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0x))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1y)))) = surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2Eqk__numOrd,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1y)))) & ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2Eqk__numOrd,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0x))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1y)))) = surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2Eqk__numOrd,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1y)))) & ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2Eqk__numOrd,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0x))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1y)))) = fo__c_2EternaryComparisons_2ELESS) & (surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2Eqk__numOrd,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0x))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1y)))) = fo__c_2EternaryComparisons_2EGREATER))))))))))))).
tff(ax_thm_2Etoto_2Eqk__numto,axiom,(surj__c_ty_2Etoto_2Etoto_ty_2Enum_2Enum(c_2Etoto_2Eqk__numto) = surj__c_ty_2Etoto_2Etoto_ty_2Enum_2Enum(ap(c_2Etoto_2ETO(ty_2Enum_2Enum),c_2Etoto_2Eqk__numOrd)))).
tff(conj_thm_2Etoto_2Eap__qk__numto__thm,lemma,((ap(c_2Etoto_2Eapto(ty_2Enum_2Enum),c_2Etoto_2Eqk__numto) = c_2Etoto_2Eqk__numOrd))).
tff(ax_thm_2Etoto_2EcharOrd,axiom,( ! [V0a:tp__ty_2Estring_2Echar] : ( ! [V1b:tp__ty_2Estring_2Echar] : (surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2EcharOrd,inj__ty_2Estring_2Echar(V0a)),inj__ty_2Estring_2Echar(V1b))) = surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2EnumOrd,ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0a))),ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V1b)))))))).
tff(ax_thm_2Etoto_2Echarto,axiom,(surj__c_ty_2Etoto_2Etoto_ty_2Estring_2Echar(c_2Etoto_2Echarto) = surj__c_ty_2Etoto_2Etoto_ty_2Estring_2Echar(ap(c_2Etoto_2ETO(ty_2Estring_2Echar),c_2Etoto_2EcharOrd)))).
tff(conj_thm_2Etoto_2ETO__charOrd,lemma,(p(ap(c_2Etoto_2ETotOrd(ty_2Estring_2Echar),c_2Etoto_2EcharOrd)))).
tff(conj_thm_2Etoto_2Eapcharto__thm,lemma,((ap(c_2Etoto_2Eapto(ty_2Estring_2Echar),c_2Etoto_2Echarto) = c_2Etoto_2EcharOrd))).
tff(conj_thm_2Etoto_2EcharOrd__lt__lem,lemma,(( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2EnumOrd,inj__ty_2Enum_2Enum(V0a)),inj__ty_2Enum_2Enum(V1b))) = fo__c_2EternaryComparisons_2ELESS) => ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1b)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))) <=> $true) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2EcharOrd,ap(c_2Estring_2ECHR,inj__ty_2Enum_2Enum(V0a))),ap(c_2Estring_2ECHR,inj__ty_2Enum_2Enum(V1b)))) = fo__c_2EternaryComparisons_2ELESS))))))).
tff(conj_thm_2Etoto_2EcharOrd__gt__lem,lemma,(( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2EnumOrd,inj__ty_2Enum_2Enum(V0a)),inj__ty_2Enum_2Enum(V1b))) = fo__c_2EternaryComparisons_2EGREATER) => ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0a)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))) <=> $true) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2EcharOrd,ap(c_2Estring_2ECHR,inj__ty_2Enum_2Enum(V0a))),ap(c_2Estring_2ECHR,inj__ty_2Enum_2Enum(V1b)))) = fo__c_2EternaryComparisons_2EGREATER))))))).
tff(conj_thm_2Etoto_2EcharOrd__eq__lem,lemma,(( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2EnumOrd,inj__ty_2Enum_2Enum(V0a)),inj__ty_2Enum_2Enum(V1b))) = fo__c_2EternaryComparisons_2EEQUAL) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(c_2Etoto_2EcharOrd,ap(c_2Estring_2ECHR,inj__ty_2Enum_2Enum(V0a))),ap(c_2Estring_2ECHR,inj__ty_2Enum_2Enum(V1b)))) = fo__c_2EternaryComparisons_2EEQUAL)))))).
tff(conj_thm_2Etoto_2EcharOrd__thm,lemma,((c_2Etoto_2EcharOrd = ap(c_2Etoto_2ETO__of__LinearOrder(ty_2Estring_2Echar),c_2Estring_2Echar__lt)))).
tff(conj_thm_2Etoto_2Elistorder__ind,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(arr(A_27a,arr(A_27a,bool)),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Elist_2Elist(A_27a),bool)))) => ((( ! [V1V:$i] : (mem(V1V,arr(A_27a,arr(A_27a,bool))) => ( ! [V2l:$i] : (mem(V2l,ty_2Elist_2Elist(A_27a)) => p(ap(ap(ap(V0P,V1V),V2l),c_2Elist_2ENIL(A_27a))))))) & (( ! [V3V:$i] : (mem(V3V,arr(A_27a,arr(A_27a,bool))) => ( ! [V4s:$i] : (mem(V4s,A_27a) => ( ! [V5m:$i] : (mem(V5m,ty_2Elist_2Elist(A_27a)) => p(ap(ap(ap(V0P,V3V),c_2Elist_2ENIL(A_27a)),ap(ap(c_2Elist_2ECONS(A_27a),V4s),V5m))))))))) & ( ! [V6V:$i] : (mem(V6V,arr(A_27a,arr(A_27a,bool))) => ( ! [V7r:$i] : (mem(V7r,A_27a) => ( ! [V8l:$i] : (mem(V8l,ty_2Elist_2Elist(A_27a)) => ( ! [V9s:$i] : (mem(V9s,A_27a) => ( ! [V10m:$i] : (mem(V10m,ty_2Elist_2Elist(A_27a)) => (p(ap(ap(ap(V0P,V6V),V8l),V10m)) => p(ap(ap(ap(V0P,V6V),ap(ap(c_2Elist_2ECONS(A_27a),V7r),V8l)),ap(ap(c_2Elist_2ECONS(A_27a),V9s),V10m)))))))))))))))) => ( ! [V11v:$i] : (mem(V11v,arr(A_27a,arr(A_27a,bool))) => ( ! [V12v1:$i] : (mem(V12v1,ty_2Elist_2Elist(A_27a)) => ( ! [V13v2:$i] : (mem(V13v2,ty_2Elist_2Elist(A_27a)) => p(ap(ap(ap(V0P,V11v),V12v1),V13v2)))))))))))))).
tff(conj_thm_2Etoto_2Elistorder,conjecture,(( ! [A_27a:del]: (( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ! [V1V:$i] : (mem(V1V,arr(A_27a,arr(A_27a,bool))) => (p(ap(ap(ap(c_2Etoto_2Elistorder(A_27a),V1V),V0l),c_2Elist_2ENIL(A_27a))) <=> $false))))) & (( ! [V2s:$i] : (mem(V2s,A_27a) => ( ! [V3m:$i] : (mem(V3m,ty_2Elist_2Elist(A_27a)) => ( ! [V4V:$i] : (mem(V4V,arr(A_27a,arr(A_27a,bool))) => (p(ap(ap(ap(c_2Etoto_2Elistorder(A_27a),V4V),c_2Elist_2ENIL(A_27a)),ap(ap(c_2Elist_2ECONS(A_27a),V2s),V3m))) <=> $true))))))) & ( ! [V5s:$i] : (mem(V5s,A_27a) => ( ! [V6r:$i] : (mem(V6r,A_27a) => ( ! [V7m:$i] : (mem(V7m,ty_2Elist_2Elist(A_27a)) => ( ! [V8l:$i] : (mem(V8l,ty_2Elist_2Elist(A_27a)) => ( ! [V9V:$i] : (mem(V9V,arr(A_27a,arr(A_27a,bool))) => (p(ap(ap(ap(c_2Etoto_2Elistorder(A_27a),V9V),ap(ap(c_2Elist_2ECONS(A_27a),V6r),V8l)),ap(ap(c_2Elist_2ECONS(A_27a),V5s),V7m))) <=> (p(ap(ap(V9V,V6r),V5s)) | ((V6r = V5s) & p(ap(ap(ap(c_2Etoto_2Elistorder(A_27a),V9V),V8l),V7m)))))))))))))))))))).
