include('Axioms/numRing^2.ax').
thf(stp_c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint,type,(tp__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint : $tType)).
thf(stp_inj_c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint,type,(inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint : (tp__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint > $i))).
thf(stp_surj_c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint,type,(surj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint : ($i > tp__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint))).
thf(stp_inj_surj_c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint,axiom,( ! [X:tp__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint] : ((surj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ (inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ X)) = X))).
thf(stp_inj_mem_c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint,axiom,( ! [X:tp__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint] : (mem @ (inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ X) @ (ty_2EringNorm_2Epolynom@ty_2Einteger_2Eint)))).
thf(stp_iso_mem_c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint,axiom,( ! [X:$i] : ((mem @ X @ (ty_2EringNorm_2Epolynom@ty_2Einteger_2Eint)) => (X = (inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ (surj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ X)))))).
thf(stp_c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint,type,(tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint : $tType)).
thf(stp_inj_c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint,type,(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint : (tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint > $i))).
thf(stp_surj_c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint,type,(surj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint : ($i > tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint))).
thf(stp_inj_surj_c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint,axiom,( ! [X:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : ((surj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ (inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ X)) = X))).
thf(stp_inj_mem_c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint,axiom,( ! [X:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : (mem @ (inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ X) @ (ty_2Equote_2Evarmap@ty_2Einteger_2Eint)))).
thf(stp_iso_mem_c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Equote_2Evarmap@ty_2Einteger_2Eint)) => (X = (inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ (surj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ X)))))).
thf(tp_c_2EintegerRing_2Eint__interp__p,type,(c_2EintegerRing_2Eint__interp__p:$i)).
thf(mem_c_2EintegerRing_2Eint__interp__p,axiom,(mem@c_2EintegerRing_2Eint__interp__p@(arr@(ty_2Equote_2Evarmap@ty_2Einteger_2Eint)@(arr@(ty_2EringNorm_2Epolynom@ty_2Einteger_2Eint)@ty_2Einteger_2Eint)))).
thf(stp_fo_c_2EintegerRing_2Eint__interp__p,type,(fo__c_2EintegerRing_2Eint__interp__p:(tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint > (tp__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint > tp__ty_2Einteger_2Eint)))).
thf(stp_eq_fo_c_2EintegerRing_2Eint__interp__p,axiom,( ! [X0:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : ( ! [X1:tp__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint] : ((inj__ty_2Einteger_2Eint @ ((fo__c_2EintegerRing_2Eint__interp__p @ X0) @ X1)) = (ap @ (ap @ c_2EintegerRing_2Eint__interp__p @ (inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ X0)) @ (inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ X1)))))).
thf(stp_c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint,type,(tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint : $tType)).
thf(stp_inj_c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint,type,(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint : (tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint > $i))).
thf(stp_surj_c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint,type,(surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint : ($i > tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint))).
thf(stp_inj_surj_c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint,axiom,( ! [X:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ X)) = X))).
thf(stp_inj_mem_c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint,axiom,( ! [X:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : (mem @ (inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ X) @ (ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint)))).
thf(stp_iso_mem_c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint)) => (X = (inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ X)))))).
thf(tp_c_2EintegerRing_2Eint__polynom__normalize,type,(c_2EintegerRing_2Eint__polynom__normalize:$i)).
thf(mem_c_2EintegerRing_2Eint__polynom__normalize,axiom,(mem@c_2EintegerRing_2Eint__polynom__normalize@(arr@(ty_2EringNorm_2Epolynom@ty_2Einteger_2Eint)@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint)))).
thf(tp_c_2EintegerRing_2Eint__polynom__simplify,type,(c_2EintegerRing_2Eint__polynom__simplify:$i)).
thf(mem_c_2EintegerRing_2Eint__polynom__simplify,axiom,(mem@c_2EintegerRing_2Eint__polynom__simplify@(arr@(ty_2EringNorm_2Epolynom@ty_2Einteger_2Eint)@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint)))).
thf(tp_c_2EintegerRing_2Eint__r__canonical__sum__merge,type,(c_2EintegerRing_2Eint__r__canonical__sum__merge:$i)).
thf(mem_c_2EintegerRing_2Eint__r__canonical__sum__merge,axiom,(mem@c_2EintegerRing_2Eint__r__canonical__sum__merge@(arr@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint)@(arr@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint)@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint))))).
thf(tp_c_2EintegerRing_2Eint__r__canonical__sum__prod,type,(c_2EintegerRing_2Eint__r__canonical__sum__prod:$i)).
thf(mem_c_2EintegerRing_2Eint__r__canonical__sum__prod,axiom,(mem@c_2EintegerRing_2Eint__r__canonical__sum__prod@(arr@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint)@(arr@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint)@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint))))).
thf(tp_c_2EintegerRing_2Eint__r__canonical__sum__scalar,type,(c_2EintegerRing_2Eint__r__canonical__sum__scalar:$i)).
thf(mem_c_2EintegerRing_2Eint__r__canonical__sum__scalar,axiom,(mem@c_2EintegerRing_2Eint__r__canonical__sum__scalar@(arr@ty_2Einteger_2Eint@(arr@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint)@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint))))).
thf(tp_c_2EintegerRing_2Eint__r__canonical__sum__scalar2,type,(c_2EintegerRing_2Eint__r__canonical__sum__scalar2:$i)).
thf(mem_c_2EintegerRing_2Eint__r__canonical__sum__scalar2,axiom,(mem@c_2EintegerRing_2Eint__r__canonical__sum__scalar2@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@(arr@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint)@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint))))).
thf(tp_c_2EintegerRing_2Eint__r__canonical__sum__scalar3,type,(c_2EintegerRing_2Eint__r__canonical__sum__scalar3:$i)).
thf(mem_c_2EintegerRing_2Eint__r__canonical__sum__scalar3,axiom,(mem@c_2EintegerRing_2Eint__r__canonical__sum__scalar3@(arr@ty_2Einteger_2Eint@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@(arr@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint)@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint)))))).
thf(tp_c_2EintegerRing_2Eint__r__canonical__sum__simplify,type,(c_2EintegerRing_2Eint__r__canonical__sum__simplify:$i)).
thf(mem_c_2EintegerRing_2Eint__r__canonical__sum__simplify,axiom,(mem@c_2EintegerRing_2Eint__r__canonical__sum__simplify@(arr@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint)@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint)))).
thf(tp_c_2EintegerRing_2Eint__r__ics__aux,type,(c_2EintegerRing_2Eint__r__ics__aux:$i)).
thf(mem_c_2EintegerRing_2Eint__r__ics__aux,axiom,(mem@c_2EintegerRing_2Eint__r__ics__aux@(arr@(ty_2Equote_2Evarmap@ty_2Einteger_2Eint)@(arr@ty_2Einteger_2Eint@(arr@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint)@ty_2Einteger_2Eint))))).
thf(stp_fo_c_2EintegerRing_2Eint__r__ics__aux,type,(fo__c_2EintegerRing_2Eint__r__ics__aux:(tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint > (tp__ty_2Einteger_2Eint > (tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint > tp__ty_2Einteger_2Eint))))).
thf(stp_eq_fo_c_2EintegerRing_2Eint__r__ics__aux,axiom,( ! [X0:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : ( ! [X1:tp__ty_2Einteger_2Eint] : ( ! [X2:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ((inj__ty_2Einteger_2Eint @ (((fo__c_2EintegerRing_2Eint__r__ics__aux @ X0) @ X1) @ X2)) = (ap @ (ap @ (ap @ c_2EintegerRing_2Eint__r__ics__aux @ (inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ X0)) @ (inj__ty_2Einteger_2Eint @ X1)) @ (inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ X2))))))).
thf(tp_c_2EintegerRing_2Eint__r__interp__cs,type,(c_2EintegerRing_2Eint__r__interp__cs:$i)).
thf(mem_c_2EintegerRing_2Eint__r__interp__cs,axiom,(mem@c_2EintegerRing_2Eint__r__interp__cs@(arr@(ty_2Equote_2Evarmap@ty_2Einteger_2Eint)@(arr@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint)@ty_2Einteger_2Eint)))).
thf(stp_fo_c_2EintegerRing_2Eint__r__interp__cs,type,(fo__c_2EintegerRing_2Eint__r__interp__cs:(tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint > (tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint > tp__ty_2Einteger_2Eint)))).
thf(stp_eq_fo_c_2EintegerRing_2Eint__r__interp__cs,axiom,( ! [X0:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : ( ! [X1:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ((inj__ty_2Einteger_2Eint @ ((fo__c_2EintegerRing_2Eint__r__interp__cs @ X0) @ X1)) = (ap @ (ap @ c_2EintegerRing_2Eint__r__interp__cs @ (inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ X0)) @ (inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ X1)))))).
thf(tp_c_2EintegerRing_2Eint__r__interp__m,type,(c_2EintegerRing_2Eint__r__interp__m:$i)).
thf(mem_c_2EintegerRing_2Eint__r__interp__m,axiom,(mem@c_2EintegerRing_2Eint__r__interp__m@(arr@(ty_2Equote_2Evarmap@ty_2Einteger_2Eint)@(arr@ty_2Einteger_2Eint@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@ty_2Einteger_2Eint))))).
thf(stp_fo_c_2EintegerRing_2Eint__r__interp__m,type,(fo__c_2EintegerRing_2Eint__r__interp__m:(tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint > (tp__ty_2Einteger_2Eint > (tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex > tp__ty_2Einteger_2Eint))))).
thf(stp_eq_fo_c_2EintegerRing_2Eint__r__interp__m,axiom,( ! [X0:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : ( ! [X1:tp__ty_2Einteger_2Eint] : ( ! [X2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((inj__ty_2Einteger_2Eint @ (((fo__c_2EintegerRing_2Eint__r__interp__m @ X0) @ X1) @ X2)) = (ap @ (ap @ (ap @ c_2EintegerRing_2Eint__r__interp__m @ (inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ X0)) @ (inj__ty_2Einteger_2Eint @ X1)) @ (inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ X2))))))).
thf(stp_c_ty_2Ecanonical_2Espolynom_ty_2Einteger_2Eint,type,(tp__c_ty_2Ecanonical_2Espolynom_ty_2Einteger_2Eint : $tType)).
thf(stp_inj_c_ty_2Ecanonical_2Espolynom_ty_2Einteger_2Eint,type,(inj__c_ty_2Ecanonical_2Espolynom_ty_2Einteger_2Eint : (tp__c_ty_2Ecanonical_2Espolynom_ty_2Einteger_2Eint > $i))).
thf(stp_surj_c_ty_2Ecanonical_2Espolynom_ty_2Einteger_2Eint,type,(surj__c_ty_2Ecanonical_2Espolynom_ty_2Einteger_2Eint : ($i > tp__c_ty_2Ecanonical_2Espolynom_ty_2Einteger_2Eint))).
thf(stp_inj_surj_c_ty_2Ecanonical_2Espolynom_ty_2Einteger_2Eint,axiom,( ! [X:tp__c_ty_2Ecanonical_2Espolynom_ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Espolynom_ty_2Einteger_2Eint @ (inj__c_ty_2Ecanonical_2Espolynom_ty_2Einteger_2Eint @ X)) = X))).
thf(stp_inj_mem_c_ty_2Ecanonical_2Espolynom_ty_2Einteger_2Eint,axiom,( ! [X:tp__c_ty_2Ecanonical_2Espolynom_ty_2Einteger_2Eint] : (mem @ (inj__c_ty_2Ecanonical_2Espolynom_ty_2Einteger_2Eint @ X) @ (ty_2Ecanonical_2Espolynom@ty_2Einteger_2Eint)))).
thf(stp_iso_mem_c_ty_2Ecanonical_2Espolynom_ty_2Einteger_2Eint,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Ecanonical_2Espolynom@ty_2Einteger_2Eint)) => (X = (inj__c_ty_2Ecanonical_2Espolynom_ty_2Einteger_2Eint @ (surj__c_ty_2Ecanonical_2Espolynom_ty_2Einteger_2Eint @ X)))))).
thf(tp_c_2EintegerRing_2Eint__r__interp__sp,type,(c_2EintegerRing_2Eint__r__interp__sp:$i)).
thf(mem_c_2EintegerRing_2Eint__r__interp__sp,axiom,(mem@c_2EintegerRing_2Eint__r__interp__sp@(arr@(ty_2Equote_2Evarmap@ty_2Einteger_2Eint)@(arr@(ty_2Ecanonical_2Espolynom@ty_2Einteger_2Eint)@ty_2Einteger_2Eint)))).
thf(stp_fo_c_2EintegerRing_2Eint__r__interp__sp,type,(fo__c_2EintegerRing_2Eint__r__interp__sp:(tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint > (tp__c_ty_2Ecanonical_2Espolynom_ty_2Einteger_2Eint > tp__ty_2Einteger_2Eint)))).
thf(stp_eq_fo_c_2EintegerRing_2Eint__r__interp__sp,axiom,( ! [X0:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : ( ! [X1:tp__c_ty_2Ecanonical_2Espolynom_ty_2Einteger_2Eint] : ((inj__ty_2Einteger_2Eint @ ((fo__c_2EintegerRing_2Eint__r__interp__sp @ X0) @ X1)) = (ap @ (ap @ c_2EintegerRing_2Eint__r__interp__sp @ (inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ X0)) @ (inj__c_ty_2Ecanonical_2Espolynom_ty_2Einteger_2Eint @ X1)))))).
thf(tp_c_2EintegerRing_2Eint__r__interp__vl,type,(c_2EintegerRing_2Eint__r__interp__vl:$i)).
thf(mem_c_2EintegerRing_2Eint__r__interp__vl,axiom,(mem@c_2EintegerRing_2Eint__r__interp__vl@(arr@(ty_2Equote_2Evarmap@ty_2Einteger_2Eint)@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@ty_2Einteger_2Eint)))).
thf(stp_fo_c_2EintegerRing_2Eint__r__interp__vl,type,(fo__c_2EintegerRing_2Eint__r__interp__vl:(tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint > (tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex > tp__ty_2Einteger_2Eint)))).
thf(stp_eq_fo_c_2EintegerRing_2Eint__r__interp__vl,axiom,( ! [X0:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : ( ! [X1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((inj__ty_2Einteger_2Eint @ ((fo__c_2EintegerRing_2Eint__r__interp__vl @ X0) @ X1)) = (ap @ (ap @ c_2EintegerRing_2Eint__r__interp__vl @ (inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ X0)) @ (inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ X1)))))).
thf(tp_c_2EintegerRing_2Eint__r__ivl__aux,type,(c_2EintegerRing_2Eint__r__ivl__aux:$i)).
thf(mem_c_2EintegerRing_2Eint__r__ivl__aux,axiom,(mem@c_2EintegerRing_2Eint__r__ivl__aux@(arr@(ty_2Equote_2Evarmap@ty_2Einteger_2Eint)@(arr@ty_2Equote_2Eindex@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@ty_2Einteger_2Eint))))).
thf(stp_fo_c_2EintegerRing_2Eint__r__ivl__aux,type,(fo__c_2EintegerRing_2Eint__r__ivl__aux:(tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint > (tp__ty_2Equote_2Eindex > (tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex > tp__ty_2Einteger_2Eint))))).
thf(stp_eq_fo_c_2EintegerRing_2Eint__r__ivl__aux,axiom,( ! [X0:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : ( ! [X1:tp__ty_2Equote_2Eindex] : ( ! [X2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((inj__ty_2Einteger_2Eint @ (((fo__c_2EintegerRing_2Eint__r__ivl__aux @ X0) @ X1) @ X2)) = (ap @ (ap @ (ap @ c_2EintegerRing_2Eint__r__ivl__aux @ (inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ X0)) @ (inj__ty_2Equote_2Eindex @ X1)) @ (inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ X2))))))).
thf(tp_c_2EintegerRing_2Eint__r__monom__insert,type,(c_2EintegerRing_2Eint__r__monom__insert:$i)).
thf(mem_c_2EintegerRing_2Eint__r__monom__insert,axiom,(mem@c_2EintegerRing_2Eint__r__monom__insert@(arr@ty_2Einteger_2Eint@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@(arr@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint)@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint)))))).
thf(tp_c_2EintegerRing_2Eint__r__spolynom__normalize,type,(c_2EintegerRing_2Eint__r__spolynom__normalize:$i)).
thf(mem_c_2EintegerRing_2Eint__r__spolynom__normalize,axiom,(mem@c_2EintegerRing_2Eint__r__spolynom__normalize@(arr@(ty_2Ecanonical_2Espolynom@ty_2Einteger_2Eint)@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint)))).
thf(tp_c_2EintegerRing_2Eint__r__spolynom__simplify,type,(c_2EintegerRing_2Eint__r__spolynom__simplify:$i)).
thf(mem_c_2EintegerRing_2Eint__r__spolynom__simplify,axiom,(mem@c_2EintegerRing_2Eint__r__spolynom__simplify@(arr@(ty_2Ecanonical_2Espolynom@ty_2Einteger_2Eint)@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint)))).
thf(tp_c_2EintegerRing_2Eint__r__varlist__insert,type,(c_2EintegerRing_2Eint__r__varlist__insert:$i)).
thf(mem_c_2EintegerRing_2Eint__r__varlist__insert,axiom,(mem@c_2EintegerRing_2Eint__r__varlist__insert@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@(arr@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint)@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint))))).
thf(conj_thm_2EintegerRing_2Eint__is__ring,lemma,(p@(ap@(c_2Ering_2Eis__ring@ty_2Einteger_2Eint)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__0))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1))@c_2Einteger_2Eint__add)@c_2Einteger_2Eint__mul)@c_2Einteger_2Eint__neg)))).
thf(ax_thm_2EintegerRing_2Eint__interp__p__def,axiom,(c_2EintegerRing_2Eint__interp__p = (ap@(c_2EringNorm_2Einterp__p@ty_2Einteger_2Eint)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__0))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1))@c_2Einteger_2Eint__add)@c_2Einteger_2Eint__mul)@c_2Einteger_2Eint__neg)))).
thf(ax_thm_2EintegerRing_2Eint__polynom__simplify__def,axiom,(c_2EintegerRing_2Eint__polynom__simplify = (ap@(c_2EringNorm_2Epolynom__simplify@ty_2Einteger_2Eint)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__0))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1))@c_2Einteger_2Eint__add)@c_2Einteger_2Eint__mul)@c_2Einteger_2Eint__neg)))).
thf(ax_thm_2EintegerRing_2Eint__polynom__normalize__def,axiom,(c_2EintegerRing_2Eint__polynom__normalize = (ap@(c_2EringNorm_2Epolynom__normalize@ty_2Einteger_2Eint)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__0))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1))@c_2Einteger_2Eint__add)@c_2Einteger_2Eint__mul)@c_2Einteger_2Eint__neg)))).
thf(ax_thm_2EintegerRing_2Eint__r__canonical__sum__merge__def,axiom,(c_2EintegerRing_2Eint__r__canonical__sum__merge = (ap@(c_2EringNorm_2Er__canonical__sum__merge@ty_2Einteger_2Eint)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__0))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1))@c_2Einteger_2Eint__add)@c_2Einteger_2Eint__mul)@c_2Einteger_2Eint__neg)))).
thf(ax_thm_2EintegerRing_2Eint__r__monom__insert__def,axiom,(c_2EintegerRing_2Eint__r__monom__insert = (ap@(c_2EringNorm_2Er__monom__insert@ty_2Einteger_2Eint)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__0))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1))@c_2Einteger_2Eint__add)@c_2Einteger_2Eint__mul)@c_2Einteger_2Eint__neg)))).
thf(ax_thm_2EintegerRing_2Eint__r__varlist__insert__def,axiom,(c_2EintegerRing_2Eint__r__varlist__insert = (ap@(c_2EringNorm_2Er__varlist__insert@ty_2Einteger_2Eint)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__0))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1))@c_2Einteger_2Eint__add)@c_2Einteger_2Eint__mul)@c_2Einteger_2Eint__neg)))).
thf(ax_thm_2EintegerRing_2Eint__r__canonical__sum__scalar__def,axiom,(c_2EintegerRing_2Eint__r__canonical__sum__scalar = (ap@(c_2EringNorm_2Er__canonical__sum__scalar@ty_2Einteger_2Eint)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__0))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1))@c_2Einteger_2Eint__add)@c_2Einteger_2Eint__mul)@c_2Einteger_2Eint__neg)))).
thf(ax_thm_2EintegerRing_2Eint__r__canonical__sum__scalar2__def,axiom,(c_2EintegerRing_2Eint__r__canonical__sum__scalar2 = (ap@(c_2EringNorm_2Er__canonical__sum__scalar2@ty_2Einteger_2Eint)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__0))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1))@c_2Einteger_2Eint__add)@c_2Einteger_2Eint__mul)@c_2Einteger_2Eint__neg)))).
thf(ax_thm_2EintegerRing_2Eint__r__canonical__sum__scalar3__def,axiom,(c_2EintegerRing_2Eint__r__canonical__sum__scalar3 = (ap@(c_2EringNorm_2Er__canonical__sum__scalar3@ty_2Einteger_2Eint)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__0))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1))@c_2Einteger_2Eint__add)@c_2Einteger_2Eint__mul)@c_2Einteger_2Eint__neg)))).
thf(ax_thm_2EintegerRing_2Eint__r__canonical__sum__prod__def,axiom,(c_2EintegerRing_2Eint__r__canonical__sum__prod = (ap@(c_2EringNorm_2Er__canonical__sum__prod@ty_2Einteger_2Eint)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__0))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1))@c_2Einteger_2Eint__add)@c_2Einteger_2Eint__mul)@c_2Einteger_2Eint__neg)))).
thf(ax_thm_2EintegerRing_2Eint__r__canonical__sum__simplify__def,axiom,(c_2EintegerRing_2Eint__r__canonical__sum__simplify = (ap@(c_2EringNorm_2Er__canonical__sum__simplify@ty_2Einteger_2Eint)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__0))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1))@c_2Einteger_2Eint__add)@c_2Einteger_2Eint__mul)@c_2Einteger_2Eint__neg)))).
thf(ax_thm_2EintegerRing_2Eint__r__ivl__aux__def,axiom,(c_2EintegerRing_2Eint__r__ivl__aux = (ap@(c_2EringNorm_2Er__ivl__aux@ty_2Einteger_2Eint)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__0))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1))@c_2Einteger_2Eint__add)@c_2Einteger_2Eint__mul)@c_2Einteger_2Eint__neg)))).
thf(ax_thm_2EintegerRing_2Eint__r__interp__vl__def,axiom,(c_2EintegerRing_2Eint__r__interp__vl = (ap@(c_2EringNorm_2Er__interp__vl@ty_2Einteger_2Eint)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__0))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1))@c_2Einteger_2Eint__add)@c_2Einteger_2Eint__mul)@c_2Einteger_2Eint__neg)))).
thf(ax_thm_2EintegerRing_2Eint__r__interp__m__def,axiom,(c_2EintegerRing_2Eint__r__interp__m = (ap@(c_2EringNorm_2Er__interp__m@ty_2Einteger_2Eint)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__0))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1))@c_2Einteger_2Eint__add)@c_2Einteger_2Eint__mul)@c_2Einteger_2Eint__neg)))).
thf(ax_thm_2EintegerRing_2Eint__r__ics__aux__def,axiom,(c_2EintegerRing_2Eint__r__ics__aux = (ap@(c_2EringNorm_2Er__ics__aux@ty_2Einteger_2Eint)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__0))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1))@c_2Einteger_2Eint__add)@c_2Einteger_2Eint__mul)@c_2Einteger_2Eint__neg)))).
thf(ax_thm_2EintegerRing_2Eint__r__interp__cs__def,axiom,(c_2EintegerRing_2Eint__r__interp__cs = (ap@(c_2EringNorm_2Er__interp__cs@ty_2Einteger_2Eint)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__0))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1))@c_2Einteger_2Eint__add)@c_2Einteger_2Eint__mul)@c_2Einteger_2Eint__neg)))).
thf(ax_thm_2EintegerRing_2Eint__r__spolynom__normalize__def,axiom,(c_2EintegerRing_2Eint__r__spolynom__normalize = (ap@(c_2EringNorm_2Er__spolynom__normalize@ty_2Einteger_2Eint)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__0))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1))@c_2Einteger_2Eint__add)@c_2Einteger_2Eint__mul)@c_2Einteger_2Eint__neg)))).
thf(ax_thm_2EintegerRing_2Eint__r__spolynom__simplify__def,axiom,(c_2EintegerRing_2Eint__r__spolynom__simplify = (ap@(c_2EringNorm_2Er__spolynom__simplify@ty_2Einteger_2Eint)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__0))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1))@c_2Einteger_2Eint__add)@c_2Einteger_2Eint__mul)@c_2Einteger_2Eint__neg)))).
thf(ax_thm_2EintegerRing_2Eint__r__interp__sp__def,axiom,(c_2EintegerRing_2Eint__r__interp__sp = (ap@(c_2EringNorm_2Er__interp__sp@ty_2Einteger_2Eint)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__0))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1))@c_2Einteger_2Eint__add)@c_2Einteger_2Eint__mul)@c_2Einteger_2Eint__neg)))).
thf(conj_thm_2EintegerRing_2Eint__ring__thms,conjecture,( ! [A_27a:del]: ((p@(ap@(c_2Ering_2Eis__ring@ty_2Einteger_2Eint)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__0))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1))@c_2Einteger_2Eint__add)@c_2Einteger_2Eint__mul)@c_2Einteger_2Eint__neg))) & (( ! [V0vm:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : ( ! [V1p:tp__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__interp__p@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V0vm))@(inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ V1p))) = (surj__ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__interp__cs@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V0vm))@(ap@c_2EintegerRing_2Eint__polynom__simplify@(inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ V1p))))))) & (((( ! [V2vm:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : ( ! [V3c:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__interp__p@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V2vm))@(ap@(c_2EringNorm_2EPconst@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V3c)))) = V3c))) & (( ! [V4vm:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : ( ! [V5i:tp__ty_2Equote_2Eindex] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__interp__p@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V4vm))@(ap@(c_2EringNorm_2EPvar@ty_2Einteger_2Eint)@(inj__ty_2Equote_2Eindex @ V5i)))) = (surj__ty_2Einteger_2Eint @ (ap@(ap@(c_2Equote_2Evarmap__find@ty_2Einteger_2Eint)@(inj__ty_2Equote_2Eindex @ V5i))@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V4vm)))))) & (( ! [V6vm:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : ( ! [V7p1:tp__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint] : ( ! [V8p2:tp__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__interp__p@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V6vm))@(ap@(ap@(c_2EringNorm_2EPplus@ty_2Einteger_2Eint)@(inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ V7p1))@(inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ V8p2)))) = (surj__ty_2Einteger_2Eint @ (ap@(ap@c_2Einteger_2Eint__add@(ap@(ap@c_2EintegerRing_2Eint__interp__p@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V6vm))@(inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ V7p1)))@(ap@(ap@c_2EintegerRing_2Eint__interp__p@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V6vm))@(inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ V8p2)))))))) & (( ! [V9vm:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : ( ! [V10p1:tp__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint] : ( ! [V11p2:tp__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__interp__p@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V9vm))@(ap@(ap@(c_2EringNorm_2EPmult@ty_2Einteger_2Eint)@(inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ V10p1))@(inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ V11p2)))) = (surj__ty_2Einteger_2Eint @ (ap@(ap@c_2Einteger_2Eint__mul@(ap@(ap@c_2EintegerRing_2Eint__interp__p@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V9vm))@(inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ V10p1)))@(ap@(ap@c_2EintegerRing_2Eint__interp__p@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V9vm))@(inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ V11p2)))))))) & ( ! [V12vm:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : ( ! [V13p1:tp__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__interp__p@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V12vm))@(ap@(c_2EringNorm_2EPopp@ty_2Einteger_2Eint)@(inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ V13p1)))) = (surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__neg@(ap@(ap@c_2EintegerRing_2Eint__interp__p@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V12vm))@(inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ V13p1))))))))))) & (( ! [V14x:$i] : ((mem@V14x@A_27a) => ( ! [V15v2:$i] : ((mem@V15v2@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V16v1:$i] : ((mem@V16v1@(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)@V14x)@V16v1)@V15v2)) = V14x))))))) & (( ! [V17x:$i] : ((mem@V17x@A_27a) => ( ! [V18v2:$i] : ((mem@V18v2@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V19v1:$i] : ((mem@V19v1@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V20i1:tp__ty_2Equote_2Eindex] : ((ap@(ap@(c_2Equote_2Evarmap__find@A_27a)@(ap@c_2Equote_2ERight__idx@(inj__ty_2Equote_2Eindex @ V20i1)))@(ap@(ap@(ap@(c_2Equote_2ENode__vm@A_27a)@V17x)@V19v1)@V18v2)) = (ap@(ap@(c_2Equote_2Evarmap__find@A_27a)@(inj__ty_2Equote_2Eindex @ V20i1))@V18v2))))))))) & (( ! [V21x:$i] : ((mem@V21x@A_27a) => ( ! [V22v2:$i] : ((mem@V22v2@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V23v1:$i] : ((mem@V23v1@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V24i1:tp__ty_2Equote_2Eindex] : ((ap@(ap@(c_2Equote_2Evarmap__find@A_27a)@(ap@c_2Equote_2ELeft__idx@(inj__ty_2Equote_2Eindex @ V24i1)))@(ap@(ap@(ap@(c_2Equote_2ENode__vm@A_27a)@V21x)@V23v1)@V22v2)) = (ap@(ap@(c_2Equote_2Evarmap__find@A_27a)@(inj__ty_2Equote_2Eindex @ V24i1))@V23v1))))))))) & ( ! [V25i:tp__ty_2Equote_2Eindex] : ((ap@(ap@(c_2Equote_2Evarmap__find@A_27a)@(inj__ty_2Equote_2Eindex @ V25i))@(c_2Equote_2EEmpty__vm@A_27a)) = (ap@(c_2Emin_2E_40@A_27a)@(lam@A_27a@(^ [V26x:$i] : c_2Ebool_2ET))))))))) & ((( ! [V27t2:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ( ! [V28t1:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ( ! [V29l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V30l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V31c2:tp__ty_2Einteger_2Eint] : ( ! [V32c1:tp__ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__merge@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V32c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V30l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V28t1)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V31c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V29l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V27t2)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(ap@(ap@(c_2EternaryComparisons_2Eordering__CASE@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint))@(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 @ V30l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V29l2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V32c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V30l1))@(ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__merge@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V28t1))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V31c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V29l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V27t2)))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(ap@(ap@c_2Einteger_2Eint__add@(inj__ty_2Einteger_2Eint @ V32c1))@(inj__ty_2Einteger_2Eint @ V31c2)))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V30l1))@(ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__merge@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V28t1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V27t2))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V31c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V29l2))@(ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__merge@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V32c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V30l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V28t1)))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V27t2)))))))))))) & (( ! [V33t2:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ( ! [V34t1:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ( ! [V35l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V36l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V37c1:tp__ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__merge@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V37c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V36l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V34t1)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V35l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V33t2)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(ap@(ap@(c_2EternaryComparisons_2Eordering__CASE@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint))@(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 @ V36l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V35l2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V37c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V36l1))@(ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__merge@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V34t1))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V35l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V33t2)))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(ap@(ap@c_2Einteger_2Eint__add@(inj__ty_2Einteger_2Eint @ V37c1))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1)))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V36l1))@(ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__merge@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V34t1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V33t2))))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V35l2))@(ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__merge@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V37c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V36l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V34t1)))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V33t2))))))))))) & (( ! [V38t2:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ( ! [V39t1:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ( ! [V40l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V41l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V42c2:tp__ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__merge@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V41l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V39t1)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V42c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V40l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V38t2)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(ap@(ap@(c_2EternaryComparisons_2Eordering__CASE@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint))@(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 @ V41l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V40l2)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V41l1))@(ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__merge@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V39t1))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V42c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V40l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V38t2)))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(ap@(ap@c_2Einteger_2Eint__add@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1))@(inj__ty_2Einteger_2Eint @ V42c2)))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V41l1))@(ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__merge@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V39t1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V38t2))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V42c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V40l2))@(ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__merge@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V41l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V39t1)))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V38t2))))))))))) & (( ! [V43t2:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ( ! [V44t1:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ( ! [V45l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V46l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__merge@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V46l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V44t1)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V45l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V43t2)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(ap@(ap@(c_2EternaryComparisons_2Eordering__CASE@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint))@(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 @ V46l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V45l2)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V46l1))@(ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__merge@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V44t1))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V45l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V43t2)))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(ap@(ap@c_2Einteger_2Eint__add@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1)))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V46l1))@(ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__merge@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V44t1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V43t2))))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V45l2))@(ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__merge@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V46l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V44t1)))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V43t2)))))))))) & (( ! [V47s1:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__merge@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V47s1))@(c_2Ecanonical_2ENil__monom@ty_2Einteger_2Eint))) = V47s1)) & (( ! [V48v6:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ( ! [V49v5:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V50v4:tp__ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__merge@(c_2Ecanonical_2ENil__monom@ty_2Einteger_2Eint))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V50v4))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V49v5))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V48v6)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V50v4))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V49v5))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V48v6))))))) & ( ! [V51v8:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ( ! [V52v7:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__merge@(c_2Ecanonical_2ENil__monom@ty_2Einteger_2Eint))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V52v7))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V51v8)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V52v7))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V51v8)))))))))))) & ((( ! [V53t2:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ( ! [V54l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V55l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V56c2:tp__ty_2Einteger_2Eint] : ( ! [V57c1:tp__ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(ap@c_2EintegerRing_2Eint__r__monom__insert@(inj__ty_2Einteger_2Eint @ V57c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V55l1))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V56c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V54l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V53t2)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(ap@(ap@(c_2EternaryComparisons_2Eordering__CASE@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint))@(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 @ V55l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V54l2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V57c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V55l1))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V56c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V54l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V53t2))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(ap@(ap@c_2Einteger_2Eint__add@(inj__ty_2Einteger_2Eint @ V57c1))@(inj__ty_2Einteger_2Eint @ V56c2)))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V55l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V53t2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V56c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V54l2))@(ap@(ap@(ap@c_2EintegerRing_2Eint__r__monom__insert@(inj__ty_2Einteger_2Eint @ V57c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V55l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V53t2))))))))))) & (( ! [V58t2:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ( ! [V59l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V60l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V61c1:tp__ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(ap@c_2EintegerRing_2Eint__r__monom__insert@(inj__ty_2Einteger_2Eint @ V61c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V60l1))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V59l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V58t2)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(ap@(ap@(c_2EternaryComparisons_2Eordering__CASE@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint))@(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 @ V60l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V59l2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V61c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V60l1))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V59l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V58t2))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(ap@(ap@c_2Einteger_2Eint__add@(inj__ty_2Einteger_2Eint @ V61c1))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1)))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V60l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V58t2)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V59l2))@(ap@(ap@(ap@c_2EintegerRing_2Eint__r__monom__insert@(inj__ty_2Einteger_2Eint @ V61c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V60l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V58t2)))))))))) & ( ! [V62l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V63c1:tp__ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(ap@c_2EintegerRing_2Eint__r__monom__insert@(inj__ty_2Einteger_2Eint @ V63c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V62l1))@(c_2Ecanonical_2ENil__monom@ty_2Einteger_2Eint))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V63c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V62l1))@(c_2Ecanonical_2ENil__monom@ty_2Einteger_2Eint)))))))) & ((( ! [V64t2:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ( ! [V65l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V66l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V67c2:tp__ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__varlist__insert@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V66l1))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V67c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V65l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V64t2)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(ap@(ap@(c_2EternaryComparisons_2Eordering__CASE@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint))@(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 @ V66l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V65l2)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V66l1))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V67c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V65l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V64t2))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(ap@(ap@c_2Einteger_2Eint__add@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1))@(inj__ty_2Einteger_2Eint @ V67c2)))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V66l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V64t2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V67c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V65l2))@(ap@(ap@c_2EintegerRing_2Eint__r__varlist__insert@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V66l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V64t2)))))))))) & (( ! [V68t2:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ( ! [V69l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V70l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__varlist__insert@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V70l1))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V69l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V68t2)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(ap@(ap@(c_2EternaryComparisons_2Eordering__CASE@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint))@(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 @ V70l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V69l2)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V70l1))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V69l2))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V68t2))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(ap@(ap@c_2Einteger_2Eint__add@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1)))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V70l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V68t2)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V69l2))@(ap@(ap@c_2EintegerRing_2Eint__r__varlist__insert@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V70l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V68t2))))))))) & ( ! [V71l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__varlist__insert@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V71l1))@(c_2Ecanonical_2ENil__monom@ty_2Einteger_2Eint))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V71l1))@(c_2Ecanonical_2ENil__monom@ty_2Einteger_2Eint))))))) & ((( ! [V72c0:tp__ty_2Einteger_2Eint] : ( ! [V73c:tp__ty_2Einteger_2Eint] : ( ! [V74l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V75t:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__scalar@(inj__ty_2Einteger_2Eint @ V72c0))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V73c))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V74l))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V75t)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(ap@(ap@c_2Einteger_2Eint__mul@(inj__ty_2Einteger_2Eint @ V72c0))@(inj__ty_2Einteger_2Eint @ V73c)))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V74l))@(ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__scalar@(inj__ty_2Einteger_2Eint @ V72c0))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V75t))))))))) & (( ! [V76c0:tp__ty_2Einteger_2Eint] : ( ! [V77l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V78t:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__scalar@(inj__ty_2Einteger_2Eint @ V76c0))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V77l))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V78t)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V76c0))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V77l))@(ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__scalar@(inj__ty_2Einteger_2Eint @ V76c0))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V78t)))))))) & ( ! [V79c0:tp__ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__scalar@(inj__ty_2Einteger_2Eint @ V79c0))@(c_2Ecanonical_2ENil__monom@ty_2Einteger_2Eint))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (c_2Ecanonical_2ENil__monom@ty_2Einteger_2Eint)))))) & ((( ! [V80l0:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V81c:tp__ty_2Einteger_2Eint] : ( ! [V82l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V83t:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__scalar2@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V80l0))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V81c))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V82l))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V83t)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(ap@c_2EintegerRing_2Eint__r__monom__insert@(inj__ty_2Einteger_2Eint @ V81c))@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__merge@ty_2Equote_2Eindex)@c_2Equote_2Eindex__lt)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V80l0))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V82l)))@(ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__scalar2@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V80l0))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V83t))))))))) & (( ! [V84l0:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V85l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V86t:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__scalar2@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V84l0))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V85l))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V86t)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__varlist__insert@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__merge@ty_2Equote_2Eindex)@c_2Equote_2Eindex__lt)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V84l0))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V85l)))@(ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__scalar2@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V84l0))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V86t)))))))) & ( ! [V87l0:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__scalar2@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V87l0))@(c_2Ecanonical_2ENil__monom@ty_2Einteger_2Eint))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (c_2Ecanonical_2ENil__monom@ty_2Einteger_2Eint)))))) & ((( ! [V88c0:tp__ty_2Einteger_2Eint] : ( ! [V89l0:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V90c:tp__ty_2Einteger_2Eint] : ( ! [V91l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V92t:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__scalar3@(inj__ty_2Einteger_2Eint @ V88c0))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V89l0))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V90c))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V91l))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V92t)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(ap@c_2EintegerRing_2Eint__r__monom__insert@(ap@(ap@c_2Einteger_2Eint__mul@(inj__ty_2Einteger_2Eint @ V88c0))@(inj__ty_2Einteger_2Eint @ V90c)))@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__merge@ty_2Equote_2Eindex)@c_2Equote_2Eindex__lt)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V89l0))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V91l)))@(ap@(ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__scalar3@(inj__ty_2Einteger_2Eint @ V88c0))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V89l0))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V92t)))))))))) & (( ! [V93c0:tp__ty_2Einteger_2Eint] : ( ! [V94l0:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V95l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V96t:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__scalar3@(inj__ty_2Einteger_2Eint @ V93c0))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V94l0))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V95l))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V96t)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(ap@c_2EintegerRing_2Eint__r__monom__insert@(inj__ty_2Einteger_2Eint @ V93c0))@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__merge@ty_2Equote_2Eindex)@c_2Equote_2Eindex__lt)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V94l0))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V95l)))@(ap@(ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__scalar3@(inj__ty_2Einteger_2Eint @ V93c0))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V94l0))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V96t))))))))) & ( ! [V97c0:tp__ty_2Einteger_2Eint] : ( ! [V98l0:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__scalar3@(inj__ty_2Einteger_2Eint @ V97c0))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V98l0))@(c_2Ecanonical_2ENil__monom@ty_2Einteger_2Eint))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (c_2Ecanonical_2ENil__monom@ty_2Einteger_2Eint))))))) & ((( ! [V99c1:tp__ty_2Einteger_2Eint] : ( ! [V100l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V101t1:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ( ! [V102s2:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__prod@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V99c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V100l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V101t1)))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V102s2))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__merge@(ap@(ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__scalar3@(inj__ty_2Einteger_2Eint @ V99c1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V100l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V102s2)))@(ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__prod@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V101t1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V102s2))))))))) & (( ! [V103l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V104t1:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ( ! [V105s2:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__prod@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V103l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V104t1)))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V105s2))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__merge@(ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__scalar2@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V103l1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V105s2)))@(ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__prod@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V104t1))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V105s2)))))))) & ( ! [V106s2:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__prod@(c_2Ecanonical_2ENil__monom@ty_2Einteger_2Eint))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V106s2))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (c_2Ecanonical_2ENil__monom@ty_2Einteger_2Eint)))))) & ((( ! [V107c:tp__ty_2Einteger_2Eint] : ( ! [V108l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V109t:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@c_2EintegerRing_2Eint__r__canonical__sum__simplify@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V107c))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V108l))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V109t)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Emin_2E_3D@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V107c))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__0)))@(ap@c_2EintegerRing_2Eint__r__canonical__sum__simplify@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V109t)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Ecanonical_2Ecanonical__sum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Emin_2E_3D@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V107c))@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V108l))@(ap@c_2EintegerRing_2Eint__r__canonical__sum__simplify@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V109t))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V107c))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V108l))@(ap@c_2EintegerRing_2Eint__r__canonical__sum__simplify@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V109t)))))))))) & (( ! [V110l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V111t:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@c_2EintegerRing_2Eint__r__canonical__sum__simplify@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V110l))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V111t)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V110l))@(ap@c_2EintegerRing_2Eint__r__canonical__sum__simplify@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V111t))))))) & ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@c_2EintegerRing_2Eint__r__canonical__sum__simplify@(c_2Ecanonical_2ENil__monom@ty_2Einteger_2Eint))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (c_2Ecanonical_2ENil__monom@ty_2Einteger_2Eint))))) & ((( ! [V112vm:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : ( ! [V113x:tp__ty_2Equote_2Eindex] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@(ap@c_2EintegerRing_2Eint__r__ivl__aux@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V112vm))@(inj__ty_2Equote_2Eindex @ V113x))@(c_2Elist_2ENIL@ty_2Equote_2Eindex))) = (surj__ty_2Einteger_2Eint @ (ap@(ap@(c_2Equote_2Evarmap__find@ty_2Einteger_2Eint)@(inj__ty_2Equote_2Eindex @ V113x))@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V112vm)))))) & ( ! [V114vm:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : ( ! [V115x:tp__ty_2Equote_2Eindex] : ( ! [V116x_27:tp__ty_2Equote_2Eindex] : ( ! [V117t_27:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@(ap@c_2EintegerRing_2Eint__r__ivl__aux@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V114vm))@(inj__ty_2Equote_2Eindex @ V115x))@(ap@(ap@(c_2Elist_2ECONS@ty_2Equote_2Eindex)@(inj__ty_2Equote_2Eindex @ V116x_27))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V117t_27)))) = (surj__ty_2Einteger_2Eint @ (ap@(ap@c_2Einteger_2Eint__mul@(ap@(ap@(c_2Equote_2Evarmap__find@ty_2Einteger_2Eint)@(inj__ty_2Equote_2Eindex @ V115x))@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V114vm)))@(ap@(ap@(ap@c_2EintegerRing_2Eint__r__ivl__aux@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V114vm))@(inj__ty_2Equote_2Eindex @ V116x_27))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V117t_27)))))))))) & ((( ! [V118vm:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__interp__vl@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V118vm))@(c_2Elist_2ENIL@ty_2Equote_2Eindex))) = fo__c_2Einteger_2Eint__1)) & ( ! [V119vm:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : ( ! [V120x:tp__ty_2Equote_2Eindex] : ( ! [V121t:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__interp__vl@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V119vm))@(ap@(ap@(c_2Elist_2ECONS@ty_2Equote_2Eindex)@(inj__ty_2Equote_2Eindex @ V120x))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V121t)))) = (surj__ty_2Einteger_2Eint @ (ap@(ap@(ap@c_2EintegerRing_2Eint__r__ivl__aux@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V119vm))@(inj__ty_2Equote_2Eindex @ V120x))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V121t)))))))) & ((( ! [V122vm:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : ( ! [V123c:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@(ap@c_2EintegerRing_2Eint__r__interp__m@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V122vm))@(inj__ty_2Einteger_2Eint @ V123c))@(c_2Elist_2ENIL@ty_2Equote_2Eindex))) = V123c))) & ( ! [V124vm:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : ( ! [V125c:tp__ty_2Einteger_2Eint] : ( ! [V126x:tp__ty_2Equote_2Eindex] : ( ! [V127t:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@(ap@c_2EintegerRing_2Eint__r__interp__m@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V124vm))@(inj__ty_2Einteger_2Eint @ V125c))@(ap@(ap@(c_2Elist_2ECONS@ty_2Equote_2Eindex)@(inj__ty_2Equote_2Eindex @ V126x))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V127t)))) = (surj__ty_2Einteger_2Eint @ (ap@(ap@c_2Einteger_2Eint__mul@(inj__ty_2Einteger_2Eint @ V125c))@(ap@(ap@(ap@c_2EintegerRing_2Eint__r__ivl__aux@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V124vm))@(inj__ty_2Equote_2Eindex @ V126x))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V127t)))))))))) & ((( ! [V128vm:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : ( ! [V129a:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@(ap@c_2EintegerRing_2Eint__r__ics__aux@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V128vm))@(inj__ty_2Einteger_2Eint @ V129a))@(c_2Ecanonical_2ENil__monom@ty_2Einteger_2Eint))) = V129a))) & (( ! [V130vm:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : ( ! [V131a:tp__ty_2Einteger_2Eint] : ( ! [V132l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V133t:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@(ap@c_2EintegerRing_2Eint__r__ics__aux@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V130vm))@(inj__ty_2Einteger_2Eint @ V131a))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V132l))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V133t)))) = (surj__ty_2Einteger_2Eint @ (ap@(ap@c_2Einteger_2Eint__add@(inj__ty_2Einteger_2Eint @ V131a))@(ap@(ap@(ap@c_2EintegerRing_2Eint__r__ics__aux@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V130vm))@(ap@(ap@c_2EintegerRing_2Eint__r__interp__vl@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V130vm))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V132l)))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V133t))))))))) & ( ! [V134vm:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : ( ! [V135a:tp__ty_2Einteger_2Eint] : ( ! [V136c:tp__ty_2Einteger_2Eint] : ( ! [V137l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V138t:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@(ap@c_2EintegerRing_2Eint__r__ics__aux@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V134vm))@(inj__ty_2Einteger_2Eint @ V135a))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V136c))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V137l))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V138t)))) = (surj__ty_2Einteger_2Eint @ (ap@(ap@c_2Einteger_2Eint__add@(inj__ty_2Einteger_2Eint @ V135a))@(ap@(ap@(ap@c_2EintegerRing_2Eint__r__ics__aux@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V134vm))@(ap@(ap@(ap@c_2EintegerRing_2Eint__r__interp__m@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V134vm))@(inj__ty_2Einteger_2Eint @ V136c))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V137l)))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V138t)))))))))))) & ((( ! [V139vm:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__interp__cs@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V139vm))@(c_2Ecanonical_2ENil__monom@ty_2Einteger_2Eint))) = fo__c_2Einteger_2Eint__0)) & (( ! [V140vm:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : ( ! [V141l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V142t:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__interp__cs@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V140vm))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V141l))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V142t)))) = (surj__ty_2Einteger_2Eint @ (ap@(ap@(ap@c_2EintegerRing_2Eint__r__ics__aux@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V140vm))@(ap@(ap@c_2EintegerRing_2Eint__r__interp__vl@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V140vm))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V141l)))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V142t))))))) & ( ! [V143vm:tp__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint] : ( ! [V144c:tp__ty_2Einteger_2Eint] : ( ! [V145l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V146t:tp__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__interp__cs@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V143vm))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V144c))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V145l))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V146t)))) = (surj__ty_2Einteger_2Eint @ (ap@(ap@(ap@c_2EintegerRing_2Eint__r__ics__aux@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V143vm))@(ap@(ap@(ap@c_2EintegerRing_2Eint__r__interp__m@(inj__c_ty_2Equote_2Evarmap_ty_2Einteger_2Eint @ V143vm))@(inj__ty_2Einteger_2Eint @ V144c))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V145l)))@(inj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ V146t)))))))))) & ((( ! [V147i:tp__ty_2Equote_2Eindex] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@c_2EintegerRing_2Eint__polynom__normalize@(ap@(c_2EringNorm_2EPvar@ty_2Einteger_2Eint)@(inj__ty_2Equote_2Eindex @ V147i)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(c_2Ecanonical_2ECons__varlist@ty_2Einteger_2Eint)@(ap@(ap@(c_2Elist_2ECONS@ty_2Equote_2Eindex)@(inj__ty_2Equote_2Eindex @ V147i))@(c_2Elist_2ENIL@ty_2Equote_2Eindex)))@(c_2Ecanonical_2ENil__monom@ty_2Einteger_2Eint))))) & (( ! [V148c:tp__ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@c_2EintegerRing_2Eint__polynom__normalize@(ap@(c_2EringNorm_2EPconst@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V148c)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V148c))@(c_2Elist_2ENIL@ty_2Equote_2Eindex))@(c_2Ecanonical_2ENil__monom@ty_2Einteger_2Eint))))) & (( ! [V149pl:tp__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint] : ( ! [V150pr:tp__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@c_2EintegerRing_2Eint__polynom__normalize@(ap@(ap@(c_2EringNorm_2EPplus@ty_2Einteger_2Eint)@(inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ V149pl))@(inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ V150pr)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__merge@(ap@c_2EintegerRing_2Eint__polynom__normalize@(inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ V149pl)))@(ap@c_2EintegerRing_2Eint__polynom__normalize@(inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ V150pr))))))) & (( ! [V151pl:tp__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint] : ( ! [V152pr:tp__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@c_2EintegerRing_2Eint__polynom__normalize@(ap@(ap@(c_2EringNorm_2EPmult@ty_2Einteger_2Eint)@(inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ V151pl))@(inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ V152pr)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__prod@(ap@c_2EintegerRing_2Eint__polynom__normalize@(inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ V151pl)))@(ap@c_2EintegerRing_2Eint__polynom__normalize@(inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ V152pr))))))) & ( ! [V153p:tp__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@c_2EintegerRing_2Eint__polynom__normalize@(ap@(c_2EringNorm_2EPopp@ty_2Einteger_2Eint)@(inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ V153p)))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@(ap@(ap@c_2EintegerRing_2Eint__r__canonical__sum__scalar3@(ap@c_2Einteger_2Eint__neg@(inj__ty_2Einteger_2Eint @ fo__c_2Einteger_2Eint__1)))@(c_2Elist_2ENIL@ty_2Equote_2Eindex))@(ap@c_2EintegerRing_2Eint__polynom__normalize@(inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ V153p)))))))))) & ( ! [V154x:tp__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint] : ((surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@c_2EintegerRing_2Eint__polynom__simplify@(inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ V154x))) = (surj__c_ty_2Ecanonical_2Ecanonical__sum_ty_2Einteger_2Eint @ (ap@c_2EintegerRing_2Eint__r__canonical__sum__simplify@(ap@c_2EintegerRing_2Eint__polynom__normalize@(inj__c_ty_2EringNorm_2Epolynom_ty_2Einteger_2Eint @ V154x))))))))))))))))))))))))).
