include('Axioms/words^2.ax').
thf(tp_ty_2Etoto_2Enum__dt,type,( ty_2Etoto_2Enum__dt:del )).
thf(tp_ty_2Etoto_2Etoto,type,( ty_2Etoto_2Etoto: del >del )).
thf(tp_c_2Etoto_2EListOrd,type,(c_2Etoto_2EListOrd:(del>$i))).
thf(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)))))).
thf(tp_c_2Etoto_2EStrongLinearOrder__of__TO,type,(c_2Etoto_2EStrongLinearOrder__of__TO:(del>$i))).
thf(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)))))).
thf(tp_c_2Etoto_2ETO,type,(c_2Etoto_2ETO:(del>$i))).
thf(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))))).
thf(tp_c_2Etoto_2ETO__inv,type,(c_2Etoto_2ETO__inv:(del>$i))).
thf(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)))))).
thf(tp_c_2Etoto_2ETO__of__LinearOrder,type,(c_2Etoto_2ETO__of__LinearOrder:(del>$i))).
thf(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)))))).
thf(tp_c_2Etoto_2ETotOrd,type,(c_2Etoto_2ETotOrd:(del>$i))).
thf(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)))).
thf(tp_c_2Etoto_2EWeakLinearOrder__of__TO,type,(c_2Etoto_2EWeakLinearOrder__of__TO:(del>$i))).
thf(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)))))).
thf(tp_c_2Etoto_2Eapto,type,(c_2Etoto_2Eapto:(del>$i))).
thf(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)))))).
thf(stp_ty_2Etoto_2Enum__dt,type,(tp__ty_2Etoto_2Enum__dt : $tType)).
thf(stp_inj_ty_2Etoto_2Enum__dt,type,(inj__ty_2Etoto_2Enum__dt : (tp__ty_2Etoto_2Enum__dt > $i))).
thf(stp_surj_ty_2Etoto_2Enum__dt,type,(surj__ty_2Etoto_2Enum__dt : ($i > tp__ty_2Etoto_2Enum__dt))).
thf(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))).
thf(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))).
thf(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)))))).
thf(tp_c_2Etoto_2Ebit1,type,(c_2Etoto_2Ebit1:$i)).
thf(mem_c_2Etoto_2Ebit1,axiom,(mem@c_2Etoto_2Ebit1@(arr@ty_2Etoto_2Enum__dt@ty_2Etoto_2Enum__dt))).
thf(stp_fo_c_2Etoto_2Ebit1,type,(fo__c_2Etoto_2Ebit1:(tp__ty_2Etoto_2Enum__dt > tp__ty_2Etoto_2Enum__dt))).
thf(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))))).
thf(tp_c_2Etoto_2Ebit2,type,(c_2Etoto_2Ebit2:$i)).
thf(mem_c_2Etoto_2Ebit2,axiom,(mem@c_2Etoto_2Ebit2@(arr@ty_2Etoto_2Enum__dt@ty_2Etoto_2Enum__dt))).
thf(stp_fo_c_2Etoto_2Ebit2,type,(fo__c_2Etoto_2Ebit2:(tp__ty_2Etoto_2Enum__dt > tp__ty_2Etoto_2Enum__dt))).
thf(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))))).
thf(tp_c_2Etoto_2EcharOrd,type,(c_2Etoto_2EcharOrd:$i)).
thf(mem_c_2Etoto_2EcharOrd,axiom,(mem@c_2Etoto_2EcharOrd@(arr@ty_2Estring_2Echar@(arr@ty_2Estring_2Echar@ty_2EternaryComparisons_2Eordering)))).
thf(stp_fo_c_2Etoto_2EcharOrd,type,(fo__c_2Etoto_2EcharOrd:(tp__ty_2Estring_2Echar > (tp__ty_2Estring_2Echar > tp__ty_2EternaryComparisons_2Eordering)))).
thf(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)))))).
thf(stp_c_ty_2Etoto_2Etoto_ty_2Estring_2Echar,type,(tp__c_ty_2Etoto_2Etoto_ty_2Estring_2Echar : $tType)).
thf(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))).
thf(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))).
thf(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))).
thf(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)))).
thf(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)))))).
thf(tp_c_2Etoto_2Echarto,type,(c_2Etoto_2Echarto:$i)).
thf(mem_c_2Etoto_2Echarto,axiom,(mem@c_2Etoto_2Echarto@(ty_2Etoto_2Etoto@ty_2Estring_2Echar))).
thf(tp_c_2Etoto_2EimageOrd,type,(c_2Etoto_2EimageOrd:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2Etoto_2ElexTO,type,(c_2Etoto_2ElexTO:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2Etoto_2Elextoto,type,(c_2Etoto_2Elextoto:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2Etoto_2Elistorder,type,(c_2Etoto_2Elistorder:(del>$i))).
thf(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)))))).
thf(tp_c_2Etoto_2Elistoto,type,(c_2Etoto_2Elistoto:(del>$i))).
thf(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)))))).
thf(tp_c_2Etoto_2EnumOrd,type,(c_2Etoto_2EnumOrd:$i)).
thf(mem_c_2Etoto_2EnumOrd,axiom,(mem@c_2Etoto_2EnumOrd@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2EternaryComparisons_2Eordering)))).
thf(stp_fo_c_2Etoto_2EnumOrd,type,(fo__c_2Etoto_2EnumOrd:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2EternaryComparisons_2Eordering)))).
thf(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)))))).
thf(tp_c_2Etoto_2Enum__dtOrd,type,(c_2Etoto_2Enum__dtOrd:$i)).
thf(mem_c_2Etoto_2Enum__dtOrd,axiom,(mem@c_2Etoto_2Enum__dtOrd@(arr@ty_2Etoto_2Enum__dt@(arr@ty_2Etoto_2Enum__dt@ty_2EternaryComparisons_2Eordering)))).
thf(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)))).
thf(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)))))).
thf(tp_c_2Etoto_2Enum__dt__CASE,type,(c_2Etoto_2Enum__dt__CASE:(del>$i))).
thf(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))))))).
thf(tp_c_2Etoto_2Enum__dt__size,type,(c_2Etoto_2Enum__dt__size:$i)).
thf(mem_c_2Etoto_2Enum__dt__size,axiom,(mem@c_2Etoto_2Enum__dt__size@(arr@ty_2Etoto_2Enum__dt@ty_2Enum_2Enum))).
thf(stp_fo_c_2Etoto_2Enum__dt__size,type,(fo__c_2Etoto_2Enum__dt__size:(tp__ty_2Etoto_2Enum__dt > tp__ty_2Enum_2Enum))).
thf(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))))).
thf(tp_c_2Etoto_2Enum__to__dt,type,(c_2Etoto_2Enum__to__dt:$i)).
thf(mem_c_2Etoto_2Enum__to__dt,axiom,(mem@c_2Etoto_2Enum__to__dt@(arr@ty_2Enum_2Enum@ty_2Etoto_2Enum__dt))).
thf(stp_fo_c_2Etoto_2Enum__to__dt,type,(fo__c_2Etoto_2Enum__to__dt:(tp__ty_2Enum_2Enum > tp__ty_2Etoto_2Enum__dt))).
thf(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))))).
thf(stp_c_ty_2Etoto_2Etoto_ty_2Enum_2Enum,type,(tp__c_ty_2Etoto_2Etoto_ty_2Enum_2Enum : $tType)).
thf(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))).
thf(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))).
thf(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))).
thf(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)))).
thf(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)))))).
thf(tp_c_2Etoto_2Enumto,type,(c_2Etoto_2Enumto:$i)).
thf(mem_c_2Etoto_2Enumto,axiom,(mem@c_2Etoto_2Enumto@(ty_2Etoto_2Etoto@ty_2Enum_2Enum))).
thf(tp_c_2Etoto_2Eqk__numOrd,type,(c_2Etoto_2Eqk__numOrd:$i)).
thf(mem_c_2Etoto_2Eqk__numOrd,axiom,(mem@c_2Etoto_2Eqk__numOrd@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2EternaryComparisons_2Eordering)))).
thf(stp_fo_c_2Etoto_2Eqk__numOrd,type,(fo__c_2Etoto_2Eqk__numOrd:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2EternaryComparisons_2Eordering)))).
thf(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)))))).
thf(tp_c_2Etoto_2Eqk__numto,type,(c_2Etoto_2Eqk__numto:$i)).
thf(mem_c_2Etoto_2Eqk__numto,axiom,(mem@c_2Etoto_2Eqk__numto@(ty_2Etoto_2Etoto@ty_2Enum_2Enum))).
thf(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)).
thf(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))).
thf(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))).
thf(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))).
thf(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))))).
thf(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)))))).
thf(tp_c_2Etoto_2Estringto,type,(c_2Etoto_2Estringto:$i)).
thf(mem_c_2Etoto_2Estringto,axiom,(mem@c_2Etoto_2Estringto@(ty_2Etoto_2Etoto@(ty_2Elist_2Elist@ty_2Estring_2Echar)))).
thf(tp_c_2Etoto_2Etoto__inv,type,(c_2Etoto_2Etoto__inv:(del>$i))).
thf(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))))).
thf(tp_c_2Etoto_2Etoto__of__LinearOrder,type,(c_2Etoto_2Etoto__of__LinearOrder:(del>$i))).
thf(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))))).
thf(tp_c_2Etoto_2Ezer,type,(c_2Etoto_2Ezer:$i)).
thf(mem_c_2Etoto_2Ezer,axiom,(mem@c_2Etoto_2Ezer@ty_2Etoto_2Enum__dt)).
thf(stp_fo_c_2Etoto_2Ezer,type,(fo__c_2Etoto_2Ezer:tp__ty_2Etoto_2Enum__dt)).
thf(stp_eq_fo_c_2Etoto_2Ezer,axiom,((inj__ty_2Etoto_2Enum__dt @ fo__c_2Etoto_2Ezer) = c_2Etoto_2Ezer)).
thf(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)))))).
thf(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))))))))))))))).
thf(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))))))))))))).
thf(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))))))))))).
thf(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)))))))).
thf(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))))))))))).
thf(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)))))).
thf(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)))))).
thf(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)))))).
thf(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))))))).
thf(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))))).
thf(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)))))).
thf(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)))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))).
thf(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)))))).
thf(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)))))))))))))).
thf(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))))))))))).
thf(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)))))))))).
thf(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)))))))))).
thf(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)))))))).
thf(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))))))).
thf(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)))))))))).
thf(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))))))))))).
thf(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)))))))))).
thf(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))))))).
thf(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)))))))))))).
thf(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)))))))))))).
thf(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))))))))))))).
thf(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))))))))))))).
thf(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))))))))))).
thf(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))))))))))))).
thf(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)))))))))))).
thf(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)))))))))))).
thf(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)))))))))))).
thf(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)))))))))))).
thf(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)))))))))))).
thf(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)))))))))))).
thf(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))))))))))))))))).
thf(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))@c_2Ebool_2ET)@c_2Ebool_2ET)@c_2Ebool_2EF))))))))))).
thf(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))@c_2Ebool_2ET)@c_2Ebool_2EF)@c_2Ebool_2EF))))))))))).
thf(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))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))).
thf(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))))).
thf(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))))).
thf(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)))))).
thf(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)))))).
thf(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))))))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))).
thf(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))))))).
thf(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)))))))).
thf(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)))))))).
thf(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))))).
thf(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))))).
thf(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))))))).
thf(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)))))))))))).
thf(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)))))))))))).
thf(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))))))))))))).
thf(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)))))))))))))))).
thf(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)))))))).
thf(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))))))))))))))))).
thf(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))))))))))).
thf(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))))))))))).
thf(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))))))))))).
thf(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)))))))))))))))).
thf(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)@(lam@A_27a@(^ [V2r:$i] : (lam@A_27b@(^ [V3u:$i] : (ap@(c_2Ebool_2E_21@(ty_2Epair_2Eprod@A_27a@A_27b))@(ap@(c_2Epair_2EUNCURRY@A_27a@A_27b@bool)@(lam@A_27a@(^ [V4r_27:$i] : (lam@A_27b@(^ [V5u_27:$i] : (ap@(ap@(c_2Emin_2E_3D@ty_2EternaryComparisons_2Eordering)@(ap@(ap@(ap@(ap@(c_2Etoto_2ElexTO@A_27a@A_27b)@V0R)@V1V)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V2r)@V3u))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V4r_27)@V5u_27)))@(ap@(ap@(ap@(ap@(c_2EternaryComparisons_2Eordering__CASE@ty_2EternaryComparisons_2Eordering)@(ap@(ap@V0R@V2r)@V4r_27))@(inj__ty_2EternaryComparisons_2Eordering @ fo__c_2EternaryComparisons_2ELESS))@(ap@(ap@V1V@V3u)@V5u_27))@(inj__ty_2EternaryComparisons_2Eordering @ fo__c_2EternaryComparisons_2EGREATER)))))))))))))))))))))))).
thf(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))))))))))).
thf(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))))))))))))))).
thf(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))))))))))))))))))).
thf(conj_thm_2Etoto_2EStrongLinearOrder__LESS,lemma,(p@(ap@(c_2Erelation_2EStrongLinearOrder@ty_2Enum_2Enum)@c_2Eprim__rec_2E_3C))).
thf(ax_thm_2Etoto_2EnumOrd,axiom,(c_2Etoto_2EnumOrd = (ap@(c_2Etoto_2ETO__of__LinearOrder@ty_2Enum_2Enum)@c_2Eprim__rec_2E_3C))).
thf(conj_thm_2Etoto_2ETO__numOrd,lemma,(p@(ap@(c_2Etoto_2ETotOrd@ty_2Enum_2Enum)@c_2Etoto_2EnumOrd))).
thf(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)))).
thf(conj_thm_2Etoto_2Eapnumto__thm,lemma,((ap@(c_2Etoto_2Eapto@ty_2Enum_2Enum)@c_2Etoto_2Enumto) = c_2Etoto_2EnumOrd)).
thf(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))))))))))))))).
thf(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)@(lam@(ty_2Eind__type_2Erecspace@bool)@(^ [V1a0:$i] : (ap@(c_2Ebool_2E_21@(arr@(ty_2Eind__type_2Erecspace@bool)@bool))@(lam@(arr@(ty_2Eind__type_2Erecspace@bool)@bool)@(^ [V2_27num__dt_27:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(c_2Ebool_2E_21@(ty_2Eind__type_2Erecspace@bool))@(lam@(ty_2Eind__type_2Erecspace@bool)@(^ [V3a0:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(c_2Emin_2E_3D@(ty_2Eind__type_2Erecspace@bool))@V3a0)@(ap@(ap@(ap@(c_2Eind__type_2ECONSTR@bool)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(c_2Ebool_2EARB@bool))@(lam@ty_2Enum_2Enum@(^ [V4n:$i] : (c_2Eind__type_2EBOTTOM@bool))))))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(c_2Ebool_2E_3F@(ty_2Eind__type_2Erecspace@bool))@(lam@(ty_2Eind__type_2Erecspace@bool)@(^ [V5a:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@(ty_2Eind__type_2Erecspace@bool))@V3a0)@(ap@(lam@(ty_2Eind__type_2Erecspace@bool)@(^ [V6a:$i] : (ap@(ap@(ap@(c_2Eind__type_2ECONSTR@bool)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(c_2Ebool_2EARB@bool))@(ap@(ap@(c_2Eind__type_2EFCONS@(ty_2Eind__type_2Erecspace@bool))@V6a)@(lam@ty_2Enum_2Enum@(^ [V7n:$i] : (c_2Eind__type_2EBOTTOM@bool)))))))@V5a)))@(ap@V2_27num__dt_27@V5a))))))@(ap@(c_2Ebool_2E_3F@(ty_2Eind__type_2Erecspace@bool))@(lam@(ty_2Eind__type_2Erecspace@bool)@(^ [V8a:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@(ty_2Eind__type_2Erecspace@bool))@V3a0)@(ap@(lam@(ty_2Eind__type_2Erecspace@bool)@(^ [V9a:$i] : (ap@(ap@(ap@(c_2Eind__type_2ECONSTR@bool)@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))@(c_2Ebool_2EARB@bool))@(ap@(ap@(c_2Eind__type_2EFCONS@(ty_2Eind__type_2Erecspace@bool))@V9a)@(lam@ty_2Enum_2Enum@(^ [V10n:$i] : (c_2Eind__type_2EBOTTOM@bool)))))))@V8a)))@(ap@V2_27num__dt_27@V8a))))))))@(ap@V2_27num__dt_27@V3a0))))))@(ap@V2_27num__dt_27@V1a0))))))))@V0rep))))).
thf(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)))))))))))))).
thf(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))))))))).
thf(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)))))).
thf(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)))))).
thf(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)))))))))).
thf(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))))))))).
thf(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))))))))))))))))).
thf(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)))))))).
thf(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))))))))))))))))))).
thf(conj_thm_2Etoto_2Enum__dt__case__eq,conjecture,( ! [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))))))))))))))))).
