include('Axioms/HL4001^2.ax').
thf(tp_ty_2EternaryComparisons_2Eordering,type,( ty_2EternaryComparisons_2Eordering:del )).
thf(stp_ty_2EternaryComparisons_2Eordering,type,(tp__ty_2EternaryComparisons_2Eordering : $tType)).
thf(stp_inj_ty_2EternaryComparisons_2Eordering,type,(inj__ty_2EternaryComparisons_2Eordering : (tp__ty_2EternaryComparisons_2Eordering > $i))).
thf(stp_surj_ty_2EternaryComparisons_2Eordering,type,(surj__ty_2EternaryComparisons_2Eordering : ($i > tp__ty_2EternaryComparisons_2Eordering))).
thf(stp_inj_surj_ty_2EternaryComparisons_2Eordering,axiom,( ! [X:tp__ty_2EternaryComparisons_2Eordering] : ((surj__ty_2EternaryComparisons_2Eordering @ (inj__ty_2EternaryComparisons_2Eordering @ X)) = X))).
thf(stp_inj_mem_ty_2EternaryComparisons_2Eordering,axiom,( ! [X:tp__ty_2EternaryComparisons_2Eordering] : (mem @ (inj__ty_2EternaryComparisons_2Eordering @ X) @ ty_2EternaryComparisons_2Eordering))).
thf(stp_iso_mem_ty_2EternaryComparisons_2Eordering,axiom,( ! [X:$i] : ((mem @ X @ ty_2EternaryComparisons_2Eordering) => (X = (inj__ty_2EternaryComparisons_2Eordering @ (surj__ty_2EternaryComparisons_2Eordering @ X)))))).
thf(tp_ty_2Equote_2Eindex,type,( ty_2Equote_2Eindex:del )).
thf(stp_ty_2Equote_2Eindex,type,(tp__ty_2Equote_2Eindex : $tType)).
thf(stp_inj_ty_2Equote_2Eindex,type,(inj__ty_2Equote_2Eindex : (tp__ty_2Equote_2Eindex > $i))).
thf(stp_surj_ty_2Equote_2Eindex,type,(surj__ty_2Equote_2Eindex : ($i > tp__ty_2Equote_2Eindex))).
thf(stp_inj_surj_ty_2Equote_2Eindex,axiom,( ! [X:tp__ty_2Equote_2Eindex] : ((surj__ty_2Equote_2Eindex @ (inj__ty_2Equote_2Eindex @ X)) = X))).
thf(stp_inj_mem_ty_2Equote_2Eindex,axiom,( ! [X:tp__ty_2Equote_2Eindex] : (mem @ (inj__ty_2Equote_2Eindex @ X) @ ty_2Equote_2Eindex))).
thf(stp_iso_mem_ty_2Equote_2Eindex,axiom,( ! [X:$i] : ((mem @ X @ ty_2Equote_2Eindex) => (X = (inj__ty_2Equote_2Eindex @ (surj__ty_2Equote_2Eindex @ X)))))).
thf(tp_c_2Equote_2Eindex__compare,type,(c_2Equote_2Eindex__compare:$i)).
thf(mem_c_2Equote_2Eindex__compare,axiom,(mem@c_2Equote_2Eindex__compare@(arr@ty_2Equote_2Eindex@(arr@ty_2Equote_2Eindex@ty_2EternaryComparisons_2Eordering)))).
thf(stp_fo_c_2Equote_2Eindex__compare,type,(fo__c_2Equote_2Eindex__compare:(tp__ty_2Equote_2Eindex > (tp__ty_2Equote_2Eindex > tp__ty_2EternaryComparisons_2Eordering)))).
thf(stp_eq_fo_c_2Equote_2Eindex__compare,axiom,( ! [X0:tp__ty_2Equote_2Eindex] : ( ! [X1:tp__ty_2Equote_2Eindex] : ((inj__ty_2EternaryComparisons_2Eordering @ ((fo__c_2Equote_2Eindex__compare @ X0) @ X1)) = (ap @ (ap @ c_2Equote_2Eindex__compare @ (inj__ty_2Equote_2Eindex @ X0)) @ (inj__ty_2Equote_2Eindex @ X1)))))).
thf(tp_ty_2Elist_2Elist,type,( ty_2Elist_2Elist: del >del )).
thf(tp_c_2EternaryComparisons_2Elist__compare,type,(c_2EternaryComparisons_2Elist__compare:(del>(del>$i)))).
thf(mem_c_2EternaryComparisons_2Elist__compare,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2EternaryComparisons_2Elist__compare@A_27a@A_27b)@(arr@(arr@A_27a@(arr@A_27b@ty_2EternaryComparisons_2Eordering))@(arr@(ty_2Elist_2Elist@A_27a)@(arr@(ty_2Elist_2Elist@A_27b)@ty_2EternaryComparisons_2Eordering))))))).
thf(tp_c_2EternaryComparisons_2Eordering__CASE,type,(c_2EternaryComparisons_2Eordering__CASE:(del>$i))).
thf(mem_c_2EternaryComparisons_2Eordering__CASE,axiom,( ! [A_27a:del] : (mem@(c_2EternaryComparisons_2Eordering__CASE@A_27a)@(arr@ty_2EternaryComparisons_2Eordering@(arr@A_27a@(arr@A_27a@(arr@A_27a@A_27a))))))).
thf(tp_c_2Equote_2Eindex__lt,type,(c_2Equote_2Eindex__lt:$i)).
thf(mem_c_2Equote_2Eindex__lt,axiom,(mem@c_2Equote_2Eindex__lt@(arr@ty_2Equote_2Eindex@(arr@ty_2Equote_2Eindex@bool)))).
thf(tp_c_2EternaryComparisons_2Elist__merge,type,(c_2EternaryComparisons_2Elist__merge:(del>$i))).
thf(mem_c_2EternaryComparisons_2Elist__merge,axiom,( ! [A_27a:del] : (mem@(c_2EternaryComparisons_2Elist__merge@A_27a)@(arr@(arr@A_27a@(arr@A_27a@bool))@(arr@(ty_2Elist_2Elist@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))))))).
thf(tp_c_2Ebool_2ECOND,type,(c_2Ebool_2ECOND:(del>$i))).
thf(mem_c_2Ebool_2ECOND,axiom,( ! [A_27a:del] : (mem@(c_2Ebool_2ECOND@A_27a)@(arr@bool@(arr@A_27a@(arr@A_27a@A_27a)))))).
thf(tp_ty_2Ecanonical_2Ecanonical__sum,type,( ty_2Ecanonical_2Ecanonical__sum: del >del )).
thf(stp_c_ty_2Elist_2Elist_ty_2Equote_2Eindex,type,(tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex : $tType)).
thf(stp_inj_c_ty_2Elist_2Elist_ty_2Equote_2Eindex,type,(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex : (tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex > $i))).
thf(stp_surj_c_ty_2Elist_2Elist_ty_2Equote_2Eindex,type,(surj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex : ($i > tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex))).
thf(stp_inj_surj_c_ty_2Elist_2Elist_ty_2Equote_2Eindex,axiom,( ! [X:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((surj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ (inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ X)) = X))).
thf(stp_inj_mem_c_ty_2Elist_2Elist_ty_2Equote_2Eindex,axiom,( ! [X:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : (mem @ (inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ X) @ (ty_2Elist_2Elist@ty_2Equote_2Eindex)))).
thf(stp_iso_mem_c_ty_2Elist_2Elist_ty_2Equote_2Eindex,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Elist_2Elist@ty_2Equote_2Eindex)) => (X = (inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ (surj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ X)))))).
thf(tp_c_2Ecanonical_2ECons__monom,type,(c_2Ecanonical_2ECons__monom:(del>$i))).
thf(mem_c_2Ecanonical_2ECons__monom,axiom,( ! [A_27a:del] : (mem@(c_2Ecanonical_2ECons__monom@A_27a)@(arr@A_27a@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@(arr@(ty_2Ecanonical_2Ecanonical__sum@A_27a)@(ty_2Ecanonical_2Ecanonical__sum@A_27a))))))).
thf(tp_c_2Ecanonical_2ENil__monom,type,(c_2Ecanonical_2ENil__monom:(del>$i))).
thf(mem_c_2Ecanonical_2ENil__monom,axiom,( ! [A_27a:del] : (mem@(c_2Ecanonical_2ENil__monom@A_27a)@(ty_2Ecanonical_2Ecanonical__sum@A_27a)))).
thf(tp_c_2Elist_2ENIL,type,(c_2Elist_2ENIL:(del>$i))).
thf(mem_c_2Elist_2ENIL,axiom,( ! [A_27a:del] : (mem@(c_2Elist_2ENIL@A_27a)@(ty_2Elist_2Elist@A_27a)))).
thf(tp_c_2Elist_2ECONS,type,(c_2Elist_2ECONS:(del>$i))).
thf(mem_c_2Elist_2ECONS,axiom,( ! [A_27a:del] : (mem@(c_2Elist_2ECONS@A_27a)@(arr@A_27a@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))))).
thf(tp_c_2Ecanonical_2ECons__varlist,type,(c_2Ecanonical_2ECons__varlist:(del>$i))).
thf(mem_c_2Ecanonical_2ECons__varlist,axiom,( ! [A_27a:del] : (mem@(c_2Ecanonical_2ECons__varlist@A_27a)@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@(arr@(ty_2Ecanonical_2Ecanonical__sum@A_27a)@(ty_2Ecanonical_2Ecanonical__sum@A_27a)))))).
thf(tp_ty_2Ecanonical_2Espolynom,type,( ty_2Ecanonical_2Espolynom: del >del )).
thf(tp_c_2Ecanonical_2ESPmult,type,(c_2Ecanonical_2ESPmult:(del>$i))).
thf(mem_c_2Ecanonical_2ESPmult,axiom,( ! [A_27a:del] : (mem@(c_2Ecanonical_2ESPmult@A_27a)@(arr@(ty_2Ecanonical_2Espolynom@A_27a)@(arr@(ty_2Ecanonical_2Espolynom@A_27a)@(ty_2Ecanonical_2Espolynom@A_27a)))))).
thf(tp_c_2Ecanonical_2ESPplus,type,(c_2Ecanonical_2ESPplus:(del>$i))).
thf(mem_c_2Ecanonical_2ESPplus,axiom,( ! [A_27a:del] : (mem@(c_2Ecanonical_2ESPplus@A_27a)@(arr@(ty_2Ecanonical_2Espolynom@A_27a)@(arr@(ty_2Ecanonical_2Espolynom@A_27a)@(ty_2Ecanonical_2Espolynom@A_27a)))))).
thf(tp_c_2Ecanonical_2ESPvar,type,(c_2Ecanonical_2ESPvar:(del>$i))).
thf(mem_c_2Ecanonical_2ESPvar,axiom,( ! [A_27a:del] : (mem@(c_2Ecanonical_2ESPvar@A_27a)@(arr@ty_2Equote_2Eindex@(ty_2Ecanonical_2Espolynom@A_27a))))).
thf(tp_c_2Ecanonical_2ESPconst,type,(c_2Ecanonical_2ESPconst:(del>$i))).
thf(mem_c_2Ecanonical_2ESPconst,axiom,( ! [A_27a:del] : (mem@(c_2Ecanonical_2ESPconst@A_27a)@(arr@A_27a@(ty_2Ecanonical_2Espolynom@A_27a))))).
thf(tp_c_2Emin_2E_3D_3D_3E,type,(c_2Emin_2E_3D_3D_3E:$i)).
thf(mem_c_2Emin_2E_3D_3D_3E,axiom,(mem@c_2Emin_2E_3D_3D_3E@(arr@bool@(arr@bool@bool)))).
thf(ax_imp_p,axiom,( ! [Q:$i] : ((mem@Q@bool) => ( ! [R:$i] : ((mem@R@bool) => ((p@(ap@(ap@c_2Emin_2E_3D_3D_3E@Q)@R)) <=> ((p@Q) => (p@R)))))))).
thf(tp_ty_2Esemi__ring_2Esemi__ring,type,( ty_2Esemi__ring_2Esemi__ring: del >del )).
thf(tp_c_2Esemi__ring_2Eis__semi__ring,type,(c_2Esemi__ring_2Eis__semi__ring:(del>$i))).
thf(mem_c_2Esemi__ring_2Eis__semi__ring,axiom,( ! [A_27a:del] : (mem@(c_2Esemi__ring_2Eis__semi__ring@A_27a)@(arr@(ty_2Esemi__ring_2Esemi__ring@A_27a)@bool)))).
thf(tp_ty_2Equote_2Evarmap,type,( ty_2Equote_2Evarmap: del >del )).
thf(tp_c_2Ecanonical_2Einterp__sp,type,(c_2Ecanonical_2Einterp__sp:(del>$i))).
thf(mem_c_2Ecanonical_2Einterp__sp,axiom,( ! [A_27a:del] : (mem@(c_2Ecanonical_2Einterp__sp@A_27a)@(arr@(ty_2Esemi__ring_2Esemi__ring@A_27a)@(arr@(ty_2Equote_2Evarmap@A_27a)@(arr@(ty_2Ecanonical_2Espolynom@A_27a)@A_27a)))))).
thf(tp_ty_2Enum_2Enum,type,( ty_2Enum_2Enum:del )).
thf(stp_ty_2Enum_2Enum,type,(tp__ty_2Enum_2Enum : $tType)).
thf(stp_inj_ty_2Enum_2Enum,type,(inj__ty_2Enum_2Enum : (tp__ty_2Enum_2Enum > $i))).
thf(stp_surj_ty_2Enum_2Enum,type,(surj__ty_2Enum_2Enum : ($i > tp__ty_2Enum_2Enum))).
thf(stp_inj_surj_ty_2Enum_2Enum,axiom,( ! [X:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (inj__ty_2Enum_2Enum @ X)) = X))).
thf(stp_inj_mem_ty_2Enum_2Enum,axiom,( ! [X:tp__ty_2Enum_2Enum] : (mem @ (inj__ty_2Enum_2Enum @ X) @ ty_2Enum_2Enum))).
thf(stp_iso_mem_ty_2Enum_2Enum,axiom,( ! [X:$i] : ((mem @ X @ ty_2Enum_2Enum) => (X = (inj__ty_2Enum_2Enum @ (surj__ty_2Enum_2Enum @ X)))))).
thf(stp_c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum,type,(tp__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum : $tType)).
thf(stp_inj_c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum,type,(inj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum : (tp__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum > $i))).
thf(stp_surj_c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum,type,(surj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum : ($i > tp__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum))).
thf(stp_inj_surj_c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum @ (inj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum @ X)) = X))).
thf(stp_inj_mem_c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum] : (mem @ (inj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum @ X) @ (ty_2Ecanonical_2Espolynom@ty_2Enum_2Enum)))).
thf(stp_iso_mem_c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Ecanonical_2Espolynom@ty_2Enum_2Enum)) => (X = (inj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum @ (surj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum @ X)))))).
thf(stp_c_ty_2Equote_2Evarmap_ty_2Enum_2Enum,type,(tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum : $tType)).
thf(stp_inj_c_ty_2Equote_2Evarmap_ty_2Enum_2Enum,type,(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum : (tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum > $i))).
thf(stp_surj_c_ty_2Equote_2Evarmap_ty_2Enum_2Enum,type,(surj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum : ($i > tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum))).
thf(stp_inj_surj_c_ty_2Equote_2Evarmap_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum] : ((surj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ (inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ X)) = X))).
thf(stp_inj_mem_c_ty_2Equote_2Evarmap_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum] : (mem @ (inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ X) @ (ty_2Equote_2Evarmap@ty_2Enum_2Enum)))).
thf(stp_iso_mem_c_ty_2Equote_2Evarmap_ty_2Enum_2Enum,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Equote_2Evarmap@ty_2Enum_2Enum)) => (X = (inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ (surj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ X)))))).
thf(tp_c_2EnumRing_2Enum__interp__sp,type,(c_2EnumRing_2Enum__interp__sp:$i)).
thf(mem_c_2EnumRing_2Enum__interp__sp,axiom,(mem@c_2EnumRing_2Enum__interp__sp@(arr@(ty_2Equote_2Evarmap@ty_2Enum_2Enum)@(arr@(ty_2Ecanonical_2Espolynom@ty_2Enum_2Enum)@ty_2Enum_2Enum)))).
thf(stp_fo_c_2EnumRing_2Enum__interp__sp,type,(fo__c_2EnumRing_2Enum__interp__sp:(tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum > (tp__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(stp_eq_fo_c_2EnumRing_2Enum__interp__sp,axiom,( ! [X0:tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum] : ( ! [X1:tp__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ ((fo__c_2EnumRing_2Enum__interp__sp @ X0) @ X1)) = (ap @ (ap @ c_2EnumRing_2Enum__interp__sp @ (inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ X0)) @ (inj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum @ X1)))))).
thf(tp_c_2Ecanonical_2Espolynom__simplify,type,(c_2Ecanonical_2Espolynom__simplify:(del>$i))).
thf(mem_c_2Ecanonical_2Espolynom__simplify,axiom,( ! [A_27a:del] : (mem@(c_2Ecanonical_2Espolynom__simplify@A_27a)@(arr@(ty_2Esemi__ring_2Esemi__ring@A_27a)@(arr@(ty_2Ecanonical_2Espolynom@A_27a)@(ty_2Ecanonical_2Ecanonical__sum@A_27a)))))).
thf(stp_c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum,type,(tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum : $tType)).
thf(stp_inj_c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum,type,(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum : (tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum > $i))).
thf(stp_surj_c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum,type,(surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum : ($i > tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum))).
thf(stp_inj_surj_c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ X)) = X))).
thf(stp_inj_mem_c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : (mem @ (inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ X) @ (ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum)))).
thf(stp_iso_mem_c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum)) => (X = (inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ X)))))).
thf(tp_c_2EnumRing_2Enum__spolynom__simplify,type,(c_2EnumRing_2Enum__spolynom__simplify:$i)).
thf(mem_c_2EnumRing_2Enum__spolynom__simplify,axiom,(mem@c_2EnumRing_2Enum__spolynom__simplify@(arr@(ty_2Ecanonical_2Espolynom@ty_2Enum_2Enum)@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum)))).
thf(tp_c_2Ecanonical_2Espolynom__normalize,type,(c_2Ecanonical_2Espolynom__normalize:(del>$i))).
thf(mem_c_2Ecanonical_2Espolynom__normalize,axiom,( ! [A_27a:del] : (mem@(c_2Ecanonical_2Espolynom__normalize@A_27a)@(arr@(ty_2Esemi__ring_2Esemi__ring@A_27a)@(arr@(ty_2Ecanonical_2Espolynom@A_27a)@(ty_2Ecanonical_2Ecanonical__sum@A_27a)))))).
thf(tp_c_2EnumRing_2Enum__spolynom__normalize,type,(c_2EnumRing_2Enum__spolynom__normalize:$i)).
thf(mem_c_2EnumRing_2Enum__spolynom__normalize,axiom,(mem@c_2EnumRing_2Enum__spolynom__normalize@(arr@(ty_2Ecanonical_2Espolynom@ty_2Enum_2Enum)@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum)))).
thf(tp_c_2Ecanonical_2Einterp__cs,type,(c_2Ecanonical_2Einterp__cs:(del>$i))).
thf(mem_c_2Ecanonical_2Einterp__cs,axiom,( ! [A_27a:del] : (mem@(c_2Ecanonical_2Einterp__cs@A_27a)@(arr@(ty_2Esemi__ring_2Esemi__ring@A_27a)@(arr@(ty_2Equote_2Evarmap@A_27a)@(arr@(ty_2Ecanonical_2Ecanonical__sum@A_27a)@A_27a)))))).
thf(tp_c_2EnumRing_2Enum__interp__cs,type,(c_2EnumRing_2Enum__interp__cs:$i)).
thf(mem_c_2EnumRing_2Enum__interp__cs,axiom,(mem@c_2EnumRing_2Enum__interp__cs@(arr@(ty_2Equote_2Evarmap@ty_2Enum_2Enum)@(arr@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum)@ty_2Enum_2Enum)))).
thf(stp_fo_c_2EnumRing_2Enum__interp__cs,type,(fo__c_2EnumRing_2Enum__interp__cs:(tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum > (tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(stp_eq_fo_c_2EnumRing_2Enum__interp__cs,axiom,( ! [X0:tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum] : ( ! [X1:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ ((fo__c_2EnumRing_2Enum__interp__cs @ X0) @ X1)) = (ap @ (ap @ c_2EnumRing_2Enum__interp__cs @ (inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ X0)) @ (inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ X1)))))).
thf(tp_c_2Ecanonical_2Eics__aux,type,(c_2Ecanonical_2Eics__aux:(del>$i))).
thf(mem_c_2Ecanonical_2Eics__aux,axiom,( ! [A_27a:del] : (mem@(c_2Ecanonical_2Eics__aux@A_27a)@(arr@(ty_2Esemi__ring_2Esemi__ring@A_27a)@(arr@(ty_2Equote_2Evarmap@A_27a)@(arr@A_27a@(arr@(ty_2Ecanonical_2Ecanonical__sum@A_27a)@A_27a))))))).
thf(tp_c_2EnumRing_2Enum__ics__aux,type,(c_2EnumRing_2Enum__ics__aux:$i)).
thf(mem_c_2EnumRing_2Enum__ics__aux,axiom,(mem@c_2EnumRing_2Enum__ics__aux@(arr@(ty_2Equote_2Evarmap@ty_2Enum_2Enum)@(arr@ty_2Enum_2Enum@(arr@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum)@ty_2Enum_2Enum))))).
thf(stp_fo_c_2EnumRing_2Enum__ics__aux,type,(fo__c_2EnumRing_2Enum__ics__aux:(tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > (tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum > tp__ty_2Enum_2Enum))))).
thf(stp_eq_fo_c_2EnumRing_2Enum__ics__aux,axiom,( ! [X0:tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : ( ! [X2:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ (((fo__c_2EnumRing_2Enum__ics__aux @ X0) @ X1) @ X2)) = (ap @ (ap @ (ap @ c_2EnumRing_2Enum__ics__aux @ (inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ X0)) @ (inj__ty_2Enum_2Enum @ X1)) @ (inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ X2))))))).
thf(tp_c_2Ecanonical_2Einterp__m,type,(c_2Ecanonical_2Einterp__m:(del>$i))).
thf(mem_c_2Ecanonical_2Einterp__m,axiom,( ! [A_27a:del] : (mem@(c_2Ecanonical_2Einterp__m@A_27a)@(arr@(ty_2Esemi__ring_2Esemi__ring@A_27a)@(arr@(ty_2Equote_2Evarmap@A_27a)@(arr@A_27a@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@A_27a))))))).
thf(tp_c_2EnumRing_2Enum__interp__m,type,(c_2EnumRing_2Enum__interp__m:$i)).
thf(mem_c_2EnumRing_2Enum__interp__m,axiom,(mem@c_2EnumRing_2Enum__interp__m@(arr@(ty_2Equote_2Evarmap@ty_2Enum_2Enum)@(arr@ty_2Enum_2Enum@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@ty_2Enum_2Enum))))).
thf(stp_fo_c_2EnumRing_2Enum__interp__m,type,(fo__c_2EnumRing_2Enum__interp__m:(tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > (tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex > tp__ty_2Enum_2Enum))))).
thf(stp_eq_fo_c_2EnumRing_2Enum__interp__m,axiom,( ! [X0:tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : ( ! [X2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((inj__ty_2Enum_2Enum @ (((fo__c_2EnumRing_2Enum__interp__m @ X0) @ X1) @ X2)) = (ap @ (ap @ (ap @ c_2EnumRing_2Enum__interp__m @ (inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ X0)) @ (inj__ty_2Enum_2Enum @ X1)) @ (inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ X2))))))).
thf(tp_c_2Ecanonical_2Einterp__vl,type,(c_2Ecanonical_2Einterp__vl:(del>$i))).
thf(mem_c_2Ecanonical_2Einterp__vl,axiom,( ! [A_27a:del] : (mem@(c_2Ecanonical_2Einterp__vl@A_27a)@(arr@(ty_2Esemi__ring_2Esemi__ring@A_27a)@(arr@(ty_2Equote_2Evarmap@A_27a)@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@A_27a)))))).
thf(tp_c_2EnumRing_2Enum__interp__vl,type,(c_2EnumRing_2Enum__interp__vl:$i)).
thf(mem_c_2EnumRing_2Enum__interp__vl,axiom,(mem@c_2EnumRing_2Enum__interp__vl@(arr@(ty_2Equote_2Evarmap@ty_2Enum_2Enum)@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@ty_2Enum_2Enum)))).
thf(stp_fo_c_2EnumRing_2Enum__interp__vl,type,(fo__c_2EnumRing_2Enum__interp__vl:(tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum > (tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex > tp__ty_2Enum_2Enum)))).
thf(stp_eq_fo_c_2EnumRing_2Enum__interp__vl,axiom,( ! [X0:tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum] : ( ! [X1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((inj__ty_2Enum_2Enum @ ((fo__c_2EnumRing_2Enum__interp__vl @ X0) @ X1)) = (ap @ (ap @ c_2EnumRing_2Enum__interp__vl @ (inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ X0)) @ (inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ X1)))))).
thf(tp_c_2Ecanonical_2Eivl__aux,type,(c_2Ecanonical_2Eivl__aux:(del>$i))).
thf(mem_c_2Ecanonical_2Eivl__aux,axiom,( ! [A_27a:del] : (mem@(c_2Ecanonical_2Eivl__aux@A_27a)@(arr@(ty_2Esemi__ring_2Esemi__ring@A_27a)@(arr@(ty_2Equote_2Evarmap@A_27a)@(arr@ty_2Equote_2Eindex@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@A_27a))))))).
thf(tp_c_2EnumRing_2Enum__ivl__aux,type,(c_2EnumRing_2Enum__ivl__aux:$i)).
thf(mem_c_2EnumRing_2Enum__ivl__aux,axiom,(mem@c_2EnumRing_2Enum__ivl__aux@(arr@(ty_2Equote_2Evarmap@ty_2Enum_2Enum)@(arr@ty_2Equote_2Eindex@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@ty_2Enum_2Enum))))).
thf(stp_fo_c_2EnumRing_2Enum__ivl__aux,type,(fo__c_2EnumRing_2Enum__ivl__aux:(tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum > (tp__ty_2Equote_2Eindex > (tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex > tp__ty_2Enum_2Enum))))).
thf(stp_eq_fo_c_2EnumRing_2Enum__ivl__aux,axiom,( ! [X0:tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Equote_2Eindex] : ( ! [X2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((inj__ty_2Enum_2Enum @ (((fo__c_2EnumRing_2Enum__ivl__aux @ X0) @ X1) @ X2)) = (ap @ (ap @ (ap @ c_2EnumRing_2Enum__ivl__aux @ (inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ X0)) @ (inj__ty_2Equote_2Eindex @ X1)) @ (inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ X2))))))).
thf(tp_c_2Ecanonical_2Ecanonical__sum__simplify,type,(c_2Ecanonical_2Ecanonical__sum__simplify:(del>$i))).
thf(mem_c_2Ecanonical_2Ecanonical__sum__simplify,axiom,( ! [A_27a:del] : (mem@(c_2Ecanonical_2Ecanonical__sum__simplify@A_27a)@(arr@(ty_2Esemi__ring_2Esemi__ring@A_27a)@(arr@(ty_2Ecanonical_2Ecanonical__sum@A_27a)@(ty_2Ecanonical_2Ecanonical__sum@A_27a)))))).
thf(tp_c_2EnumRing_2Enum__canonical__sum__simplify,type,(c_2EnumRing_2Enum__canonical__sum__simplify:$i)).
thf(mem_c_2EnumRing_2Enum__canonical__sum__simplify,axiom,(mem@c_2EnumRing_2Enum__canonical__sum__simplify@(arr@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum)@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum)))).
thf(tp_c_2Ecanonical_2Ecanonical__sum__prod,type,(c_2Ecanonical_2Ecanonical__sum__prod:(del>$i))).
thf(mem_c_2Ecanonical_2Ecanonical__sum__prod,axiom,( ! [A_27a:del] : (mem@(c_2Ecanonical_2Ecanonical__sum__prod@A_27a)@(arr@(ty_2Esemi__ring_2Esemi__ring@A_27a)@(arr@(ty_2Ecanonical_2Ecanonical__sum@A_27a)@(arr@(ty_2Ecanonical_2Ecanonical__sum@A_27a)@(ty_2Ecanonical_2Ecanonical__sum@A_27a))))))).
thf(tp_c_2EnumRing_2Enum__canonical__sum__prod,type,(c_2EnumRing_2Enum__canonical__sum__prod:$i)).
thf(mem_c_2EnumRing_2Enum__canonical__sum__prod,axiom,(mem@c_2EnumRing_2Enum__canonical__sum__prod@(arr@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum)@(arr@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum)@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum))))).
thf(tp_c_2Ecanonical_2Ecanonical__sum__scalar3,type,(c_2Ecanonical_2Ecanonical__sum__scalar3:(del>$i))).
thf(mem_c_2Ecanonical_2Ecanonical__sum__scalar3,axiom,( ! [A_27a:del] : (mem@(c_2Ecanonical_2Ecanonical__sum__scalar3@A_27a)@(arr@(ty_2Esemi__ring_2Esemi__ring@A_27a)@(arr@A_27a@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@(arr@(ty_2Ecanonical_2Ecanonical__sum@A_27a)@(ty_2Ecanonical_2Ecanonical__sum@A_27a)))))))).
thf(tp_c_2EnumRing_2Enum__canonical__sum__scalar3,type,(c_2EnumRing_2Enum__canonical__sum__scalar3:$i)).
thf(mem_c_2EnumRing_2Enum__canonical__sum__scalar3,axiom,(mem@c_2EnumRing_2Enum__canonical__sum__scalar3@(arr@ty_2Enum_2Enum@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@(arr@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum)@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum)))))).
thf(tp_c_2Ecanonical_2Ecanonical__sum__scalar2,type,(c_2Ecanonical_2Ecanonical__sum__scalar2:(del>$i))).
thf(mem_c_2Ecanonical_2Ecanonical__sum__scalar2,axiom,( ! [A_27a:del] : (mem@(c_2Ecanonical_2Ecanonical__sum__scalar2@A_27a)@(arr@(ty_2Esemi__ring_2Esemi__ring@A_27a)@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@(arr@(ty_2Ecanonical_2Ecanonical__sum@A_27a)@(ty_2Ecanonical_2Ecanonical__sum@A_27a))))))).
thf(tp_c_2EnumRing_2Enum__canonical__sum__scalar2,type,(c_2EnumRing_2Enum__canonical__sum__scalar2:$i)).
thf(mem_c_2EnumRing_2Enum__canonical__sum__scalar2,axiom,(mem@c_2EnumRing_2Enum__canonical__sum__scalar2@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@(arr@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum)@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum))))).
thf(tp_c_2Ecanonical_2Ecanonical__sum__scalar,type,(c_2Ecanonical_2Ecanonical__sum__scalar:(del>$i))).
thf(mem_c_2Ecanonical_2Ecanonical__sum__scalar,axiom,( ! [A_27a:del] : (mem@(c_2Ecanonical_2Ecanonical__sum__scalar@A_27a)@(arr@(ty_2Esemi__ring_2Esemi__ring@A_27a)@(arr@A_27a@(arr@(ty_2Ecanonical_2Ecanonical__sum@A_27a)@(ty_2Ecanonical_2Ecanonical__sum@A_27a))))))).
thf(tp_c_2EnumRing_2Enum__canonical__sum__scalar,type,(c_2EnumRing_2Enum__canonical__sum__scalar:$i)).
thf(mem_c_2EnumRing_2Enum__canonical__sum__scalar,axiom,(mem@c_2EnumRing_2Enum__canonical__sum__scalar@(arr@ty_2Enum_2Enum@(arr@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum)@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum))))).
thf(tp_c_2Ecanonical_2Evarlist__insert,type,(c_2Ecanonical_2Evarlist__insert:(del>$i))).
thf(mem_c_2Ecanonical_2Evarlist__insert,axiom,( ! [A_27a:del] : (mem@(c_2Ecanonical_2Evarlist__insert@A_27a)@(arr@(ty_2Esemi__ring_2Esemi__ring@A_27a)@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@(arr@(ty_2Ecanonical_2Ecanonical__sum@A_27a)@(ty_2Ecanonical_2Ecanonical__sum@A_27a))))))).
thf(tp_c_2EnumRing_2Enum__varlist__insert,type,(c_2EnumRing_2Enum__varlist__insert:$i)).
thf(mem_c_2EnumRing_2Enum__varlist__insert,axiom,(mem@c_2EnumRing_2Enum__varlist__insert@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@(arr@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum)@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum))))).
thf(tp_c_2Ecanonical_2Emonom__insert,type,(c_2Ecanonical_2Emonom__insert:(del>$i))).
thf(mem_c_2Ecanonical_2Emonom__insert,axiom,( ! [A_27a:del] : (mem@(c_2Ecanonical_2Emonom__insert@A_27a)@(arr@(ty_2Esemi__ring_2Esemi__ring@A_27a)@(arr@A_27a@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@(arr@(ty_2Ecanonical_2Ecanonical__sum@A_27a)@(ty_2Ecanonical_2Ecanonical__sum@A_27a)))))))).
thf(tp_c_2EnumRing_2Enum__monom__insert,type,(c_2EnumRing_2Enum__monom__insert:$i)).
thf(mem_c_2EnumRing_2Enum__monom__insert,axiom,(mem@c_2EnumRing_2Enum__monom__insert@(arr@ty_2Enum_2Enum@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@(arr@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum)@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum)))))).
thf(tp_c_2Earithmetic_2E_2A,type,(c_2Earithmetic_2E_2A:$i)).
thf(mem_c_2Earithmetic_2E_2A,axiom,(mem@c_2Earithmetic_2E_2A@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Earithmetic_2E_2A,type,(fo__c_2Earithmetic_2E_2A:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(stp_eq_fo_c_2Earithmetic_2E_2A,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ ((fo__c_2Earithmetic_2E_2A @ X0) @ X1)) = (ap @ (ap @ c_2Earithmetic_2E_2A @ (inj__ty_2Enum_2Enum @ X0)) @ (inj__ty_2Enum_2Enum @ X1)))))).
thf(tp_c_2Earithmetic_2E_2B,type,(c_2Earithmetic_2E_2B:$i)).
thf(mem_c_2Earithmetic_2E_2B,axiom,(mem@c_2Earithmetic_2E_2B@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Earithmetic_2E_2B,type,(fo__c_2Earithmetic_2E_2B:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(stp_eq_fo_c_2Earithmetic_2E_2B,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ ((fo__c_2Earithmetic_2E_2B @ X0) @ X1)) = (ap @ (ap @ c_2Earithmetic_2E_2B @ (inj__ty_2Enum_2Enum @ X0)) @ (inj__ty_2Enum_2Enum @ X1)))))).
thf(tp_c_2Earithmetic_2EZERO,type,(c_2Earithmetic_2EZERO:$i)).
thf(mem_c_2Earithmetic_2EZERO,axiom,(mem@c_2Earithmetic_2EZERO@ty_2Enum_2Enum)).
thf(stp_fo_c_2Earithmetic_2EZERO,type,(fo__c_2Earithmetic_2EZERO:tp__ty_2Enum_2Enum)).
thf(stp_eq_fo_c_2Earithmetic_2EZERO,axiom,((inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO) = c_2Earithmetic_2EZERO)).
thf(tp_c_2Earithmetic_2EBIT1,type,(c_2Earithmetic_2EBIT1:$i)).
thf(mem_c_2Earithmetic_2EBIT1,axiom,(mem@c_2Earithmetic_2EBIT1@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Earithmetic_2EBIT1,type,(fo__c_2Earithmetic_2EBIT1:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Earithmetic_2EBIT1,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ (fo__c_2Earithmetic_2EBIT1 @ X0)) = (ap @ c_2Earithmetic_2EBIT1 @ (inj__ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Earithmetic_2ENUMERAL,type,(c_2Earithmetic_2ENUMERAL:$i)).
thf(mem_c_2Earithmetic_2ENUMERAL,axiom,(mem@c_2Earithmetic_2ENUMERAL@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Earithmetic_2ENUMERAL,type,(fo__c_2Earithmetic_2ENUMERAL:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Earithmetic_2ENUMERAL,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ (fo__c_2Earithmetic_2ENUMERAL @ X0)) = (ap @ c_2Earithmetic_2ENUMERAL @ (inj__ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Enum_2E0,type,(c_2Enum_2E0:$i)).
thf(mem_c_2Enum_2E0,axiom,(mem@c_2Enum_2E0@ty_2Enum_2Enum)).
thf(stp_fo_c_2Enum_2E0,type,(fo__c_2Enum_2E0:tp__ty_2Enum_2Enum)).
thf(stp_eq_fo_c_2Enum_2E0,axiom,((inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0) = c_2Enum_2E0)).
thf(tp_c_2Ecanonical_2Ecanonical__sum__merge,type,(c_2Ecanonical_2Ecanonical__sum__merge:(del>$i))).
thf(mem_c_2Ecanonical_2Ecanonical__sum__merge,axiom,( ! [A_27a:del] : (mem@(c_2Ecanonical_2Ecanonical__sum__merge@A_27a)@(arr@(ty_2Esemi__ring_2Esemi__ring@A_27a)@(arr@(ty_2Ecanonical_2Ecanonical__sum@A_27a)@(arr@(ty_2Ecanonical_2Ecanonical__sum@A_27a)@(ty_2Ecanonical_2Ecanonical__sum@A_27a))))))).
thf(tp_c_2EnumRing_2Enum__canonical__sum__merge,type,(c_2EnumRing_2Enum__canonical__sum__merge:$i)).
thf(mem_c_2EnumRing_2Enum__canonical__sum__merge,axiom,(mem@c_2EnumRing_2Enum__canonical__sum__merge@(arr@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum)@(arr@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum)@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum))))).
thf(tp_c_2Ebool_2ET,type,(c_2Ebool_2ET:$i)).
thf(mem_c_2Ebool_2ET,axiom,(mem@c_2Ebool_2ET@bool)).
thf(ax_true_p,axiom,(p@c_2Ebool_2ET)).
thf(tp_c_2Emin_2E_40,type,(c_2Emin_2E_40:(del>$i))).
thf(mem_c_2Emin_2E_40,axiom,( ! [A_27a:del] : (mem@(c_2Emin_2E_40@A_27a)@(arr@(arr@A_27a@bool)@A_27a)))).
thf(tp_c_2Equote_2EEmpty__vm,type,(c_2Equote_2EEmpty__vm:(del>$i))).
thf(mem_c_2Equote_2EEmpty__vm,axiom,( ! [A_27a:del] : (mem@(c_2Equote_2EEmpty__vm@A_27a)@(ty_2Equote_2Evarmap@A_27a)))).
thf(tp_c_2Equote_2ELeft__idx,type,(c_2Equote_2ELeft__idx:$i)).
thf(mem_c_2Equote_2ELeft__idx,axiom,(mem@c_2Equote_2ELeft__idx@(arr@ty_2Equote_2Eindex@ty_2Equote_2Eindex))).
thf(stp_fo_c_2Equote_2ELeft__idx,type,(fo__c_2Equote_2ELeft__idx:(tp__ty_2Equote_2Eindex > tp__ty_2Equote_2Eindex))).
thf(stp_eq_fo_c_2Equote_2ELeft__idx,axiom,( ! [X0:tp__ty_2Equote_2Eindex] : ((inj__ty_2Equote_2Eindex @ (fo__c_2Equote_2ELeft__idx @ X0)) = (ap @ c_2Equote_2ELeft__idx @ (inj__ty_2Equote_2Eindex @ X0))))).
thf(tp_c_2Equote_2ERight__idx,type,(c_2Equote_2ERight__idx:$i)).
thf(mem_c_2Equote_2ERight__idx,axiom,(mem@c_2Equote_2ERight__idx@(arr@ty_2Equote_2Eindex@ty_2Equote_2Eindex))).
thf(stp_fo_c_2Equote_2ERight__idx,type,(fo__c_2Equote_2ERight__idx:(tp__ty_2Equote_2Eindex > tp__ty_2Equote_2Eindex))).
thf(stp_eq_fo_c_2Equote_2ERight__idx,axiom,( ! [X0:tp__ty_2Equote_2Eindex] : ((inj__ty_2Equote_2Eindex @ (fo__c_2Equote_2ERight__idx @ X0)) = (ap @ c_2Equote_2ERight__idx @ (inj__ty_2Equote_2Eindex @ X0))))).
thf(tp_c_2Equote_2ENode__vm,type,(c_2Equote_2ENode__vm:(del>$i))).
thf(mem_c_2Equote_2ENode__vm,axiom,( ! [A_27a:del] : (mem@(c_2Equote_2ENode__vm@A_27a)@(arr@A_27a@(arr@(ty_2Equote_2Evarmap@A_27a)@(arr@(ty_2Equote_2Evarmap@A_27a)@(ty_2Equote_2Evarmap@A_27a))))))).
thf(tp_c_2Equote_2EEnd__idx,type,(c_2Equote_2EEnd__idx:$i)).
thf(mem_c_2Equote_2EEnd__idx,axiom,(mem@c_2Equote_2EEnd__idx@ty_2Equote_2Eindex)).
thf(stp_fo_c_2Equote_2EEnd__idx,type,(fo__c_2Equote_2EEnd__idx:tp__ty_2Equote_2Eindex)).
thf(stp_eq_fo_c_2Equote_2EEnd__idx,axiom,((inj__ty_2Equote_2Eindex @ fo__c_2Equote_2EEnd__idx) = c_2Equote_2EEnd__idx)).
thf(tp_c_2Equote_2Evarmap__find,type,(c_2Equote_2Evarmap__find:(del>$i))).
thf(mem_c_2Equote_2Evarmap__find,axiom,( ! [A_27a:del] : (mem@(c_2Equote_2Evarmap__find@A_27a)@(arr@ty_2Equote_2Eindex@(arr@(ty_2Equote_2Evarmap@A_27a)@A_27a))))).
thf(tp_c_2Esemi__ring_2Esemi__ring__SRM,type,(c_2Esemi__ring_2Esemi__ring__SRM:(del>$i))).
thf(mem_c_2Esemi__ring_2Esemi__ring__SRM,axiom,( ! [A_27a:del] : (mem@(c_2Esemi__ring_2Esemi__ring__SRM@A_27a)@(arr@(ty_2Esemi__ring_2Esemi__ring@A_27a)@(arr@A_27a@(arr@A_27a@A_27a)))))).
thf(tp_c_2Esemi__ring_2Esemi__ring__SRP,type,(c_2Esemi__ring_2Esemi__ring__SRP:(del>$i))).
thf(mem_c_2Esemi__ring_2Esemi__ring__SRP,axiom,( ! [A_27a:del] : (mem@(c_2Esemi__ring_2Esemi__ring__SRP@A_27a)@(arr@(ty_2Esemi__ring_2Esemi__ring@A_27a)@(arr@A_27a@(arr@A_27a@A_27a)))))).
thf(tp_c_2Esemi__ring_2Esemi__ring__SR1,type,(c_2Esemi__ring_2Esemi__ring__SR1:(del>$i))).
thf(mem_c_2Esemi__ring_2Esemi__ring__SR1,axiom,( ! [A_27a:del] : (mem@(c_2Esemi__ring_2Esemi__ring__SR1@A_27a)@(arr@(ty_2Esemi__ring_2Esemi__ring@A_27a)@A_27a)))).
thf(tp_c_2Esemi__ring_2Erecordtype_2Esemi__ring,type,(c_2Esemi__ring_2Erecordtype_2Esemi__ring:(del>$i))).
thf(mem_c_2Esemi__ring_2Erecordtype_2Esemi__ring,axiom,( ! [A_27a:del] : (mem@(c_2Esemi__ring_2Erecordtype_2Esemi__ring@A_27a)@(arr@A_27a@(arr@A_27a@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(ty_2Esemi__ring_2Esemi__ring@A_27a)))))))).
thf(tp_c_2Esemi__ring_2Esemi__ring__SR0,type,(c_2Esemi__ring_2Esemi__ring__SR0:(del>$i))).
thf(mem_c_2Esemi__ring_2Esemi__ring__SR0,axiom,( ! [A_27a:del] : (mem@(c_2Esemi__ring_2Esemi__ring__SR0@A_27a)@(arr@(ty_2Esemi__ring_2Esemi__ring@A_27a)@A_27a)))).
thf(tp_c_2Emin_2E_3D,type,(c_2Emin_2E_3D:(del>$i))).
thf(mem_c_2Emin_2E_3D,axiom,( ! [A_27a:del] : (mem@(c_2Emin_2E_3D@A_27a)@(arr@A_27a@(arr@A_27a@bool))))).
thf(ax_eq_p,axiom,( ! [A:del] : ( ! [X:$i] : ((mem@X@A) => ( ! [Y:$i] : ((mem@Y@A) => ((p@(ap@(ap@(c_2Emin_2E_3D@A)@X)@Y)) <=> (X = Y)))))))).
thf(tp_c_2Ebool_2E_21,type,(c_2Ebool_2E_21:(del>$i))).
thf(mem_c_2Ebool_2E_21,axiom,( ! [A_27a:del] : (mem@(c_2Ebool_2E_21@A_27a)@(arr@(arr@A_27a@bool)@bool)))).
thf(ax_all_p,axiom,( ! [A:del] : ( ! [Q:$i] : ((mem@Q@(arr@A@bool)) => ((p@(ap@(c_2Ebool_2E_21@A)@Q)) <=> ( ! [X:$i] : ((mem@X@A) => (p@(ap@Q@X))))))))).
thf(tp_c_2Ebool_2E_2F_5C,type,(c_2Ebool_2E_2F_5C:$i)).
thf(mem_c_2Ebool_2E_2F_5C,axiom,(mem@c_2Ebool_2E_2F_5C@(arr@bool@(arr@bool@bool)))).
thf(ax_and_p,axiom,( ! [Q:$i] : ((mem@Q@bool) => ( ! [R:$i] : ((mem@R@bool) => ((p@(ap@(ap@c_2Ebool_2E_2F_5C@Q)@R)) <=> ((p@Q) & (p@R)))))))).
thf(conj_thm_2Ebool_2EEQ__SYM__EQ,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ((V0x = V1y) <=> (V1y = V0x)))))))).
thf(conj_thm_2Ecanonical_2Ecanonical__sum__merge__def,lemma,( ! [A_27a:del]: (( ! [V0t2:$i] : ((mem@V0t2@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V1t1:$i] : ((mem@V1t1@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V2sr:$i] : ((mem@V2sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V3l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V4l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V5c2:$i] : ((mem@V5c2@A_27a) => ( ! [V6c1:$i] : ((mem@V6c1@A_27a) => ((ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__merge@A_27a)@V2sr)@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V6c1)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V4l1))@V1t1))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V5c2)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l2))@V0t2)) = (ap@(ap@(ap@(ap@(c_2EternaryComparisons_2Eordering__CASE@(ty_2Ecanonical_2Ecanonical__sum@A_27a))@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__compare@ty_2Equote_2Eindex@ty_2Equote_2Eindex)@c_2Equote_2Eindex__compare)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V4l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V6c1)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V4l1))@(ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__merge@A_27a)@V2sr)@V1t1)@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V5c2)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l2))@V0t2))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@(ap@(ap@(ap@(c_2Esemi__ring_2Esemi__ring__SRP@A_27a)@V2sr)@V6c1)@V5c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V4l1))@(ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__merge@A_27a)@V2sr)@V1t1)@V0t2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V5c2)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l2))@(ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__merge@A_27a)@V2sr)@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V6c1)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V4l1))@V1t1))@V0t2)))))))))))))))) & (( ! [V7t2:$i] : ((mem@V7t2@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V8t1:$i] : ((mem@V8t1@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V9sr:$i] : ((mem@V9sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V10l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V11l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V12c1:$i] : ((mem@V12c1@A_27a) => ((ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__merge@A_27a)@V9sr)@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V12c1)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V11l1))@V8t1))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V10l2))@V7t2)) = (ap@(ap@(ap@(ap@(c_2EternaryComparisons_2Eordering__CASE@(ty_2Ecanonical_2Ecanonical__sum@A_27a))@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__compare@ty_2Equote_2Eindex@ty_2Equote_2Eindex)@c_2Equote_2Eindex__compare)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V11l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V10l2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V12c1)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V11l1))@(ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__merge@A_27a)@V9sr)@V8t1)@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V10l2))@V7t2))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@(ap@(ap@(ap@(c_2Esemi__ring_2Esemi__ring__SRP@A_27a)@V9sr)@V12c1)@(ap@(c_2Esemi__ring_2Esemi__ring__SR1@A_27a)@V9sr)))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V11l1))@(ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__merge@A_27a)@V9sr)@V8t1)@V7t2)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V10l2))@(ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__merge@A_27a)@V9sr)@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V12c1)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V11l1))@V8t1))@V7t2)))))))))))))) & (( ! [V13t2:$i] : ((mem@V13t2@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V14t1:$i] : ((mem@V14t1@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V15sr:$i] : ((mem@V15sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V16l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V17l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V18c2:$i] : ((mem@V18c2@A_27a) => ((ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__merge@A_27a)@V15sr)@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V17l1))@V14t1))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V18c2)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V16l2))@V13t2)) = (ap@(ap@(ap@(ap@(c_2EternaryComparisons_2Eordering__CASE@(ty_2Ecanonical_2Ecanonical__sum@A_27a))@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__compare@ty_2Equote_2Eindex@ty_2Equote_2Eindex)@c_2Equote_2Eindex__compare)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V17l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V16l2)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V17l1))@(ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__merge@A_27a)@V15sr)@V14t1)@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V18c2)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V16l2))@V13t2))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@(ap@(ap@(ap@(c_2Esemi__ring_2Esemi__ring__SRP@A_27a)@V15sr)@(ap@(c_2Esemi__ring_2Esemi__ring__SR1@A_27a)@V15sr))@V18c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V17l1))@(ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__merge@A_27a)@V15sr)@V14t1)@V13t2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V18c2)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V16l2))@(ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__merge@A_27a)@V15sr)@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V17l1))@V14t1))@V13t2)))))))))))))) & (( ! [V19t2:$i] : ((mem@V19t2@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V20t1:$i] : ((mem@V20t1@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V21sr:$i] : ((mem@V21sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V22l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V23l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__merge@A_27a)@V21sr)@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V23l1))@V20t1))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V22l2))@V19t2)) = (ap@(ap@(ap@(ap@(c_2EternaryComparisons_2Eordering__CASE@(ty_2Ecanonical_2Ecanonical__sum@A_27a))@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__compare@ty_2Equote_2Eindex@ty_2Equote_2Eindex)@c_2Equote_2Eindex__compare)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V23l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V22l2)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V23l1))@(ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__merge@A_27a)@V21sr)@V20t1)@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V22l2))@V19t2))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@(ap@(ap@(ap@(c_2Esemi__ring_2Esemi__ring__SRP@A_27a)@V21sr)@(ap@(c_2Esemi__ring_2Esemi__ring__SR1@A_27a)@V21sr))@(ap@(c_2Esemi__ring_2Esemi__ring__SR1@A_27a)@V21sr)))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V23l1))@(ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__merge@A_27a)@V21sr)@V20t1)@V19t2)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V22l2))@(ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__merge@A_27a)@V21sr)@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V23l1))@V20t1))@V19t2)))))))))))) & (( ! [V24sr:$i] : ((mem@V24sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V25s1:$i] : ((mem@V25s1@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ((ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__merge@A_27a)@V24sr)@V25s1)@(c_2Ecanonical_2ENil__monom@A_27a)) = V25s1))))) & (( ! [V26v6:$i] : ((mem@V26v6@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V27v5:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V28v4:$i] : ((mem@V28v4@A_27a) => ( ! [V29sr:$i] : ((mem@V29sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ((ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__merge@A_27a)@V29sr)@(c_2Ecanonical_2ENil__monom@A_27a))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V28v4)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V27v5))@V26v6)) = (ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V28v4)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V27v5))@V26v6))))))))) & ( ! [V30v8:$i] : ((mem@V30v8@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V31v7:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V32sr:$i] : ((mem@V32sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ((ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__merge@A_27a)@V32sr)@(c_2Ecanonical_2ENil__monom@A_27a))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V31v7))@V30v8)) = (ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V31v7))@V30v8))))))))))))))).
thf(conj_thm_2Ecanonical_2Emonom__insert__def,lemma,( ! [A_27a:del]: (( ! [V0t2:$i] : ((mem@V0t2@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V1sr:$i] : ((mem@V1sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V2l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V3l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V4c2:$i] : ((mem@V4c2@A_27a) => ( ! [V5c1:$i] : ((mem@V5c1@A_27a) => ((ap@(ap@(ap@(ap@(c_2Ecanonical_2Emonom__insert@A_27a)@V1sr)@V5c1)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l1))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V4c2)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V2l2))@V0t2)) = (ap@(ap@(ap@(ap@(c_2EternaryComparisons_2Eordering__CASE@(ty_2Ecanonical_2Ecanonical__sum@A_27a))@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__compare@ty_2Equote_2Eindex@ty_2Equote_2Eindex)@c_2Equote_2Eindex__compare)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V2l2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V5c1)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l1))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V4c2)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V2l2))@V0t2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@(ap@(ap@(ap@(c_2Esemi__ring_2Esemi__ring__SRP@A_27a)@V1sr)@V5c1)@V4c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l1))@V0t2))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V4c2)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V2l2))@(ap@(ap@(ap@(ap@(c_2Ecanonical_2Emonom__insert@A_27a)@V1sr)@V5c1)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l1))@V0t2)))))))))))))) & (( ! [V6t2:$i] : ((mem@V6t2@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V7sr:$i] : ((mem@V7sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V8l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V9l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V10c1:$i] : ((mem@V10c1@A_27a) => ((ap@(ap@(ap@(ap@(c_2Ecanonical_2Emonom__insert@A_27a)@V7sr)@V10c1)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V9l1))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V8l2))@V6t2)) = (ap@(ap@(ap@(ap@(c_2EternaryComparisons_2Eordering__CASE@(ty_2Ecanonical_2Ecanonical__sum@A_27a))@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__compare@ty_2Equote_2Eindex@ty_2Equote_2Eindex)@c_2Equote_2Eindex__compare)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V9l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V8l2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V10c1)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V9l1))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V8l2))@V6t2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@(ap@(ap@(ap@(c_2Esemi__ring_2Esemi__ring__SRP@A_27a)@V7sr)@V10c1)@(ap@(c_2Esemi__ring_2Esemi__ring__SR1@A_27a)@V7sr)))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V9l1))@V6t2))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V8l2))@(ap@(ap@(ap@(ap@(c_2Ecanonical_2Emonom__insert@A_27a)@V7sr)@V10c1)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V9l1))@V6t2)))))))))))) & ( ! [V11sr:$i] : ((mem@V11sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V12l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V13c1:$i] : ((mem@V13c1@A_27a) => ((ap@(ap@(ap@(ap@(c_2Ecanonical_2Emonom__insert@A_27a)@V11sr)@V13c1)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V12l1))@(c_2Ecanonical_2ENil__monom@A_27a)) = (ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V13c1)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V12l1))@(c_2Ecanonical_2ENil__monom@A_27a)))))))))))).
thf(conj_thm_2Ecanonical_2Evarlist__insert__def,lemma,( ! [A_27a:del]: (( ! [V0t2:$i] : ((mem@V0t2@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V1sr:$i] : ((mem@V1sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V2l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V3l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V4c2:$i] : ((mem@V4c2@A_27a) => ((ap@(ap@(ap@(c_2Ecanonical_2Evarlist__insert@A_27a)@V1sr)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l1))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V4c2)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V2l2))@V0t2)) = (ap@(ap@(ap@(ap@(c_2EternaryComparisons_2Eordering__CASE@(ty_2Ecanonical_2Ecanonical__sum@A_27a))@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__compare@ty_2Equote_2Eindex@ty_2Equote_2Eindex)@c_2Equote_2Eindex__compare)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V2l2)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l1))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V4c2)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V2l2))@V0t2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@(ap@(ap@(ap@(c_2Esemi__ring_2Esemi__ring__SRP@A_27a)@V1sr)@(ap@(c_2Esemi__ring_2Esemi__ring__SR1@A_27a)@V1sr))@V4c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l1))@V0t2))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V4c2)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V2l2))@(ap@(ap@(ap@(c_2Ecanonical_2Evarlist__insert@A_27a)@V1sr)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l1))@V0t2)))))))))))) & (( ! [V5t2:$i] : ((mem@V5t2@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V6sr:$i] : ((mem@V6sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V7l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V8l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((ap@(ap@(ap@(c_2Ecanonical_2Evarlist__insert@A_27a)@V6sr)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V8l1))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V7l2))@V5t2)) = (ap@(ap@(ap@(ap@(c_2EternaryComparisons_2Eordering__CASE@(ty_2Ecanonical_2Ecanonical__sum@A_27a))@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__compare@ty_2Equote_2Eindex@ty_2Equote_2Eindex)@c_2Equote_2Eindex__compare)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V8l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V7l2)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V8l1))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V7l2))@V5t2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@(ap@(ap@(ap@(c_2Esemi__ring_2Esemi__ring__SRP@A_27a)@V6sr)@(ap@(c_2Esemi__ring_2Esemi__ring__SR1@A_27a)@V6sr))@(ap@(c_2Esemi__ring_2Esemi__ring__SR1@A_27a)@V6sr)))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V8l1))@V5t2))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V7l2))@(ap@(ap@(ap@(c_2Ecanonical_2Evarlist__insert@A_27a)@V6sr)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V8l1))@V5t2)))))))))) & ( ! [V9sr:$i] : ((mem@V9sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V10l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((ap@(ap@(ap@(c_2Ecanonical_2Evarlist__insert@A_27a)@V9sr)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V10l1))@(c_2Ecanonical_2ENil__monom@A_27a)) = (ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V10l1))@(c_2Ecanonical_2ENil__monom@A_27a)))))))))).
thf(ax_thm_2Ecanonical_2Ecanonical__sum__scalar__def,axiom,( ! [A_27a:del]: (( ! [V0sr:$i] : ((mem@V0sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V1c0:$i] : ((mem@V1c0@A_27a) => ( ! [V2c:$i] : ((mem@V2c@A_27a) => ( ! [V3l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V4t:$i] : ((mem@V4t@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ((ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__scalar@A_27a)@V0sr)@V1c0)@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V2c)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l))@V4t)) = (ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@(ap@(ap@(ap@(c_2Esemi__ring_2Esemi__ring__SRM@A_27a)@V0sr)@V1c0)@V2c))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l))@(ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__scalar@A_27a)@V0sr)@V1c0)@V4t)))))))))))) & (( ! [V5sr:$i] : ((mem@V5sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V6c0:$i] : ((mem@V6c0@A_27a) => ( ! [V7l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V8t:$i] : ((mem@V8t@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ((ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__scalar@A_27a)@V5sr)@V6c0)@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V7l))@V8t)) = (ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V6c0)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V7l))@(ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__scalar@A_27a)@V5sr)@V6c0)@V8t)))))))))) & ( ! [V9sr:$i] : ((mem@V9sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V10c0:$i] : ((mem@V10c0@A_27a) => ((ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__scalar@A_27a)@V9sr)@V10c0)@(c_2Ecanonical_2ENil__monom@A_27a)) = (c_2Ecanonical_2ENil__monom@A_27a)))))))))).
thf(ax_thm_2Ecanonical_2Ecanonical__sum__scalar2__def,axiom,( ! [A_27a:del]: (( ! [V0sr:$i] : ((mem@V0sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V1l0:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V2c:$i] : ((mem@V2c@A_27a) => ( ! [V3l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V4t:$i] : ((mem@V4t@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ((ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__scalar2@A_27a)@V0sr)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V1l0))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V2c)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l))@V4t)) = (ap@(ap@(ap@(ap@(c_2Ecanonical_2Emonom__insert@A_27a)@V0sr)@V2c)@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__merge@ty_2Equote_2Eindex)@c_2Equote_2Eindex__lt)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V1l0))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l)))@(ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__scalar2@A_27a)@V0sr)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V1l0))@V4t))))))))))) & (( ! [V5sr:$i] : ((mem@V5sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V6l0:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V7l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V8t:$i] : ((mem@V8t@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ((ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__scalar2@A_27a)@V5sr)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V6l0))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V7l))@V8t)) = (ap@(ap@(ap@(c_2Ecanonical_2Evarlist__insert@A_27a)@V5sr)@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__merge@ty_2Equote_2Eindex)@c_2Equote_2Eindex__lt)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V6l0))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V7l)))@(ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__scalar2@A_27a)@V5sr)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V6l0))@V8t))))))))) & ( ! [V9sr:$i] : ((mem@V9sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V10l0:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__scalar2@A_27a)@V9sr)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V10l0))@(c_2Ecanonical_2ENil__monom@A_27a)) = (c_2Ecanonical_2ENil__monom@A_27a))))))))).
thf(ax_thm_2Ecanonical_2Ecanonical__sum__scalar3__def,axiom,( ! [A_27a:del]: (( ! [V0sr:$i] : ((mem@V0sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V1c0:$i] : ((mem@V1c0@A_27a) => ( ! [V2l0:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V3c:$i] : ((mem@V3c@A_27a) => ( ! [V4l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V5t:$i] : ((mem@V5t@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ((ap@(ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__scalar3@A_27a)@V0sr)@V1c0)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V2l0))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V3c)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V4l))@V5t)) = (ap@(ap@(ap@(ap@(c_2Ecanonical_2Emonom__insert@A_27a)@V0sr)@(ap@(ap@(ap@(c_2Esemi__ring_2Esemi__ring__SRM@A_27a)@V0sr)@V1c0)@V3c))@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__merge@ty_2Equote_2Eindex)@c_2Equote_2Eindex__lt)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V2l0))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V4l)))@(ap@(ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__scalar3@A_27a)@V0sr)@V1c0)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V2l0))@V5t))))))))))))) & (( ! [V6sr:$i] : ((mem@V6sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V7c0:$i] : ((mem@V7c0@A_27a) => ( ! [V8l0:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V9l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V10t:$i] : ((mem@V10t@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ((ap@(ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__scalar3@A_27a)@V6sr)@V7c0)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V8l0))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V9l))@V10t)) = (ap@(ap@(ap@(ap@(c_2Ecanonical_2Emonom__insert@A_27a)@V6sr)@V7c0)@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__merge@ty_2Equote_2Eindex)@c_2Equote_2Eindex__lt)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V8l0))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V9l)))@(ap@(ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__scalar3@A_27a)@V6sr)@V7c0)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V8l0))@V10t))))))))))) & ( ! [V11sr:$i] : ((mem@V11sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V12c0:$i] : ((mem@V12c0@A_27a) => ( ! [V13l0:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((ap@(ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__scalar3@A_27a)@V11sr)@V12c0)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V13l0))@(c_2Ecanonical_2ENil__monom@A_27a)) = (c_2Ecanonical_2ENil__monom@A_27a))))))))))).
thf(ax_thm_2Ecanonical_2Ecanonical__sum__prod__def,axiom,( ! [A_27a:del]: (( ! [V0sr:$i] : ((mem@V0sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V1c1:$i] : ((mem@V1c1@A_27a) => ( ! [V2l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V3t1:$i] : ((mem@V3t1@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V4s2:$i] : ((mem@V4s2@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ((ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__prod@A_27a)@V0sr)@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V1c1)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V2l1))@V3t1))@V4s2) = (ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__merge@A_27a)@V0sr)@(ap@(ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__scalar3@A_27a)@V0sr)@V1c1)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V2l1))@V4s2))@(ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__prod@A_27a)@V0sr)@V3t1)@V4s2)))))))))))) & (( ! [V5sr:$i] : ((mem@V5sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V6l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V7t1:$i] : ((mem@V7t1@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V8s2:$i] : ((mem@V8s2@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ((ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__prod@A_27a)@V5sr)@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V6l1))@V7t1))@V8s2) = (ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__merge@A_27a)@V5sr)@(ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__scalar2@A_27a)@V5sr)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V6l1))@V8s2))@(ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__prod@A_27a)@V5sr)@V7t1)@V8s2)))))))))) & ( ! [V9sr:$i] : ((mem@V9sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V10s2:$i] : ((mem@V10s2@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ((ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__prod@A_27a)@V9sr)@(c_2Ecanonical_2ENil__monom@A_27a))@V10s2) = (c_2Ecanonical_2ENil__monom@A_27a)))))))))).
thf(ax_thm_2Ecanonical_2Ecanonical__sum__simplify__def,axiom,( ! [A_27a:del]: (( ! [V0sr:$i] : ((mem@V0sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V1c:$i] : ((mem@V1c@A_27a) => ( ! [V2l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V3t:$i] : ((mem@V3t@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ((ap@(ap@(c_2Ecanonical_2Ecanonical__sum__simplify@A_27a)@V0sr)@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V1c)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V2l))@V3t)) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Ecanonical_2Ecanonical__sum@A_27a))@(ap@(ap@(c_2Emin_2E_3D@A_27a)@V1c)@(ap@(c_2Esemi__ring_2Esemi__ring__SR0@A_27a)@V0sr)))@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__simplify@A_27a)@V0sr)@V3t))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Ecanonical_2Ecanonical__sum@A_27a))@(ap@(ap@(c_2Emin_2E_3D@A_27a)@V1c)@(ap@(c_2Esemi__ring_2Esemi__ring__SR1@A_27a)@V0sr)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V2l))@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__simplify@A_27a)@V0sr)@V3t)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V1c)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V2l))@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__simplify@A_27a)@V0sr)@V3t)))))))))))) & (( ! [V4sr:$i] : ((mem@V4sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V5l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V6t:$i] : ((mem@V6t@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ((ap@(ap@(c_2Ecanonical_2Ecanonical__sum__simplify@A_27a)@V4sr)@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V5l))@V6t)) = (ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V5l))@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__simplify@A_27a)@V4sr)@V6t)))))))) & ( ! [V7sr:$i] : ((mem@V7sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ((ap@(ap@(c_2Ecanonical_2Ecanonical__sum__simplify@A_27a)@V7sr)@(c_2Ecanonical_2ENil__monom@A_27a)) = (c_2Ecanonical_2ENil__monom@A_27a)))))))).
thf(ax_thm_2Ecanonical_2Eivl__aux__def,axiom,( ! [A_27a:del]: (( ! [V0sr:$i] : ((mem@V0sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V1vm:$i] : ((mem@V1vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V2x:tp__ty_2Equote_2Eindex] : ((ap@(ap@(ap@(ap@(c_2Ecanonical_2Eivl__aux@A_27a)@V0sr)@V1vm)@(inj__ty_2Equote_2Eindex @ V2x))@(c_2Elist_2ENIL@ty_2Equote_2Eindex)) = (ap@(ap@(c_2Equote_2Evarmap__find@A_27a)@(inj__ty_2Equote_2Eindex @ V2x))@V1vm))))))) & ( ! [V3sr:$i] : ((mem@V3sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V4vm:$i] : ((mem@V4vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V5x:tp__ty_2Equote_2Eindex] : ( ! [V6x_27:tp__ty_2Equote_2Eindex] : ( ! [V7t_27:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((ap@(ap@(ap@(ap@(c_2Ecanonical_2Eivl__aux@A_27a)@V3sr)@V4vm)@(inj__ty_2Equote_2Eindex @ V5x))@(ap@(ap@(c_2Elist_2ECONS@ty_2Equote_2Eindex)@(inj__ty_2Equote_2Eindex @ V6x_27))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V7t_27))) = (ap@(ap@(ap@(c_2Esemi__ring_2Esemi__ring__SRM@A_27a)@V3sr)@(ap@(ap@(c_2Equote_2Evarmap__find@A_27a)@(inj__ty_2Equote_2Eindex @ V5x))@V4vm))@(ap@(ap@(ap@(ap@(c_2Ecanonical_2Eivl__aux@A_27a)@V3sr)@V4vm)@(inj__ty_2Equote_2Eindex @ V6x_27))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V7t_27)))))))))))))).
thf(ax_thm_2Ecanonical_2Einterp__vl__def,axiom,( ! [A_27a:del]: (( ! [V0sr:$i] : ((mem@V0sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V1vm:$i] : ((mem@V1vm@(ty_2Equote_2Evarmap@A_27a)) => ((ap@(ap@(ap@(c_2Ecanonical_2Einterp__vl@A_27a)@V0sr)@V1vm)@(c_2Elist_2ENIL@ty_2Equote_2Eindex)) = (ap@(c_2Esemi__ring_2Esemi__ring__SR1@A_27a)@V0sr)))))) & ( ! [V2sr:$i] : ((mem@V2sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V3vm:$i] : ((mem@V3vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V4x:tp__ty_2Equote_2Eindex] : ( ! [V5t:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((ap@(ap@(ap@(c_2Ecanonical_2Einterp__vl@A_27a)@V2sr)@V3vm)@(ap@(ap@(c_2Elist_2ECONS@ty_2Equote_2Eindex)@(inj__ty_2Equote_2Eindex @ V4x))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V5t))) = (ap@(ap@(ap@(ap@(c_2Ecanonical_2Eivl__aux@A_27a)@V2sr)@V3vm)@(inj__ty_2Equote_2Eindex @ V4x))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V5t)))))))))))).
thf(ax_thm_2Ecanonical_2Einterp__m__def,axiom,( ! [A_27a:del]: (( ! [V0sr:$i] : ((mem@V0sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V1vm:$i] : ((mem@V1vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V2c:$i] : ((mem@V2c@A_27a) => ((ap@(ap@(ap@(ap@(c_2Ecanonical_2Einterp__m@A_27a)@V0sr)@V1vm)@V2c)@(c_2Elist_2ENIL@ty_2Equote_2Eindex)) = V2c))))))) & ( ! [V3sr:$i] : ((mem@V3sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V4vm:$i] : ((mem@V4vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V5c:$i] : ((mem@V5c@A_27a) => ( ! [V6x:tp__ty_2Equote_2Eindex] : ( ! [V7t:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((ap@(ap@(ap@(ap@(c_2Ecanonical_2Einterp__m@A_27a)@V3sr)@V4vm)@V5c)@(ap@(ap@(c_2Elist_2ECONS@ty_2Equote_2Eindex)@(inj__ty_2Equote_2Eindex @ V6x))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V7t))) = (ap@(ap@(ap@(c_2Esemi__ring_2Esemi__ring__SRM@A_27a)@V3sr)@V5c)@(ap@(ap@(ap@(ap@(c_2Ecanonical_2Eivl__aux@A_27a)@V3sr)@V4vm)@(inj__ty_2Equote_2Eindex @ V6x))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V7t))))))))))))))).
thf(ax_thm_2Ecanonical_2Eics__aux__def,axiom,( ! [A_27a:del]: (( ! [V0sr:$i] : ((mem@V0sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V1vm:$i] : ((mem@V1vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V2a:$i] : ((mem@V2a@A_27a) => ((ap@(ap@(ap@(ap@(c_2Ecanonical_2Eics__aux@A_27a)@V0sr)@V1vm)@V2a)@(c_2Ecanonical_2ENil__monom@A_27a)) = V2a))))))) & (( ! [V3sr:$i] : ((mem@V3sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V4vm:$i] : ((mem@V4vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V5a:$i] : ((mem@V5a@A_27a) => ( ! [V6l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V7t:$i] : ((mem@V7t@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ((ap@(ap@(ap@(ap@(c_2Ecanonical_2Eics__aux@A_27a)@V3sr)@V4vm)@V5a)@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V6l))@V7t)) = (ap@(ap@(ap@(c_2Esemi__ring_2Esemi__ring__SRP@A_27a)@V3sr)@V5a)@(ap@(ap@(ap@(ap@(c_2Ecanonical_2Eics__aux@A_27a)@V3sr)@V4vm)@(ap@(ap@(ap@(c_2Ecanonical_2Einterp__vl@A_27a)@V3sr)@V4vm)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V6l)))@V7t)))))))))))) & ( ! [V8sr:$i] : ((mem@V8sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V9vm:$i] : ((mem@V9vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V10a:$i] : ((mem@V10a@A_27a) => ( ! [V11c:$i] : ((mem@V11c@A_27a) => ( ! [V12l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V13t:$i] : ((mem@V13t@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ((ap@(ap@(ap@(ap@(c_2Ecanonical_2Eics__aux@A_27a)@V8sr)@V9vm)@V10a)@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V11c)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V12l))@V13t)) = (ap@(ap@(ap@(c_2Esemi__ring_2Esemi__ring__SRP@A_27a)@V8sr)@V10a)@(ap@(ap@(ap@(ap@(c_2Ecanonical_2Eics__aux@A_27a)@V8sr)@V9vm)@(ap@(ap@(ap@(ap@(c_2Ecanonical_2Einterp__m@A_27a)@V8sr)@V9vm)@V11c)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V12l)))@V13t)))))))))))))))))).
thf(ax_thm_2Ecanonical_2Einterp__cs__def,axiom,( ! [A_27a:del]: (( ! [V0sr:$i] : ((mem@V0sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V1vm:$i] : ((mem@V1vm@(ty_2Equote_2Evarmap@A_27a)) => ((ap@(ap@(ap@(c_2Ecanonical_2Einterp__cs@A_27a)@V0sr)@V1vm)@(c_2Ecanonical_2ENil__monom@A_27a)) = (ap@(c_2Esemi__ring_2Esemi__ring__SR0@A_27a)@V0sr)))))) & (( ! [V2sr:$i] : ((mem@V2sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V3vm:$i] : ((mem@V3vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V4l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V5t:$i] : ((mem@V5t@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ((ap@(ap@(ap@(c_2Ecanonical_2Einterp__cs@A_27a)@V2sr)@V3vm)@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V4l))@V5t)) = (ap@(ap@(ap@(ap@(c_2Ecanonical_2Eics__aux@A_27a)@V2sr)@V3vm)@(ap@(ap@(ap@(c_2Ecanonical_2Einterp__vl@A_27a)@V2sr)@V3vm)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V4l)))@V5t))))))))) & ( ! [V6sr:$i] : ((mem@V6sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V7vm:$i] : ((mem@V7vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V8c:$i] : ((mem@V8c@A_27a) => ( ! [V9l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V10t:$i] : ((mem@V10t@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ((ap@(ap@(ap@(c_2Ecanonical_2Einterp__cs@A_27a)@V6sr)@V7vm)@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V8c)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V9l))@V10t)) = (ap@(ap@(ap@(ap@(c_2Ecanonical_2Eics__aux@A_27a)@V6sr)@V7vm)@(ap@(ap@(ap@(ap@(c_2Ecanonical_2Einterp__m@A_27a)@V6sr)@V7vm)@V8c)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V9l)))@V10t))))))))))))))).
thf(ax_thm_2Ecanonical_2Espolynom__normalize__def,axiom,( ! [A_27a:del]: (( ! [V0sr:$i] : ((mem@V0sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V1i:tp__ty_2Equote_2Eindex] : ((ap@(ap@(c_2Ecanonical_2Espolynom__normalize@A_27a)@V0sr)@(ap@(c_2Ecanonical_2ESPvar@A_27a)@(inj__ty_2Equote_2Eindex @ V1i))) = (ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(ap@(ap@(c_2Elist_2ECONS@ty_2Equote_2Eindex)@(inj__ty_2Equote_2Eindex @ V1i))@(c_2Elist_2ENIL@ty_2Equote_2Eindex)))@(c_2Ecanonical_2ENil__monom@A_27a)))))) & (( ! [V2sr:$i] : ((mem@V2sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V3c:$i] : ((mem@V3c@A_27a) => ((ap@(ap@(c_2Ecanonical_2Espolynom__normalize@A_27a)@V2sr)@(ap@(c_2Ecanonical_2ESPconst@A_27a)@V3c)) = (ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V3c)@(c_2Elist_2ENIL@ty_2Equote_2Eindex))@(c_2Ecanonical_2ENil__monom@A_27a))))))) & (( ! [V4sr:$i] : ((mem@V4sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V5l:$i] : ((mem@V5l@(ty_2Ecanonical_2Espolynom@A_27a)) => ( ! [V6r:$i] : ((mem@V6r@(ty_2Ecanonical_2Espolynom@A_27a)) => ((ap@(ap@(c_2Ecanonical_2Espolynom__normalize@A_27a)@V4sr)@(ap@(ap@(c_2Ecanonical_2ESPplus@A_27a)@V5l)@V6r)) = (ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__merge@A_27a)@V4sr)@(ap@(ap@(c_2Ecanonical_2Espolynom__normalize@A_27a)@V4sr)@V5l))@(ap@(ap@(c_2Ecanonical_2Espolynom__normalize@A_27a)@V4sr)@V6r))))))))) & ( ! [V7sr:$i] : ((mem@V7sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V8l:$i] : ((mem@V8l@(ty_2Ecanonical_2Espolynom@A_27a)) => ( ! [V9r:$i] : ((mem@V9r@(ty_2Ecanonical_2Espolynom@A_27a)) => ((ap@(ap@(c_2Ecanonical_2Espolynom__normalize@A_27a)@V7sr)@(ap@(ap@(c_2Ecanonical_2ESPmult@A_27a)@V8l)@V9r)) = (ap@(ap@(ap@(c_2Ecanonical_2Ecanonical__sum__prod@A_27a)@V7sr)@(ap@(ap@(c_2Ecanonical_2Espolynom__normalize@A_27a)@V7sr)@V8l))@(ap@(ap@(c_2Ecanonical_2Espolynom__normalize@A_27a)@V7sr)@V9r)))))))))))))).
thf(ax_thm_2Ecanonical_2Espolynom__simplify__def,axiom,( ! [A_27a:del]: ( ! [V0sr:$i] : ((mem@V0sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V1x:$i] : ((mem@V1x@(ty_2Ecanonical_2Espolynom@A_27a)) => ((ap@(ap@(c_2Ecanonical_2Espolynom__simplify@A_27a)@V0sr)@V1x) = (ap@(ap@(c_2Ecanonical_2Ecanonical__sum__simplify@A_27a)@V0sr)@(ap@(ap@(c_2Ecanonical_2Espolynom__normalize@A_27a)@V0sr)@V1x))))))))).
thf(ax_thm_2Ecanonical_2Einterp__sp__def,axiom,( ! [A_27a:del]: (( ! [V0sr:$i] : ((mem@V0sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V1vm:$i] : ((mem@V1vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V2c:$i] : ((mem@V2c@A_27a) => ((ap@(ap@(ap@(c_2Ecanonical_2Einterp__sp@A_27a)@V0sr)@V1vm)@(ap@(c_2Ecanonical_2ESPconst@A_27a)@V2c)) = V2c))))))) & (( ! [V3sr:$i] : ((mem@V3sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V4vm:$i] : ((mem@V4vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V5i:tp__ty_2Equote_2Eindex] : ((ap@(ap@(ap@(c_2Ecanonical_2Einterp__sp@A_27a)@V3sr)@V4vm)@(ap@(c_2Ecanonical_2ESPvar@A_27a)@(inj__ty_2Equote_2Eindex @ V5i))) = (ap@(ap@(c_2Equote_2Evarmap__find@A_27a)@(inj__ty_2Equote_2Eindex @ V5i))@V4vm))))))) & (( ! [V6sr:$i] : ((mem@V6sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V7vm:$i] : ((mem@V7vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V8p1:$i] : ((mem@V8p1@(ty_2Ecanonical_2Espolynom@A_27a)) => ( ! [V9p2:$i] : ((mem@V9p2@(ty_2Ecanonical_2Espolynom@A_27a)) => ((ap@(ap@(ap@(c_2Ecanonical_2Einterp__sp@A_27a)@V6sr)@V7vm)@(ap@(ap@(c_2Ecanonical_2ESPplus@A_27a)@V8p1)@V9p2)) = (ap@(ap@(ap@(c_2Esemi__ring_2Esemi__ring__SRP@A_27a)@V6sr)@(ap@(ap@(ap@(c_2Ecanonical_2Einterp__sp@A_27a)@V6sr)@V7vm)@V8p1))@(ap@(ap@(ap@(c_2Ecanonical_2Einterp__sp@A_27a)@V6sr)@V7vm)@V9p2))))))))))) & ( ! [V10sr:$i] : ((mem@V10sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ( ! [V11vm:$i] : ((mem@V11vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V12p1:$i] : ((mem@V12p1@(ty_2Ecanonical_2Espolynom@A_27a)) => ( ! [V13p2:$i] : ((mem@V13p2@(ty_2Ecanonical_2Espolynom@A_27a)) => ((ap@(ap@(ap@(c_2Ecanonical_2Einterp__sp@A_27a)@V10sr)@V11vm)@(ap@(ap@(c_2Ecanonical_2ESPmult@A_27a)@V12p1)@V13p2)) = (ap@(ap@(ap@(c_2Esemi__ring_2Esemi__ring__SRM@A_27a)@V10sr)@(ap@(ap@(ap@(c_2Ecanonical_2Einterp__sp@A_27a)@V10sr)@V11vm)@V12p1))@(ap@(ap@(ap@(c_2Ecanonical_2Einterp__sp@A_27a)@V10sr)@V11vm)@V13p2)))))))))))))))).
thf(conj_thm_2Ecanonical_2Espolynomial__simplify__ok,lemma,( ! [A_27a:del]: ( ! [V0sr:$i] : ((mem@V0sr@(ty_2Esemi__ring_2Esemi__ring@A_27a)) => ((p@(ap@(c_2Esemi__ring_2Eis__semi__ring@A_27a)@V0sr)) => ( ! [V1vm:$i] : ((mem@V1vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V2p:$i] : ((mem@V2p@(ty_2Ecanonical_2Espolynom@A_27a)) => ((ap@(ap@(ap@(c_2Ecanonical_2Einterp__cs@A_27a)@V0sr)@V1vm)@(ap@(ap@(c_2Ecanonical_2Espolynom__simplify@A_27a)@V0sr)@V2p)) = (ap@(ap@(ap@(c_2Ecanonical_2Einterp__sp@A_27a)@V0sr)@V1vm)@V2p))))))))))).
thf(conj_thm_2EnumRing_2Enum__semi__ring,lemma,(p@(ap@(c_2Esemi__ring_2Eis__semi__ring@ty_2Enum_2Enum)@(ap@(ap@(ap@(ap@(c_2Esemi__ring_2Erecordtype_2Esemi__ring@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@c_2Earithmetic_2E_2B)@c_2Earithmetic_2E_2A)))).
thf(ax_thm_2EnumRing_2Enum__interp__sp__def,axiom,(c_2EnumRing_2Enum__interp__sp = (ap@(c_2Ecanonical_2Einterp__sp@ty_2Enum_2Enum)@(ap@(ap@(ap@(ap@(c_2Esemi__ring_2Erecordtype_2Esemi__ring@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@c_2Earithmetic_2E_2B)@c_2Earithmetic_2E_2A)))).
thf(ax_thm_2EnumRing_2Enum__spolynom__simplify__def,axiom,(c_2EnumRing_2Enum__spolynom__simplify = (ap@(c_2Ecanonical_2Espolynom__simplify@ty_2Enum_2Enum)@(ap@(ap@(ap@(ap@(c_2Esemi__ring_2Erecordtype_2Esemi__ring@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@c_2Earithmetic_2E_2B)@c_2Earithmetic_2E_2A)))).
thf(ax_thm_2EnumRing_2Enum__spolynom__normalize__def,axiom,(c_2EnumRing_2Enum__spolynom__normalize = (ap@(c_2Ecanonical_2Espolynom__normalize@ty_2Enum_2Enum)@(ap@(ap@(ap@(ap@(c_2Esemi__ring_2Erecordtype_2Esemi__ring@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@c_2Earithmetic_2E_2B)@c_2Earithmetic_2E_2A)))).
thf(ax_thm_2EnumRing_2Enum__interp__cs__def,axiom,(c_2EnumRing_2Enum__interp__cs = (ap@(c_2Ecanonical_2Einterp__cs@ty_2Enum_2Enum)@(ap@(ap@(ap@(ap@(c_2Esemi__ring_2Erecordtype_2Esemi__ring@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@c_2Earithmetic_2E_2B)@c_2Earithmetic_2E_2A)))).
thf(ax_thm_2EnumRing_2Enum__ics__aux__def,axiom,(c_2EnumRing_2Enum__ics__aux = (ap@(c_2Ecanonical_2Eics__aux@ty_2Enum_2Enum)@(ap@(ap@(ap@(ap@(c_2Esemi__ring_2Erecordtype_2Esemi__ring@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@c_2Earithmetic_2E_2B)@c_2Earithmetic_2E_2A)))).
thf(ax_thm_2EnumRing_2Enum__interp__m__def,axiom,(c_2EnumRing_2Enum__interp__m = (ap@(c_2Ecanonical_2Einterp__m@ty_2Enum_2Enum)@(ap@(ap@(ap@(ap@(c_2Esemi__ring_2Erecordtype_2Esemi__ring@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@c_2Earithmetic_2E_2B)@c_2Earithmetic_2E_2A)))).
thf(ax_thm_2EnumRing_2Enum__interp__vl__def,axiom,(c_2EnumRing_2Enum__interp__vl = (ap@(c_2Ecanonical_2Einterp__vl@ty_2Enum_2Enum)@(ap@(ap@(ap@(ap@(c_2Esemi__ring_2Erecordtype_2Esemi__ring@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@c_2Earithmetic_2E_2B)@c_2Earithmetic_2E_2A)))).
thf(ax_thm_2EnumRing_2Enum__ivl__aux__def,axiom,(c_2EnumRing_2Enum__ivl__aux = (ap@(c_2Ecanonical_2Eivl__aux@ty_2Enum_2Enum)@(ap@(ap@(ap@(ap@(c_2Esemi__ring_2Erecordtype_2Esemi__ring@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@c_2Earithmetic_2E_2B)@c_2Earithmetic_2E_2A)))).
thf(ax_thm_2EnumRing_2Enum__canonical__sum__simplify__def,axiom,(c_2EnumRing_2Enum__canonical__sum__simplify = (ap@(c_2Ecanonical_2Ecanonical__sum__simplify@ty_2Enum_2Enum)@(ap@(ap@(ap@(ap@(c_2Esemi__ring_2Erecordtype_2Esemi__ring@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@c_2Earithmetic_2E_2B)@c_2Earithmetic_2E_2A)))).
thf(ax_thm_2EnumRing_2Enum__canonical__sum__prod__def,axiom,(c_2EnumRing_2Enum__canonical__sum__prod = (ap@(c_2Ecanonical_2Ecanonical__sum__prod@ty_2Enum_2Enum)@(ap@(ap@(ap@(ap@(c_2Esemi__ring_2Erecordtype_2Esemi__ring@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@c_2Earithmetic_2E_2B)@c_2Earithmetic_2E_2A)))).
thf(ax_thm_2EnumRing_2Enum__canonical__sum__scalar3__def,axiom,(c_2EnumRing_2Enum__canonical__sum__scalar3 = (ap@(c_2Ecanonical_2Ecanonical__sum__scalar3@ty_2Enum_2Enum)@(ap@(ap@(ap@(ap@(c_2Esemi__ring_2Erecordtype_2Esemi__ring@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@c_2Earithmetic_2E_2B)@c_2Earithmetic_2E_2A)))).
thf(ax_thm_2EnumRing_2Enum__canonical__sum__scalar2__def,axiom,(c_2EnumRing_2Enum__canonical__sum__scalar2 = (ap@(c_2Ecanonical_2Ecanonical__sum__scalar2@ty_2Enum_2Enum)@(ap@(ap@(ap@(ap@(c_2Esemi__ring_2Erecordtype_2Esemi__ring@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@c_2Earithmetic_2E_2B)@c_2Earithmetic_2E_2A)))).
thf(ax_thm_2EnumRing_2Enum__canonical__sum__scalar__def,axiom,(c_2EnumRing_2Enum__canonical__sum__scalar = (ap@(c_2Ecanonical_2Ecanonical__sum__scalar@ty_2Enum_2Enum)@(ap@(ap@(ap@(ap@(c_2Esemi__ring_2Erecordtype_2Esemi__ring@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@c_2Earithmetic_2E_2B)@c_2Earithmetic_2E_2A)))).
thf(ax_thm_2EnumRing_2Enum__varlist__insert__def,axiom,(c_2EnumRing_2Enum__varlist__insert = (ap@(c_2Ecanonical_2Evarlist__insert@ty_2Enum_2Enum)@(ap@(ap@(ap@(ap@(c_2Esemi__ring_2Erecordtype_2Esemi__ring@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@c_2Earithmetic_2E_2B)@c_2Earithmetic_2E_2A)))).
thf(ax_thm_2EnumRing_2Enum__monom__insert__def,axiom,(c_2EnumRing_2Enum__monom__insert = (ap@(c_2Ecanonical_2Emonom__insert@ty_2Enum_2Enum)@(ap@(ap@(ap@(ap@(c_2Esemi__ring_2Erecordtype_2Esemi__ring@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@c_2Earithmetic_2E_2B)@c_2Earithmetic_2E_2A)))).
thf(ax_thm_2EnumRing_2Enum__canonical__sum__merge__def,axiom,(c_2EnumRing_2Enum__canonical__sum__merge = (ap@(c_2Ecanonical_2Ecanonical__sum__merge@ty_2Enum_2Enum)@(ap@(ap@(ap@(ap@(c_2Esemi__ring_2Erecordtype_2Esemi__ring@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@c_2Earithmetic_2E_2B)@c_2Earithmetic_2E_2A)))).
thf(conj_thm_2Equote_2Evarmap__find__def,lemma,( ! [A_27a:del]: (( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1v2:$i] : ((mem@V1v2@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V2v1:$i] : ((mem@V2v1@(ty_2Equote_2Evarmap@A_27a)) => ((ap@(ap@(c_2Equote_2Evarmap__find@A_27a)@(inj__ty_2Equote_2Eindex @ fo__c_2Equote_2EEnd__idx))@(ap@(ap@(ap@(c_2Equote_2ENode__vm@A_27a)@V0x)@V2v1)@V1v2)) = V0x))))))) & (( ! [V3x:$i] : ((mem@V3x@A_27a) => ( ! [V4v2:$i] : ((mem@V4v2@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V5v1:$i] : ((mem@V5v1@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V6i1:tp__ty_2Equote_2Eindex] : ((ap@(ap@(c_2Equote_2Evarmap__find@A_27a)@(ap@c_2Equote_2ERight__idx@(inj__ty_2Equote_2Eindex @ V6i1)))@(ap@(ap@(ap@(c_2Equote_2ENode__vm@A_27a)@V3x)@V5v1)@V4v2)) = (ap@(ap@(c_2Equote_2Evarmap__find@A_27a)@(inj__ty_2Equote_2Eindex @ V6i1))@V4v2))))))))) & (( ! [V7x:$i] : ((mem@V7x@A_27a) => ( ! [V8v2:$i] : ((mem@V8v2@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V9v1:$i] : ((mem@V9v1@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V10i1:tp__ty_2Equote_2Eindex] : ((ap@(ap@(c_2Equote_2Evarmap__find@A_27a)@(ap@c_2Equote_2ELeft__idx@(inj__ty_2Equote_2Eindex @ V10i1)))@(ap@(ap@(ap@(c_2Equote_2ENode__vm@A_27a)@V7x)@V9v1)@V8v2)) = (ap@(ap@(c_2Equote_2Evarmap__find@A_27a)@(inj__ty_2Equote_2Eindex @ V10i1))@V9v1))))))))) & ( ! [V11i:tp__ty_2Equote_2Eindex] : ((ap@(ap@(c_2Equote_2Evarmap__find@A_27a)@(inj__ty_2Equote_2Eindex @ V11i))@(c_2Equote_2EEmpty__vm@A_27a)) = (ap@(c_2Emin_2E_40@A_27a)@(lam@A_27a@(^ [V12x:$i] : c_2Ebool_2ET)))))))))).
thf(conj_thm_2Esemi__ring_2Esemi__ring__accessors,lemma,( ! [A_27a:del]: (( ! [V0a:$i] : ((mem@V0a@A_27a) => ( ! [V1a0:$i] : ((mem@V1a0@A_27a) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V3f0:$i] : ((mem@V3f0@(arr@A_27a@(arr@A_27a@A_27a))) => ((ap@(c_2Esemi__ring_2Esemi__ring__SR0@A_27a)@(ap@(ap@(ap@(ap@(c_2Esemi__ring_2Erecordtype_2Esemi__ring@A_27a)@V0a)@V1a0)@V2f)@V3f0)) = V0a))))))))) & (( ! [V4a:$i] : ((mem@V4a@A_27a) => ( ! [V5a0:$i] : ((mem@V5a0@A_27a) => ( ! [V6f:$i] : ((mem@V6f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V7f0:$i] : ((mem@V7f0@(arr@A_27a@(arr@A_27a@A_27a))) => ((ap@(c_2Esemi__ring_2Esemi__ring__SR1@A_27a)@(ap@(ap@(ap@(ap@(c_2Esemi__ring_2Erecordtype_2Esemi__ring@A_27a)@V4a)@V5a0)@V6f)@V7f0)) = V5a0))))))))) & (( ! [V8a:$i] : ((mem@V8a@A_27a) => ( ! [V9a0:$i] : ((mem@V9a0@A_27a) => ( ! [V10f:$i] : ((mem@V10f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V11f0:$i] : ((mem@V11f0@(arr@A_27a@(arr@A_27a@A_27a))) => ((ap@(c_2Esemi__ring_2Esemi__ring__SRP@A_27a)@(ap@(ap@(ap@(ap@(c_2Esemi__ring_2Erecordtype_2Esemi__ring@A_27a)@V8a)@V9a0)@V10f)@V11f0)) = V10f))))))))) & ( ! [V12a:$i] : ((mem@V12a@A_27a) => ( ! [V13a0:$i] : ((mem@V13a0@A_27a) => ( ! [V14f:$i] : ((mem@V14f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V15f0:$i] : ((mem@V15f0@(arr@A_27a@(arr@A_27a@A_27a))) => ((ap@(c_2Esemi__ring_2Esemi__ring__SRM@A_27a)@(ap@(ap@(ap@(ap@(c_2Esemi__ring_2Erecordtype_2Esemi__ring@A_27a)@V12a)@V13a0)@V14f)@V15f0)) = V15f0)))))))))))))).
thf(conj_thm_2EnumRing_2Enum__ring__thms,conjecture,( ! [A_27a:del]: ((p@(ap@(c_2Esemi__ring_2Eis__semi__ring@ty_2Enum_2Enum)@(ap@(ap@(ap@(ap@(c_2Esemi__ring_2Erecordtype_2Esemi__ring@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@c_2Earithmetic_2E_2B)@c_2Earithmetic_2E_2A))) & (( ! [V0vm:tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum] : ( ! [V1p:tp__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__interp__sp@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V0vm))@(inj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum @ V1p))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__interp__cs@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V0vm))@(ap@c_2EnumRing_2Enum__spolynom__simplify@(inj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum @ V1p))))))) & (((( ! [V2vm:tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum] : ( ! [V3c:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__interp__sp@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V2vm))@(ap@(c_2Ecanonical_2ESPconst@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V3c)))) = V3c))) & (( ! [V4vm:tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum] : ( ! [V5i:tp__ty_2Equote_2Eindex] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__interp__sp@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V4vm))@(ap@(c_2Ecanonical_2ESPvar@ty_2Enum_2Enum)@(inj__ty_2Equote_2Eindex @ V5i)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(c_2Equote_2Evarmap__find@ty_2Enum_2Enum)@(inj__ty_2Equote_2Eindex @ V5i))@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V4vm)))))) & (( ! [V6vm:tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum] : ( ! [V7p1:tp__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum] : ( ! [V8p2:tp__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__interp__sp@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V6vm))@(ap@(ap@(c_2Ecanonical_2ESPplus@ty_2Enum_2Enum)@(inj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum @ V7p1))@(inj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum @ V8p2)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@c_2EnumRing_2Enum__interp__sp@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V6vm))@(inj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum @ V7p1)))@(ap@(ap@c_2EnumRing_2Enum__interp__sp@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V6vm))@(inj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum @ V8p2)))))))) & ( ! [V9vm:tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum] : ( ! [V10p1:tp__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum] : ( ! [V11p2:tp__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__interp__sp@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V9vm))@(ap@(ap@(c_2Ecanonical_2ESPmult@ty_2Enum_2Enum)@(inj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum @ V10p1))@(inj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum @ V11p2)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2A@(ap@(ap@c_2EnumRing_2Enum__interp__sp@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V9vm))@(inj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum @ V10p1)))@(ap@(ap@c_2EnumRing_2Enum__interp__sp@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V9vm))@(inj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum @ V11p2))))))))))) & (( ! [V12x:$i] : ((mem@V12x@A_27a) => ( ! [V13v2:$i] : ((mem@V13v2@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V14v1:$i] : ((mem@V14v1@(ty_2Equote_2Evarmap@A_27a)) => ((ap@(ap@(c_2Equote_2Evarmap__find@A_27a)@(inj__ty_2Equote_2Eindex @ fo__c_2Equote_2EEnd__idx))@(ap@(ap@(ap@(c_2Equote_2ENode__vm@A_27a)@V12x)@V14v1)@V13v2)) = V12x))))))) & (( ! [V15x:$i] : ((mem@V15x@A_27a) => ( ! [V16v2:$i] : ((mem@V16v2@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V17v1:$i] : ((mem@V17v1@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V18i1:tp__ty_2Equote_2Eindex] : ((ap@(ap@(c_2Equote_2Evarmap__find@A_27a)@(ap@c_2Equote_2ERight__idx@(inj__ty_2Equote_2Eindex @ V18i1)))@(ap@(ap@(ap@(c_2Equote_2ENode__vm@A_27a)@V15x)@V17v1)@V16v2)) = (ap@(ap@(c_2Equote_2Evarmap__find@A_27a)@(inj__ty_2Equote_2Eindex @ V18i1))@V16v2))))))))) & (( ! [V19x:$i] : ((mem@V19x@A_27a) => ( ! [V20v2:$i] : ((mem@V20v2@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V21v1:$i] : ((mem@V21v1@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V22i1:tp__ty_2Equote_2Eindex] : ((ap@(ap@(c_2Equote_2Evarmap__find@A_27a)@(ap@c_2Equote_2ELeft__idx@(inj__ty_2Equote_2Eindex @ V22i1)))@(ap@(ap@(ap@(c_2Equote_2ENode__vm@A_27a)@V19x)@V21v1)@V20v2)) = (ap@(ap@(c_2Equote_2Evarmap__find@A_27a)@(inj__ty_2Equote_2Eindex @ V22i1))@V21v1))))))))) & ( ! [V23i:tp__ty_2Equote_2Eindex] : ((ap@(ap@(c_2Equote_2Evarmap__find@A_27a)@(inj__ty_2Equote_2Eindex @ V23i))@(c_2Equote_2EEmpty__vm@A_27a)) = (ap@(c_2Emin_2E_40@A_27a)@(lam@A_27a@(^ [V24x:$i] : c_2Ebool_2ET))))))))) & ((( ! [V25t2:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ( ! [V26t1:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ( ! [V27l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V28l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V29c2:tp__ty_2Enum_2Enum] : ( ! [V30c1:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__canonical__sum__merge@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V30c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V28l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V26t1)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V29c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V27l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V25t2)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(ap@(ap@(c_2EternaryComparisons_2Eordering__CASE@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum))@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__compare@ty_2Equote_2Eindex@ty_2Equote_2Eindex)@c_2Equote_2Eindex__compare)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V28l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V27l2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V30c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V28l1))@(ap@(ap@c_2EnumRing_2Enum__canonical__sum__merge@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V26t1))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V29c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V27l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V25t2)))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V30c1))@(inj__ty_2Enum_2Enum @ V29c2)))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V28l1))@(ap@(ap@c_2EnumRing_2Enum__canonical__sum__merge@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V26t1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V25t2))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V29c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V27l2))@(ap@(ap@c_2EnumRing_2Enum__canonical__sum__merge@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V30c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V28l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V26t1)))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V25t2)))))))))))) & (( ! [V31t2:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ( ! [V32t1:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ( ! [V33l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V34l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V35c1:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__canonical__sum__merge@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V35c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V34l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V32t1)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V33l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V31t2)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(ap@(ap@(c_2EternaryComparisons_2Eordering__CASE@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum))@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__compare@ty_2Equote_2Eindex@ty_2Equote_2Eindex)@c_2Equote_2Eindex__compare)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V34l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V33l2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V35c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V34l1))@(ap@(ap@c_2EnumRing_2Enum__canonical__sum__merge@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V32t1))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V33l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V31t2)))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V35c1))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V34l1))@(ap@(ap@c_2EnumRing_2Enum__canonical__sum__merge@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V32t1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V31t2))))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V33l2))@(ap@(ap@c_2EnumRing_2Enum__canonical__sum__merge@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V35c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V34l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V32t1)))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V31t2))))))))))) & (( ! [V36t2:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ( ! [V37t1:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ( ! [V38l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V39l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V40c2:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__canonical__sum__merge@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V39l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V37t1)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V40c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V38l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V36t2)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(ap@(ap@(c_2EternaryComparisons_2Eordering__CASE@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum))@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__compare@ty_2Equote_2Eindex@ty_2Equote_2Eindex)@c_2Equote_2Eindex__compare)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V39l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V38l2)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V39l1))@(ap@(ap@c_2EnumRing_2Enum__canonical__sum__merge@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V37t1))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V40c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V38l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V36t2)))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@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))))@(inj__ty_2Enum_2Enum @ V40c2)))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V39l1))@(ap@(ap@c_2EnumRing_2Enum__canonical__sum__merge@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V37t1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V36t2))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V40c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V38l2))@(ap@(ap@c_2EnumRing_2Enum__canonical__sum__merge@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V39l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V37t1)))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V36t2))))))))))) & (( ! [V41t2:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ( ! [V42t1:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ( ! [V43l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V44l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__canonical__sum__merge@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V44l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V42t1)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V43l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V41t2)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(ap@(ap@(c_2EternaryComparisons_2Eordering__CASE@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum))@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__compare@ty_2Equote_2Eindex@ty_2Equote_2Eindex)@c_2Equote_2Eindex__compare)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V44l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V43l2)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V44l1))@(ap@(ap@c_2EnumRing_2Enum__canonical__sum__merge@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V42t1))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V43l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V41t2)))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@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_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V44l1))@(ap@(ap@c_2EnumRing_2Enum__canonical__sum__merge@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V42t1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V41t2))))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V43l2))@(ap@(ap@c_2EnumRing_2Enum__canonical__sum__merge@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V44l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V42t1)))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V41t2)))))))))) & (( ! [V45s1:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__canonical__sum__merge@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V45s1))@(c_2Ecanonical_2ENil__monom@ty_2Enum_2Enum))) = V45s1)) & (( ! [V46v6:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ( ! [V47v5:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V48v4:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__canonical__sum__merge@(c_2Ecanonical_2ENil__monom@ty_2Enum_2Enum))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V48v4))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V47v5))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V46v6)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V48v4))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V47v5))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V46v6))))))) & ( ! [V49v8:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ( ! [V50v7:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__canonical__sum__merge@(c_2Ecanonical_2ENil__monom@ty_2Enum_2Enum))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V50v7))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V49v8)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V50v7))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V49v8)))))))))))) & ((( ! [V51t2:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ( ! [V52l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V53l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V54c2:tp__ty_2Enum_2Enum] : ( ! [V55c1:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(ap@c_2EnumRing_2Enum__monom__insert@(inj__ty_2Enum_2Enum @ V55c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V53l1))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V54c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V52l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V51t2)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(ap@(ap@(c_2EternaryComparisons_2Eordering__CASE@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum))@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__compare@ty_2Equote_2Eindex@ty_2Equote_2Eindex)@c_2Equote_2Eindex__compare)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V53l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V52l2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V55c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V53l1))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V54c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V52l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V51t2))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V55c1))@(inj__ty_2Enum_2Enum @ V54c2)))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V53l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V51t2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V54c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V52l2))@(ap@(ap@(ap@c_2EnumRing_2Enum__monom__insert@(inj__ty_2Enum_2Enum @ V55c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V53l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V51t2))))))))))) & (( ! [V56t2:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ( ! [V57l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V58l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V59c1:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(ap@c_2EnumRing_2Enum__monom__insert@(inj__ty_2Enum_2Enum @ V59c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V58l1))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V57l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V56t2)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(ap@(ap@(c_2EternaryComparisons_2Eordering__CASE@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum))@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__compare@ty_2Equote_2Eindex@ty_2Equote_2Eindex)@c_2Equote_2Eindex__compare)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V58l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V57l2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V59c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V58l1))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V57l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V56t2))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V59c1))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V58l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V56t2)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V57l2))@(ap@(ap@(ap@c_2EnumRing_2Enum__monom__insert@(inj__ty_2Enum_2Enum @ V59c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V58l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V56t2)))))))))) & ( ! [V60l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V61c1:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(ap@c_2EnumRing_2Enum__monom__insert@(inj__ty_2Enum_2Enum @ V61c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V60l1))@(c_2Ecanonical_2ENil__monom@ty_2Enum_2Enum))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V61c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V60l1))@(c_2Ecanonical_2ENil__monom@ty_2Enum_2Enum)))))))) & ((( ! [V62t2:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ( ! [V63l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V64l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V65c2:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__varlist__insert@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V64l1))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V65c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V63l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V62t2)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(ap@(ap@(c_2EternaryComparisons_2Eordering__CASE@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum))@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__compare@ty_2Equote_2Eindex@ty_2Equote_2Eindex)@c_2Equote_2Eindex__compare)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V64l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V63l2)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V64l1))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V65c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V63l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V62t2))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@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))))@(inj__ty_2Enum_2Enum @ V65c2)))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V64l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V62t2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V65c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V63l2))@(ap@(ap@c_2EnumRing_2Enum__varlist__insert@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V64l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V62t2)))))))))) & (( ! [V66t2:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ( ! [V67l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V68l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__varlist__insert@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V68l1))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V67l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V66t2)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(ap@(ap@(c_2EternaryComparisons_2Eordering__CASE@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum))@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__compare@ty_2Equote_2Eindex@ty_2Equote_2Eindex)@c_2Equote_2Eindex__compare)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V68l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V67l2)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V68l1))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V67l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V66t2))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@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_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V68l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V66t2)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V67l2))@(ap@(ap@c_2EnumRing_2Enum__varlist__insert@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V68l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V66t2))))))))) & ( ! [V69l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__varlist__insert@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V69l1))@(c_2Ecanonical_2ENil__monom@ty_2Enum_2Enum))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V69l1))@(c_2Ecanonical_2ENil__monom@ty_2Enum_2Enum))))))) & ((( ! [V70c0:tp__ty_2Enum_2Enum] : ( ! [V71c:tp__ty_2Enum_2Enum] : ( ! [V72l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V73t:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__canonical__sum__scalar@(inj__ty_2Enum_2Enum @ V70c0))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V71c))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V72l))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V73t)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V70c0))@(inj__ty_2Enum_2Enum @ V71c)))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V72l))@(ap@(ap@c_2EnumRing_2Enum__canonical__sum__scalar@(inj__ty_2Enum_2Enum @ V70c0))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V73t))))))))) & (( ! [V74c0:tp__ty_2Enum_2Enum] : ( ! [V75l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V76t:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__canonical__sum__scalar@(inj__ty_2Enum_2Enum @ V74c0))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V75l))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V76t)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V74c0))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V75l))@(ap@(ap@c_2EnumRing_2Enum__canonical__sum__scalar@(inj__ty_2Enum_2Enum @ V74c0))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V76t)))))))) & ( ! [V77c0:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__canonical__sum__scalar@(inj__ty_2Enum_2Enum @ V77c0))@(c_2Ecanonical_2ENil__monom@ty_2Enum_2Enum))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (c_2Ecanonical_2ENil__monom@ty_2Enum_2Enum)))))) & ((( ! [V78l0:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V79c:tp__ty_2Enum_2Enum] : ( ! [V80l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V81t:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__canonical__sum__scalar2@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V78l0))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V79c))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V80l))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V81t)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(ap@c_2EnumRing_2Enum__monom__insert@(inj__ty_2Enum_2Enum @ V79c))@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__merge@ty_2Equote_2Eindex)@c_2Equote_2Eindex__lt)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V78l0))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V80l)))@(ap@(ap@c_2EnumRing_2Enum__canonical__sum__scalar2@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V78l0))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V81t))))))))) & (( ! [V82l0:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V83l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V84t:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__canonical__sum__scalar2@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V82l0))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V83l))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V84t)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__varlist__insert@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__merge@ty_2Equote_2Eindex)@c_2Equote_2Eindex__lt)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V82l0))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V83l)))@(ap@(ap@c_2EnumRing_2Enum__canonical__sum__scalar2@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V82l0))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V84t)))))))) & ( ! [V85l0:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__canonical__sum__scalar2@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V85l0))@(c_2Ecanonical_2ENil__monom@ty_2Enum_2Enum))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (c_2Ecanonical_2ENil__monom@ty_2Enum_2Enum)))))) & ((( ! [V86c0:tp__ty_2Enum_2Enum] : ( ! [V87l0:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V88c:tp__ty_2Enum_2Enum] : ( ! [V89l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V90t:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(ap@c_2EnumRing_2Enum__canonical__sum__scalar3@(inj__ty_2Enum_2Enum @ V86c0))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V87l0))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V88c))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V89l))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V90t)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(ap@c_2EnumRing_2Enum__monom__insert@(ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V86c0))@(inj__ty_2Enum_2Enum @ V88c)))@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__merge@ty_2Equote_2Eindex)@c_2Equote_2Eindex__lt)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V87l0))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V89l)))@(ap@(ap@(ap@c_2EnumRing_2Enum__canonical__sum__scalar3@(inj__ty_2Enum_2Enum @ V86c0))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V87l0))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V90t)))))))))) & (( ! [V91c0:tp__ty_2Enum_2Enum] : ( ! [V92l0:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V93l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V94t:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(ap@c_2EnumRing_2Enum__canonical__sum__scalar3@(inj__ty_2Enum_2Enum @ V91c0))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V92l0))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V93l))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V94t)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(ap@c_2EnumRing_2Enum__monom__insert@(inj__ty_2Enum_2Enum @ V91c0))@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__merge@ty_2Equote_2Eindex)@c_2Equote_2Eindex__lt)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V92l0))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V93l)))@(ap@(ap@(ap@c_2EnumRing_2Enum__canonical__sum__scalar3@(inj__ty_2Enum_2Enum @ V91c0))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V92l0))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V94t))))))))) & ( ! [V95c0:tp__ty_2Enum_2Enum] : ( ! [V96l0:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(ap@c_2EnumRing_2Enum__canonical__sum__scalar3@(inj__ty_2Enum_2Enum @ V95c0))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V96l0))@(c_2Ecanonical_2ENil__monom@ty_2Enum_2Enum))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (c_2Ecanonical_2ENil__monom@ty_2Enum_2Enum))))))) & ((( ! [V97c1:tp__ty_2Enum_2Enum] : ( ! [V98l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V99t1:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ( ! [V100s2:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__canonical__sum__prod@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V97c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V98l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V99t1)))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V100s2))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__canonical__sum__merge@(ap@(ap@(ap@c_2EnumRing_2Enum__canonical__sum__scalar3@(inj__ty_2Enum_2Enum @ V97c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V98l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V100s2)))@(ap@(ap@c_2EnumRing_2Enum__canonical__sum__prod@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V99t1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V100s2))))))))) & (( ! [V101l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V102t1:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ( ! [V103s2:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__canonical__sum__prod@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V101l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V102t1)))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V103s2))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__canonical__sum__merge@(ap@(ap@c_2EnumRing_2Enum__canonical__sum__scalar2@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V101l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V103s2)))@(ap@(ap@c_2EnumRing_2Enum__canonical__sum__prod@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V102t1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V103s2)))))))) & ( ! [V104s2:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__canonical__sum__prod@(c_2Ecanonical_2ENil__monom@ty_2Enum_2Enum))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V104s2))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (c_2Ecanonical_2ENil__monom@ty_2Enum_2Enum)))))) & ((( ! [V105c:tp__ty_2Enum_2Enum] : ( ! [V106l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V107t:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@c_2EnumRing_2Enum__canonical__sum__simplify@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V105c))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V106l))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V107t)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum))@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V105c))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@c_2EnumRing_2Enum__canonical__sum__simplify@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V107t)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Ecanonical_2Ecanonical__sum@ty_2Enum_2Enum))@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V105c))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V106l))@(ap@c_2EnumRing_2Enum__canonical__sum__simplify@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V107t))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V105c))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V106l))@(ap@c_2EnumRing_2Enum__canonical__sum__simplify@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V107t)))))))))) & (( ! [V108l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V109t:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@c_2EnumRing_2Enum__canonical__sum__simplify@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V108l))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V109t)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V108l))@(ap@c_2EnumRing_2Enum__canonical__sum__simplify@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V109t))))))) & ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@c_2EnumRing_2Enum__canonical__sum__simplify@(c_2Ecanonical_2ENil__monom@ty_2Enum_2Enum))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (c_2Ecanonical_2ENil__monom@ty_2Enum_2Enum))))) & ((( ! [V110vm:tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum] : ( ! [V111x:tp__ty_2Equote_2Eindex] : ((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2EnumRing_2Enum__ivl__aux@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V110vm))@(inj__ty_2Equote_2Eindex @ V111x))@(c_2Elist_2ENIL@ty_2Equote_2Eindex))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(c_2Equote_2Evarmap__find@ty_2Enum_2Enum)@(inj__ty_2Equote_2Eindex @ V111x))@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V110vm)))))) & ( ! [V112vm:tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum] : ( ! [V113x:tp__ty_2Equote_2Eindex] : ( ! [V114x_27:tp__ty_2Equote_2Eindex] : ( ! [V115t_27:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2EnumRing_2Enum__ivl__aux@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V112vm))@(inj__ty_2Equote_2Eindex @ V113x))@(ap@(ap@(c_2Elist_2ECONS@ty_2Equote_2Eindex)@(inj__ty_2Equote_2Eindex @ V114x_27))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V115t_27)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2A@(ap@(ap@(c_2Equote_2Evarmap__find@ty_2Enum_2Enum)@(inj__ty_2Equote_2Eindex @ V113x))@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V112vm)))@(ap@(ap@(ap@c_2EnumRing_2Enum__ivl__aux@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V112vm))@(inj__ty_2Equote_2Eindex @ V114x_27))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V115t_27)))))))))) & ((( ! [V116vm:tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__interp__vl@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V116vm))@(c_2Elist_2ENIL@ty_2Equote_2Eindex))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) & ( ! [V117vm:tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum] : ( ! [V118x:tp__ty_2Equote_2Eindex] : ( ! [V119t:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__interp__vl@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V117vm))@(ap@(ap@(c_2Elist_2ECONS@ty_2Equote_2Eindex)@(inj__ty_2Equote_2Eindex @ V118x))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V119t)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2EnumRing_2Enum__ivl__aux@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V117vm))@(inj__ty_2Equote_2Eindex @ V118x))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V119t)))))))) & ((( ! [V120vm:tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum] : ( ! [V121c:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2EnumRing_2Enum__interp__m@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V120vm))@(inj__ty_2Enum_2Enum @ V121c))@(c_2Elist_2ENIL@ty_2Equote_2Eindex))) = V121c))) & ( ! [V122vm:tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum] : ( ! [V123c:tp__ty_2Enum_2Enum] : ( ! [V124x:tp__ty_2Equote_2Eindex] : ( ! [V125t:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2EnumRing_2Enum__interp__m@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V122vm))@(inj__ty_2Enum_2Enum @ V123c))@(ap@(ap@(c_2Elist_2ECONS@ty_2Equote_2Eindex)@(inj__ty_2Equote_2Eindex @ V124x))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V125t)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V123c))@(ap@(ap@(ap@c_2EnumRing_2Enum__ivl__aux@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V122vm))@(inj__ty_2Equote_2Eindex @ V124x))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V125t)))))))))) & ((( ! [V126vm:tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum] : ( ! [V127a:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2EnumRing_2Enum__ics__aux@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V126vm))@(inj__ty_2Enum_2Enum @ V127a))@(c_2Ecanonical_2ENil__monom@ty_2Enum_2Enum))) = V127a))) & (( ! [V128vm:tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum] : ( ! [V129a:tp__ty_2Enum_2Enum] : ( ! [V130l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V131t:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2EnumRing_2Enum__ics__aux@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V128vm))@(inj__ty_2Enum_2Enum @ V129a))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V130l))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V131t)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V129a))@(ap@(ap@(ap@c_2EnumRing_2Enum__ics__aux@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V128vm))@(ap@(ap@c_2EnumRing_2Enum__interp__vl@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V128vm))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V130l)))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V131t))))))))) & ( ! [V132vm:tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum] : ( ! [V133a:tp__ty_2Enum_2Enum] : ( ! [V134c:tp__ty_2Enum_2Enum] : ( ! [V135l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V136t:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2EnumRing_2Enum__ics__aux@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V132vm))@(inj__ty_2Enum_2Enum @ V133a))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V134c))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V135l))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V136t)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V133a))@(ap@(ap@(ap@c_2EnumRing_2Enum__ics__aux@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V132vm))@(ap@(ap@(ap@c_2EnumRing_2Enum__interp__m@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V132vm))@(inj__ty_2Enum_2Enum @ V134c))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V135l)))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V136t)))))))))))) & ((( ! [V137vm:tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__interp__cs@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V137vm))@(c_2Ecanonical_2ENil__monom@ty_2Enum_2Enum))) = fo__c_2Enum_2E0)) & (( ! [V138vm:tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum] : ( ! [V139l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V140t:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__interp__cs@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V138vm))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V139l))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V140t)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2EnumRing_2Enum__ics__aux@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V138vm))@(ap@(ap@c_2EnumRing_2Enum__interp__vl@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V138vm))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V139l)))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V140t))))))) & ( ! [V141vm:tp__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum] : ( ! [V142c:tp__ty_2Enum_2Enum] : ( ! [V143l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V144t:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__interp__cs@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V141vm))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V142c))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V143l))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V144t)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2EnumRing_2Enum__ics__aux@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V141vm))@(ap@(ap@(ap@c_2EnumRing_2Enum__interp__m@(inj__c_ty_2Equote_2Evarmap_ty_2Enum_2Enum @ V141vm))@(inj__ty_2Enum_2Enum @ V142c))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V143l)))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ V144t)))))))))) & ((( ! [V145i:tp__ty_2Equote_2Eindex] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@c_2EnumRing_2Enum__spolynom__normalize@(ap@(c_2Ecanonical_2ESPvar@ty_2Enum_2Enum)@(inj__ty_2Equote_2Eindex @ V145i)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Enum_2Enum)@(ap@(ap@(c_2Elist_2ECONS@ty_2Equote_2Eindex)@(inj__ty_2Equote_2Eindex @ V145i))@(c_2Elist_2ENIL@ty_2Equote_2Eindex)))@(c_2Ecanonical_2ENil__monom@ty_2Enum_2Enum))))) & (( ! [V146c:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@c_2EnumRing_2Enum__spolynom__normalize@(ap@(c_2Ecanonical_2ESPconst@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V146c)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V146c))@(c_2Elist_2ENIL@ty_2Equote_2Eindex))@(c_2Ecanonical_2ENil__monom@ty_2Enum_2Enum))))) & (( ! [V147l:tp__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum] : ( ! [V148r:tp__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@c_2EnumRing_2Enum__spolynom__normalize@(ap@(ap@(c_2Ecanonical_2ESPplus@ty_2Enum_2Enum)@(inj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum @ V147l))@(inj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum @ V148r)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__canonical__sum__merge@(ap@c_2EnumRing_2Enum__spolynom__normalize@(inj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum @ V147l)))@(ap@c_2EnumRing_2Enum__spolynom__normalize@(inj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum @ V148r))))))) & ( ! [V149l:tp__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum] : ( ! [V150r:tp__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@c_2EnumRing_2Enum__spolynom__normalize@(ap@(ap@(c_2Ecanonical_2ESPmult@ty_2Enum_2Enum)@(inj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum @ V149l))@(inj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum @ V150r)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@(ap@c_2EnumRing_2Enum__canonical__sum__prod@(ap@c_2EnumRing_2Enum__spolynom__normalize@(inj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum @ V149l)))@(ap@c_2EnumRing_2Enum__spolynom__normalize@(inj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum @ V150r)))))))))) & ( ! [V151x:tp__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@c_2EnumRing_2Enum__spolynom__simplify@(inj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum @ V151x))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Enum_2Enum @ (ap@c_2EnumRing_2Enum__canonical__sum__simplify@(ap@c_2EnumRing_2Enum__spolynom__normalize@(inj__c_ty_2Ecanonical_2Espolynom_ty_2Enum_2Enum @ V151x))))))))))))))))))))))))).
