include('Axioms/fmapal^2.ax').
thf(tp_ty_2EringNorm_2Epolynom,type,( ty_2EringNorm_2Epolynom: del >del )).
thf(tp_c_2EringNorm_2EPconst,type,(c_2EringNorm_2EPconst:(del>$i))).
thf(mem_c_2EringNorm_2EPconst,axiom,( ! [A_27a:del] : (mem@(c_2EringNorm_2EPconst@A_27a)@(arr@A_27a@(ty_2EringNorm_2Epolynom@A_27a))))).
thf(tp_c_2EringNorm_2EPmult,type,(c_2EringNorm_2EPmult:(del>$i))).
thf(mem_c_2EringNorm_2EPmult,axiom,( ! [A_27a:del] : (mem@(c_2EringNorm_2EPmult@A_27a)@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(ty_2EringNorm_2Epolynom@A_27a)))))).
thf(tp_c_2EringNorm_2EPopp,type,(c_2EringNorm_2EPopp:(del>$i))).
thf(mem_c_2EringNorm_2EPopp,axiom,( ! [A_27a:del] : (mem@(c_2EringNorm_2EPopp@A_27a)@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(ty_2EringNorm_2Epolynom@A_27a))))).
thf(tp_c_2EringNorm_2EPplus,type,(c_2EringNorm_2EPplus:(del>$i))).
thf(mem_c_2EringNorm_2EPplus,axiom,( ! [A_27a:del] : (mem@(c_2EringNorm_2EPplus@A_27a)@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(ty_2EringNorm_2Epolynom@A_27a)))))).
thf(tp_c_2EringNorm_2EPvar,type,(c_2EringNorm_2EPvar:(del>$i))).
thf(mem_c_2EringNorm_2EPvar,axiom,( ! [A_27a:del] : (mem@(c_2EringNorm_2EPvar@A_27a)@(arr@ty_2Equote_2Eindex@(ty_2EringNorm_2Epolynom@A_27a))))).
thf(tp_c_2EringNorm_2Einterp__p,type,(c_2EringNorm_2Einterp__p:(del>$i))).
thf(mem_c_2EringNorm_2Einterp__p,axiom,( ! [A_27a:del] : (mem@(c_2EringNorm_2Einterp__p@A_27a)@(arr@(ty_2Ering_2Ering@A_27a)@(arr@(ty_2Equote_2Evarmap@A_27a)@(arr@(ty_2EringNorm_2Epolynom@A_27a)@A_27a)))))).
thf(tp_c_2EringNorm_2Epolynom__CASE,type,(c_2EringNorm_2Epolynom__CASE:(del>(del>$i)))).
thf(mem_c_2EringNorm_2Epolynom__CASE,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2EringNorm_2Epolynom__CASE@A_27a@A_27b)@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(arr@(arr@ty_2Equote_2Eindex@A_27b)@(arr@(arr@A_27a@A_27b)@(arr@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(arr@(ty_2EringNorm_2Epolynom@A_27a)@A_27b))@(arr@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(arr@(ty_2EringNorm_2Epolynom@A_27a)@A_27b))@(arr@(arr@(ty_2EringNorm_2Epolynom@A_27a)@A_27b)@A_27b)))))))))).
thf(tp_c_2EringNorm_2Epolynom__normalize,type,(c_2EringNorm_2Epolynom__normalize:(del>$i))).
thf(mem_c_2EringNorm_2Epolynom__normalize,axiom,( ! [A_27a:del] : (mem@(c_2EringNorm_2Epolynom__normalize@A_27a)@(arr@(ty_2Ering_2Ering@A_27a)@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(ty_2Ecanonical_2Ecanonical__sum@A_27a)))))).
thf(tp_c_2EringNorm_2Epolynom__simplify,type,(c_2EringNorm_2Epolynom__simplify:(del>$i))).
thf(mem_c_2EringNorm_2Epolynom__simplify,axiom,( ! [A_27a:del] : (mem@(c_2EringNorm_2Epolynom__simplify@A_27a)@(arr@(ty_2Ering_2Ering@A_27a)@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(ty_2Ecanonical_2Ecanonical__sum@A_27a)))))).
thf(tp_c_2EringNorm_2Epolynom__size,type,(c_2EringNorm_2Epolynom__size:(del>$i))).
thf(mem_c_2EringNorm_2Epolynom__size,axiom,( ! [A_27a:del] : (mem@(c_2EringNorm_2Epolynom__size@A_27a)@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@(ty_2EringNorm_2Epolynom@A_27a)@ty_2Enum_2Enum))))).
thf(tp_c_2EringNorm_2Er__canonical__sum__merge,type,(c_2EringNorm_2Er__canonical__sum__merge:(del>$i))).
thf(mem_c_2EringNorm_2Er__canonical__sum__merge,axiom,( ! [A_27a:del] : (mem@(c_2EringNorm_2Er__canonical__sum__merge@A_27a)@(arr@(ty_2Ering_2Ering@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_2EringNorm_2Er__canonical__sum__prod,type,(c_2EringNorm_2Er__canonical__sum__prod:(del>$i))).
thf(mem_c_2EringNorm_2Er__canonical__sum__prod,axiom,( ! [A_27a:del] : (mem@(c_2EringNorm_2Er__canonical__sum__prod@A_27a)@(arr@(ty_2Ering_2Ering@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_2EringNorm_2Er__canonical__sum__scalar,type,(c_2EringNorm_2Er__canonical__sum__scalar:(del>$i))).
thf(mem_c_2EringNorm_2Er__canonical__sum__scalar,axiom,( ! [A_27a:del] : (mem@(c_2EringNorm_2Er__canonical__sum__scalar@A_27a)@(arr@(ty_2Ering_2Ering@A_27a)@(arr@A_27a@(arr@(ty_2Ecanonical_2Ecanonical__sum@A_27a)@(ty_2Ecanonical_2Ecanonical__sum@A_27a))))))).
thf(tp_c_2EringNorm_2Er__canonical__sum__scalar2,type,(c_2EringNorm_2Er__canonical__sum__scalar2:(del>$i))).
thf(mem_c_2EringNorm_2Er__canonical__sum__scalar2,axiom,( ! [A_27a:del] : (mem@(c_2EringNorm_2Er__canonical__sum__scalar2@A_27a)@(arr@(ty_2Ering_2Ering@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_2EringNorm_2Er__canonical__sum__scalar3,type,(c_2EringNorm_2Er__canonical__sum__scalar3:(del>$i))).
thf(mem_c_2EringNorm_2Er__canonical__sum__scalar3,axiom,( ! [A_27a:del] : (mem@(c_2EringNorm_2Er__canonical__sum__scalar3@A_27a)@(arr@(ty_2Ering_2Ering@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_2EringNorm_2Er__canonical__sum__simplify,type,(c_2EringNorm_2Er__canonical__sum__simplify:(del>$i))).
thf(mem_c_2EringNorm_2Er__canonical__sum__simplify,axiom,( ! [A_27a:del] : (mem@(c_2EringNorm_2Er__canonical__sum__simplify@A_27a)@(arr@(ty_2Ering_2Ering@A_27a)@(arr@(ty_2Ecanonical_2Ecanonical__sum@A_27a)@(ty_2Ecanonical_2Ecanonical__sum@A_27a)))))).
thf(tp_c_2EringNorm_2Er__ics__aux,type,(c_2EringNorm_2Er__ics__aux:(del>$i))).
thf(mem_c_2EringNorm_2Er__ics__aux,axiom,( ! [A_27a:del] : (mem@(c_2EringNorm_2Er__ics__aux@A_27a)@(arr@(ty_2Ering_2Ering@A_27a)@(arr@(ty_2Equote_2Evarmap@A_27a)@(arr@A_27a@(arr@(ty_2Ecanonical_2Ecanonical__sum@A_27a)@A_27a))))))).
thf(tp_c_2EringNorm_2Er__interp__cs,type,(c_2EringNorm_2Er__interp__cs:(del>$i))).
thf(mem_c_2EringNorm_2Er__interp__cs,axiom,( ! [A_27a:del] : (mem@(c_2EringNorm_2Er__interp__cs@A_27a)@(arr@(ty_2Ering_2Ering@A_27a)@(arr@(ty_2Equote_2Evarmap@A_27a)@(arr@(ty_2Ecanonical_2Ecanonical__sum@A_27a)@A_27a)))))).
thf(tp_c_2EringNorm_2Er__interp__m,type,(c_2EringNorm_2Er__interp__m:(del>$i))).
thf(mem_c_2EringNorm_2Er__interp__m,axiom,( ! [A_27a:del] : (mem@(c_2EringNorm_2Er__interp__m@A_27a)@(arr@(ty_2Ering_2Ering@A_27a)@(arr@(ty_2Equote_2Evarmap@A_27a)@(arr@A_27a@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@A_27a))))))).
thf(tp_c_2EringNorm_2Er__interp__sp,type,(c_2EringNorm_2Er__interp__sp:(del>$i))).
thf(mem_c_2EringNorm_2Er__interp__sp,axiom,( ! [A_27a:del] : (mem@(c_2EringNorm_2Er__interp__sp@A_27a)@(arr@(ty_2Ering_2Ering@A_27a)@(arr@(ty_2Equote_2Evarmap@A_27a)@(arr@(ty_2Ecanonical_2Espolynom@A_27a)@A_27a)))))).
thf(tp_c_2EringNorm_2Er__interp__vl,type,(c_2EringNorm_2Er__interp__vl:(del>$i))).
thf(mem_c_2EringNorm_2Er__interp__vl,axiom,( ! [A_27a:del] : (mem@(c_2EringNorm_2Er__interp__vl@A_27a)@(arr@(ty_2Ering_2Ering@A_27a)@(arr@(ty_2Equote_2Evarmap@A_27a)@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@A_27a)))))).
thf(tp_c_2EringNorm_2Er__ivl__aux,type,(c_2EringNorm_2Er__ivl__aux:(del>$i))).
thf(mem_c_2EringNorm_2Er__ivl__aux,axiom,( ! [A_27a:del] : (mem@(c_2EringNorm_2Er__ivl__aux@A_27a)@(arr@(ty_2Ering_2Ering@A_27a)@(arr@(ty_2Equote_2Evarmap@A_27a)@(arr@ty_2Equote_2Eindex@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@A_27a))))))).
thf(tp_c_2EringNorm_2Er__monom__insert,type,(c_2EringNorm_2Er__monom__insert:(del>$i))).
thf(mem_c_2EringNorm_2Er__monom__insert,axiom,( ! [A_27a:del] : (mem@(c_2EringNorm_2Er__monom__insert@A_27a)@(arr@(ty_2Ering_2Ering@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_2EringNorm_2Er__spolynom__normalize,type,(c_2EringNorm_2Er__spolynom__normalize:(del>$i))).
thf(mem_c_2EringNorm_2Er__spolynom__normalize,axiom,( ! [A_27a:del] : (mem@(c_2EringNorm_2Er__spolynom__normalize@A_27a)@(arr@(ty_2Ering_2Ering@A_27a)@(arr@(ty_2Ecanonical_2Espolynom@A_27a)@(ty_2Ecanonical_2Ecanonical__sum@A_27a)))))).
thf(tp_c_2EringNorm_2Er__spolynom__simplify,type,(c_2EringNorm_2Er__spolynom__simplify:(del>$i))).
thf(mem_c_2EringNorm_2Er__spolynom__simplify,axiom,( ! [A_27a:del] : (mem@(c_2EringNorm_2Er__spolynom__simplify@A_27a)@(arr@(ty_2Ering_2Ering@A_27a)@(arr@(ty_2Ecanonical_2Espolynom@A_27a)@(ty_2Ecanonical_2Ecanonical__sum@A_27a)))))).
thf(tp_c_2EringNorm_2Er__varlist__insert,type,(c_2EringNorm_2Er__varlist__insert:(del>$i))).
thf(mem_c_2EringNorm_2Er__varlist__insert,axiom,( ! [A_27a:del] : (mem@(c_2EringNorm_2Er__varlist__insert@A_27a)@(arr@(ty_2Ering_2Ering@A_27a)@(arr@(ty_2Elist_2Elist@ty_2Equote_2Eindex)@(arr@(ty_2Ecanonical_2Ecanonical__sum@A_27a)@(ty_2Ecanonical_2Ecanonical__sum@A_27a))))))).
thf(ax_thm_2EringNorm_2Er__interp__sp__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((ap@(c_2EringNorm_2Er__interp__sp@A_27a)@V0r) = (ap@(c_2Ecanonical_2Einterp__sp@A_27a)@(ap@(c_2Ering_2Esemi__ring__of@A_27a)@V0r))))))).
thf(ax_thm_2EringNorm_2Er__spolynom__simplify__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((ap@(c_2EringNorm_2Er__spolynom__simplify@A_27a)@V0r) = (ap@(c_2Ecanonical_2Espolynom__simplify@A_27a)@(ap@(c_2Ering_2Esemi__ring__of@A_27a)@V0r))))))).
thf(ax_thm_2EringNorm_2Er__spolynom__normalize__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((ap@(c_2EringNorm_2Er__spolynom__normalize@A_27a)@V0r) = (ap@(c_2Ecanonical_2Espolynom__normalize@A_27a)@(ap@(c_2Ering_2Esemi__ring__of@A_27a)@V0r))))))).
thf(ax_thm_2EringNorm_2Er__interp__cs__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((ap@(c_2EringNorm_2Er__interp__cs@A_27a)@V0r) = (ap@(c_2Ecanonical_2Einterp__cs@A_27a)@(ap@(c_2Ering_2Esemi__ring__of@A_27a)@V0r))))))).
thf(ax_thm_2EringNorm_2Er__ics__aux__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((ap@(c_2EringNorm_2Er__ics__aux@A_27a)@V0r) = (ap@(c_2Ecanonical_2Eics__aux@A_27a)@(ap@(c_2Ering_2Esemi__ring__of@A_27a)@V0r))))))).
thf(ax_thm_2EringNorm_2Er__interp__m__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((ap@(c_2EringNorm_2Er__interp__m@A_27a)@V0r) = (ap@(c_2Ecanonical_2Einterp__m@A_27a)@(ap@(c_2Ering_2Esemi__ring__of@A_27a)@V0r))))))).
thf(ax_thm_2EringNorm_2Er__interp__vl__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((ap@(c_2EringNorm_2Er__interp__vl@A_27a)@V0r) = (ap@(c_2Ecanonical_2Einterp__vl@A_27a)@(ap@(c_2Ering_2Esemi__ring__of@A_27a)@V0r))))))).
thf(ax_thm_2EringNorm_2Er__ivl__aux__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((ap@(c_2EringNorm_2Er__ivl__aux@A_27a)@V0r) = (ap@(c_2Ecanonical_2Eivl__aux@A_27a)@(ap@(c_2Ering_2Esemi__ring__of@A_27a)@V0r))))))).
thf(ax_thm_2EringNorm_2Er__canonical__sum__simplify__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((ap@(c_2EringNorm_2Er__canonical__sum__simplify@A_27a)@V0r) = (ap@(c_2Ecanonical_2Ecanonical__sum__simplify@A_27a)@(ap@(c_2Ering_2Esemi__ring__of@A_27a)@V0r))))))).
thf(ax_thm_2EringNorm_2Er__canonical__sum__prod__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((ap@(c_2EringNorm_2Er__canonical__sum__prod@A_27a)@V0r) = (ap@(c_2Ecanonical_2Ecanonical__sum__prod@A_27a)@(ap@(c_2Ering_2Esemi__ring__of@A_27a)@V0r))))))).
thf(ax_thm_2EringNorm_2Er__canonical__sum__scalar3__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((ap@(c_2EringNorm_2Er__canonical__sum__scalar3@A_27a)@V0r) = (ap@(c_2Ecanonical_2Ecanonical__sum__scalar3@A_27a)@(ap@(c_2Ering_2Esemi__ring__of@A_27a)@V0r))))))).
thf(ax_thm_2EringNorm_2Er__canonical__sum__scalar2__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((ap@(c_2EringNorm_2Er__canonical__sum__scalar2@A_27a)@V0r) = (ap@(c_2Ecanonical_2Ecanonical__sum__scalar2@A_27a)@(ap@(c_2Ering_2Esemi__ring__of@A_27a)@V0r))))))).
thf(ax_thm_2EringNorm_2Er__canonical__sum__scalar__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((ap@(c_2EringNorm_2Er__canonical__sum__scalar@A_27a)@V0r) = (ap@(c_2Ecanonical_2Ecanonical__sum__scalar@A_27a)@(ap@(c_2Ering_2Esemi__ring__of@A_27a)@V0r))))))).
thf(ax_thm_2EringNorm_2Er__varlist__insert__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((ap@(c_2EringNorm_2Er__varlist__insert@A_27a)@V0r) = (ap@(c_2Ecanonical_2Evarlist__insert@A_27a)@(ap@(c_2Ering_2Esemi__ring__of@A_27a)@V0r))))))).
thf(ax_thm_2EringNorm_2Er__monom__insert__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((ap@(c_2EringNorm_2Er__monom__insert@A_27a)@V0r) = (ap@(c_2Ecanonical_2Emonom__insert@A_27a)@(ap@(c_2Ering_2Esemi__ring__of@A_27a)@V0r))))))).
thf(ax_thm_2EringNorm_2Er__canonical__sum__merge__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((ap@(c_2EringNorm_2Er__canonical__sum__merge@A_27a)@V0r) = (ap@(c_2Ecanonical_2Ecanonical__sum__merge@A_27a)@(ap@(c_2Ering_2Esemi__ring__of@A_27a)@V0r))))))).
thf(conj_thm_2EringNorm_2Einterp__sp__def,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => (( ! [V1vm:$i] : ((mem@V1vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V2c:$i] : ((mem@V2c@A_27a) => ((ap@(ap@(ap@(c_2EringNorm_2Er__interp__sp@A_27a)@V0r)@V1vm)@(ap@(c_2Ecanonical_2ESPconst@A_27a)@V2c)) = V2c))))) & (( ! [V3vm:$i] : ((mem@V3vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V4i:tp__ty_2Equote_2Eindex] : ((ap@(ap@(ap@(c_2EringNorm_2Er__interp__sp@A_27a)@V0r)@V3vm)@(ap@(c_2Ecanonical_2ESPvar@A_27a)@(inj__ty_2Equote_2Eindex @ V4i))) = (ap@(ap@(c_2Equote_2Evarmap__find@A_27a)@(inj__ty_2Equote_2Eindex @ V4i))@V3vm))))) & (( ! [V5vm:$i] : ((mem@V5vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V6p1:$i] : ((mem@V6p1@(ty_2Ecanonical_2Espolynom@A_27a)) => ( ! [V7p2:$i] : ((mem@V7p2@(ty_2Ecanonical_2Espolynom@A_27a)) => ((ap@(ap@(ap@(c_2EringNorm_2Er__interp__sp@A_27a)@V0r)@V5vm)@(ap@(ap@(c_2Ecanonical_2ESPplus@A_27a)@V6p1)@V7p2)) = (ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@(ap@(ap@(ap@(c_2EringNorm_2Er__interp__sp@A_27a)@V0r)@V5vm)@V6p1))@(ap@(ap@(ap@(c_2EringNorm_2Er__interp__sp@A_27a)@V0r)@V5vm)@V7p2))))))))) & ( ! [V8vm:$i] : ((mem@V8vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V9p1:$i] : ((mem@V9p1@(ty_2Ecanonical_2Espolynom@A_27a)) => ( ! [V10p2:$i] : ((mem@V10p2@(ty_2Ecanonical_2Espolynom@A_27a)) => ((ap@(ap@(ap@(c_2EringNorm_2Er__interp__sp@A_27a)@V0r)@V8vm)@(ap@(ap@(c_2Ecanonical_2ESPmult@A_27a)@V9p1)@V10p2)) = (ap@(ap@(ap@(c_2Ering_2Ering__RM@A_27a)@V0r)@(ap@(ap@(ap@(c_2EringNorm_2Er__interp__sp@A_27a)@V0r)@V8vm)@V9p1))@(ap@(ap@(ap@(c_2EringNorm_2Er__interp__sp@A_27a)@V0r)@V8vm)@V10p2)))))))))))))))).
thf(conj_thm_2EringNorm_2Ecanonical__sum__merge__def,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => (( ! [V1t2:$i] : ((mem@V1t2@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V2t1:$i] : ((mem@V2t1@(ty_2Ecanonical_2Ecanonical__sum@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_2EringNorm_2Er__canonical__sum__merge@A_27a)@V0r)@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V6c1)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V4l1))@V2t1))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V5c2)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l2))@V1t2)) = (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_2EringNorm_2Er__canonical__sum__merge@A_27a)@V0r)@V2t1)@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V5c2)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l2))@V1t2))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@(ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@V6c1)@V5c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V4l1))@(ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__merge@A_27a)@V0r)@V2t1)@V1t2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V5c2)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l2))@(ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__merge@A_27a)@V0r)@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V6c1)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V4l1))@V2t1))@V1t2)))))))))))))) & (( ! [V7t2:$i] : ((mem@V7t2@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V8t1:$i] : ((mem@V8t1@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V9l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V10l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V11c1:$i] : ((mem@V11c1@A_27a) => ((ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__merge@A_27a)@V0r)@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V11c1)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V10l1))@V8t1))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V9l2))@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 @ V10l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V9l2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V11c1)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V10l1))@(ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__merge@A_27a)@V0r)@V8t1)@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V9l2))@V7t2))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@(ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@V11c1)@(ap@(c_2Ering_2Ering__R1@A_27a)@V0r)))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V10l1))@(ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__merge@A_27a)@V0r)@V8t1)@V7t2)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V9l2))@(ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__merge@A_27a)@V0r)@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V11c1)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V10l1))@V8t1))@V7t2)))))))))))) & (( ! [V12t2:$i] : ((mem@V12t2@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V13t1:$i] : ((mem@V13t1@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V14l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V15l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V16c2:$i] : ((mem@V16c2@A_27a) => ((ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__merge@A_27a)@V0r)@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V15l1))@V13t1))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V16c2)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V14l2))@V12t2)) = (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 @ V15l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V14l2)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V15l1))@(ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__merge@A_27a)@V0r)@V13t1)@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V16c2)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V14l2))@V12t2))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@(ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@(ap@(c_2Ering_2Ering__R1@A_27a)@V0r))@V16c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V15l1))@(ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__merge@A_27a)@V0r)@V13t1)@V12t2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V16c2)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V14l2))@(ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__merge@A_27a)@V0r)@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V15l1))@V13t1))@V12t2)))))))))))) & (( ! [V17t2:$i] : ((mem@V17t2@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V18t1:$i] : ((mem@V18t1@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V19l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V20l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__merge@A_27a)@V0r)@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V20l1))@V18t1))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V19l2))@V17t2)) = (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 @ V20l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V19l2)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V20l1))@(ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__merge@A_27a)@V0r)@V18t1)@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V19l2))@V17t2))))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@(ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@(ap@(c_2Ering_2Ering__R1@A_27a)@V0r))@(ap@(c_2Ering_2Ering__R1@A_27a)@V0r)))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V20l1))@(ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__merge@A_27a)@V0r)@V18t1)@V17t2)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V19l2))@(ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__merge@A_27a)@V0r)@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V20l1))@V18t1))@V17t2)))))))))) & (( ! [V21s1:$i] : ((mem@V21s1@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ((ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__merge@A_27a)@V0r)@V21s1)@(c_2Ecanonical_2ENil__monom@A_27a)) = V21s1))) & (( ! [V22v6:$i] : ((mem@V22v6@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V23v5:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V24v4:$i] : ((mem@V24v4@A_27a) => ((ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__merge@A_27a)@V0r)@(c_2Ecanonical_2ENil__monom@A_27a))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V24v4)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V23v5))@V22v6)) = (ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V24v4)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V23v5))@V22v6))))))) & ( ! [V25v8:$i] : ((mem@V25v8@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V26v7:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__merge@A_27a)@V0r)@(c_2Ecanonical_2ENil__monom@A_27a))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V26v7))@V25v8)) = (ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V26v7))@V25v8))))))))))))))).
thf(conj_thm_2EringNorm_2Emonom__insert__def,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => (( ! [V1t2:$i] : ((mem@V1t2@(ty_2Ecanonical_2Ecanonical__sum@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_2EringNorm_2Er__monom__insert@A_27a)@V0r)@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))@V1t2)) = (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))@V1t2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@(ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@V5c1)@V4c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l1))@V1t2))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V4c2)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V2l2))@(ap@(ap@(ap@(ap@(c_2EringNorm_2Er__monom__insert@A_27a)@V0r)@V5c1)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l1))@V1t2)))))))))))) & (( ! [V6t2:$i] : ((mem@V6t2@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V7l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V8l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V9c1:$i] : ((mem@V9c1@A_27a) => ((ap@(ap@(ap@(ap@(c_2EringNorm_2Er__monom__insert@A_27a)@V0r)@V9c1)@(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))@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 @ V8l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V7l2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V9c1)@(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))@V6t2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@(ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@V9c1)@(ap@(c_2Ering_2Ering__R1@A_27a)@V0r)))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V8l1))@V6t2))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V7l2))@(ap@(ap@(ap@(ap@(c_2EringNorm_2Er__monom__insert@A_27a)@V0r)@V9c1)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V8l1))@V6t2)))))))))) & ( ! [V10l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V11c1:$i] : ((mem@V11c1@A_27a) => ((ap@(ap@(ap@(ap@(c_2EringNorm_2Er__monom__insert@A_27a)@V0r)@V11c1)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V10l1))@(c_2Ecanonical_2ENil__monom@A_27a)) = (ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V11c1)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V10l1))@(c_2Ecanonical_2ENil__monom@A_27a)))))))))))).
thf(conj_thm_2EringNorm_2Evarlist__insert__def,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => (( ! [V1t2:$i] : ((mem@V1t2@(ty_2Ecanonical_2Ecanonical__sum@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_2EringNorm_2Er__varlist__insert@A_27a)@V0r)@(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))@V1t2)) = (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))@V1t2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@(ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@(ap@(c_2Ering_2Ering__R1@A_27a)@V0r))@V4c2))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l1))@V1t2))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V4c2)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V2l2))@(ap@(ap@(ap@(c_2EringNorm_2Er__varlist__insert@A_27a)@V0r)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l1))@V1t2)))))))))) & (( ! [V5t2:$i] : ((mem@V5t2@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V6l2:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V7l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((ap@(ap@(ap@(c_2EringNorm_2Er__varlist__insert@A_27a)@V0r)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V7l1))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V6l2))@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 @ V7l1))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V6l2)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V7l1))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V6l2))@V5t2)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@(ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@(ap@(c_2Ering_2Ering__R1@A_27a)@V0r))@(ap@(c_2Ering_2Ering__R1@A_27a)@V0r)))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V7l1))@V5t2))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V6l2))@(ap@(ap@(ap@(c_2EringNorm_2Er__varlist__insert@A_27a)@V0r)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V7l1))@V5t2)))))))) & ( ! [V8l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((ap@(ap@(ap@(c_2EringNorm_2Er__varlist__insert@A_27a)@V0r)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V8l1))@(c_2Ecanonical_2ENil__monom@A_27a)) = (ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V8l1))@(c_2Ecanonical_2ENil__monom@A_27a)))))))))).
thf(conj_thm_2EringNorm_2Ecanonical__sum__scalar__def,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@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_2EringNorm_2Er__canonical__sum__scalar@A_27a)@V0r)@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_2Ering_2Ering__RM@A_27a)@V0r)@V1c0)@V2c))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l))@(ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__scalar@A_27a)@V0r)@V1c0)@V4t)))))))))) & (( ! [V5c0:$i] : ((mem@V5c0@A_27a) => ( ! [V6l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V7t:$i] : ((mem@V7t@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ((ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__scalar@A_27a)@V0r)@V5c0)@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V6l))@V7t)) = (ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V5c0)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V6l))@(ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__scalar@A_27a)@V0r)@V5c0)@V7t)))))))) & ( ! [V8c0:$i] : ((mem@V8c0@A_27a) => ((ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__scalar@A_27a)@V0r)@V8c0)@(c_2Ecanonical_2ENil__monom@A_27a)) = (c_2Ecanonical_2ENil__monom@A_27a)))))))))).
thf(conj_thm_2EringNorm_2Ecanonical__sum__scalar2__def,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@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_2EringNorm_2Er__canonical__sum__scalar2@A_27a)@V0r)@(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_2EringNorm_2Er__monom__insert@A_27a)@V0r)@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_2EringNorm_2Er__canonical__sum__scalar2@A_27a)@V0r)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V1l0))@V4t))))))))) & (( ! [V5l0:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V6l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V7t:$i] : ((mem@V7t@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ((ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__scalar2@A_27a)@V0r)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V5l0))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V6l))@V7t)) = (ap@(ap@(ap@(c_2EringNorm_2Er__varlist__insert@A_27a)@V0r)@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__merge@ty_2Equote_2Eindex)@c_2Equote_2Eindex__lt)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V5l0))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V6l)))@(ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__scalar2@A_27a)@V0r)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V5l0))@V7t))))))) & ( ! [V8l0:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__scalar2@A_27a)@V0r)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V8l0))@(c_2Ecanonical_2ENil__monom@A_27a)) = (c_2Ecanonical_2ENil__monom@A_27a))))))))).
thf(conj_thm_2EringNorm_2Ecanonical__sum__scalar3__def,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@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_2EringNorm_2Er__canonical__sum__scalar3@A_27a)@V0r)@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_2EringNorm_2Er__monom__insert@A_27a)@V0r)@(ap@(ap@(ap@(c_2Ering_2Ering__RM@A_27a)@V0r)@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_2EringNorm_2Er__canonical__sum__scalar3@A_27a)@V0r)@V1c0)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V2l0))@V5t))))))))))) & (( ! [V6c0:$i] : ((mem@V6c0@A_27a) => ( ! [V7l0:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V8l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V9t:$i] : ((mem@V9t@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ((ap@(ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__scalar3@A_27a)@V0r)@V6c0)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V7l0))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V8l))@V9t)) = (ap@(ap@(ap@(ap@(c_2EringNorm_2Er__monom__insert@A_27a)@V0r)@V6c0)@(ap@(ap@(ap@(c_2EternaryComparisons_2Elist__merge@ty_2Equote_2Eindex)@c_2Equote_2Eindex__lt)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V7l0))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V8l)))@(ap@(ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__scalar3@A_27a)@V0r)@V6c0)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V7l0))@V9t))))))))) & ( ! [V10c0:$i] : ((mem@V10c0@A_27a) => ( ! [V11l0:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((ap@(ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__scalar3@A_27a)@V0r)@V10c0)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V11l0))@(c_2Ecanonical_2ENil__monom@A_27a)) = (c_2Ecanonical_2ENil__monom@A_27a))))))))))).
thf(conj_thm_2EringNorm_2Ecanonical__sum__prod__def,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@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_2EringNorm_2Er__canonical__sum__prod@A_27a)@V0r)@(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_2EringNorm_2Er__canonical__sum__merge@A_27a)@V0r)@(ap@(ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__scalar3@A_27a)@V0r)@V1c1)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V2l1))@V4s2))@(ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__prod@A_27a)@V0r)@V3t1)@V4s2)))))))))) & (( ! [V5l1:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V6t1:$i] : ((mem@V6t1@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ( ! [V7s2:$i] : ((mem@V7s2@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ((ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__prod@A_27a)@V0r)@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V5l1))@V6t1))@V7s2) = (ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__merge@A_27a)@V0r)@(ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__scalar2@A_27a)@V0r)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V5l1))@V7s2))@(ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__prod@A_27a)@V0r)@V6t1)@V7s2)))))))) & ( ! [V8s2:$i] : ((mem@V8s2@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ((ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__prod@A_27a)@V0r)@(c_2Ecanonical_2ENil__monom@A_27a))@V8s2) = (c_2Ecanonical_2ENil__monom@A_27a)))))))))).
thf(conj_thm_2EringNorm_2Ecanonical__sum__simplify__def,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@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_2EringNorm_2Er__canonical__sum__simplify@A_27a)@V0r)@(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_2Ering_2Ering__R0@A_27a)@V0r)))@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__simplify@A_27a)@V0r)@V3t))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Ecanonical_2Ecanonical__sum@A_27a))@(ap@(ap@(c_2Emin_2E_3D@A_27a)@V1c)@(ap@(c_2Ering_2Ering__R1@A_27a)@V0r)))@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V2l))@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__simplify@A_27a)@V0r)@V3t)))@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V1c)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V2l))@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__simplify@A_27a)@V0r)@V3t)))))))))) & (( ! [V4l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V5t:$i] : ((mem@V5t@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ((ap@(ap@(c_2EringNorm_2Er__canonical__sum__simplify@A_27a)@V0r)@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V4l))@V5t)) = (ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V4l))@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__simplify@A_27a)@V0r)@V5t)))))) & ((ap@(ap@(c_2EringNorm_2Er__canonical__sum__simplify@A_27a)@V0r)@(c_2Ecanonical_2ENil__monom@A_27a)) = (c_2Ecanonical_2ENil__monom@A_27a)))))))).
thf(conj_thm_2EringNorm_2Eivl__aux__def,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => (( ! [V1vm:$i] : ((mem@V1vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V2x:tp__ty_2Equote_2Eindex] : ((ap@(ap@(ap@(ap@(c_2EringNorm_2Er__ivl__aux@A_27a)@V0r)@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))))) & ( ! [V3vm:$i] : ((mem@V3vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V4x:tp__ty_2Equote_2Eindex] : ( ! [V5x_27:tp__ty_2Equote_2Eindex] : ( ! [V6t_27:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((ap@(ap@(ap@(ap@(c_2EringNorm_2Er__ivl__aux@A_27a)@V0r)@V3vm)@(inj__ty_2Equote_2Eindex @ V4x))@(ap@(ap@(c_2Elist_2ECONS@ty_2Equote_2Eindex)@(inj__ty_2Equote_2Eindex @ V5x_27))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V6t_27))) = (ap@(ap@(ap@(c_2Ering_2Ering__RM@A_27a)@V0r)@(ap@(ap@(c_2Equote_2Evarmap__find@A_27a)@(inj__ty_2Equote_2Eindex @ V4x))@V3vm))@(ap@(ap@(ap@(ap@(c_2EringNorm_2Er__ivl__aux@A_27a)@V0r)@V3vm)@(inj__ty_2Equote_2Eindex @ V5x_27))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V6t_27)))))))))))))).
thf(conj_thm_2EringNorm_2Einterp__vl__def,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => (( ! [V1vm:$i] : ((mem@V1vm@(ty_2Equote_2Evarmap@A_27a)) => ((ap@(ap@(ap@(c_2EringNorm_2Er__interp__vl@A_27a)@V0r)@V1vm)@(c_2Elist_2ENIL@ty_2Equote_2Eindex)) = (ap@(c_2Ering_2Ering__R1@A_27a)@V0r)))) & ( ! [V2vm:$i] : ((mem@V2vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V3x:tp__ty_2Equote_2Eindex] : ( ! [V4t:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((ap@(ap@(ap@(c_2EringNorm_2Er__interp__vl@A_27a)@V0r)@V2vm)@(ap@(ap@(c_2Elist_2ECONS@ty_2Equote_2Eindex)@(inj__ty_2Equote_2Eindex @ V3x))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V4t))) = (ap@(ap@(ap@(ap@(c_2EringNorm_2Er__ivl__aux@A_27a)@V0r)@V2vm)@(inj__ty_2Equote_2Eindex @ V3x))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V4t)))))))))))).
thf(conj_thm_2EringNorm_2Einterp__m__def,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => (( ! [V1vm:$i] : ((mem@V1vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V2c:$i] : ((mem@V2c@A_27a) => ((ap@(ap@(ap@(ap@(c_2EringNorm_2Er__interp__m@A_27a)@V0r)@V1vm)@V2c)@(c_2Elist_2ENIL@ty_2Equote_2Eindex)) = V2c))))) & ( ! [V3vm:$i] : ((mem@V3vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V4c:$i] : ((mem@V4c@A_27a) => ( ! [V5x:tp__ty_2Equote_2Eindex] : ( ! [V6t:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ((ap@(ap@(ap@(ap@(c_2EringNorm_2Er__interp__m@A_27a)@V0r)@V3vm)@V4c)@(ap@(ap@(c_2Elist_2ECONS@ty_2Equote_2Eindex)@(inj__ty_2Equote_2Eindex @ V5x))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V6t))) = (ap@(ap@(ap@(c_2Ering_2Ering__RM@A_27a)@V0r)@V4c)@(ap@(ap@(ap@(ap@(c_2EringNorm_2Er__ivl__aux@A_27a)@V0r)@V3vm)@(inj__ty_2Equote_2Eindex @ V5x))@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V6t))))))))))))))).
thf(conj_thm_2EringNorm_2Eics__aux__def,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => (( ! [V1vm:$i] : ((mem@V1vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V2a:$i] : ((mem@V2a@A_27a) => ((ap@(ap@(ap@(ap@(c_2EringNorm_2Er__ics__aux@A_27a)@V0r)@V1vm)@V2a)@(c_2Ecanonical_2ENil__monom@A_27a)) = V2a))))) & (( ! [V3vm:$i] : ((mem@V3vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V4a:$i] : ((mem@V4a@A_27a) => ( ! [V5l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V6t:$i] : ((mem@V6t@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ((ap@(ap@(ap@(ap@(c_2EringNorm_2Er__ics__aux@A_27a)@V0r)@V3vm)@V4a)@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V5l))@V6t)) = (ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@V4a)@(ap@(ap@(ap@(ap@(c_2EringNorm_2Er__ics__aux@A_27a)@V0r)@V3vm)@(ap@(ap@(ap@(c_2EringNorm_2Er__interp__vl@A_27a)@V0r)@V3vm)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V5l)))@V6t)))))))))) & ( ! [V7vm:$i] : ((mem@V7vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V8a:$i] : ((mem@V8a@A_27a) => ( ! [V9c:$i] : ((mem@V9c@A_27a) => ( ! [V10l:tp__c_ty_2Elist_2Elist_ty_2Equote_2Eindex] : ( ! [V11t:$i] : ((mem@V11t@(ty_2Ecanonical_2Ecanonical__sum@A_27a)) => ((ap@(ap@(ap@(ap@(c_2EringNorm_2Er__ics__aux@A_27a)@V0r)@V7vm)@V8a)@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V9c)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V10l))@V11t)) = (ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@V8a)@(ap@(ap@(ap@(ap@(c_2EringNorm_2Er__ics__aux@A_27a)@V0r)@V7vm)@(ap@(ap@(ap@(ap@(c_2EringNorm_2Er__interp__m@A_27a)@V0r)@V7vm)@V9c)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V10l)))@V11t)))))))))))))))))).
thf(conj_thm_2EringNorm_2Einterp__cs__def,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => (( ! [V1vm:$i] : ((mem@V1vm@(ty_2Equote_2Evarmap@A_27a)) => ((ap@(ap@(ap@(c_2EringNorm_2Er__interp__cs@A_27a)@V0r)@V1vm)@(c_2Ecanonical_2ENil__monom@A_27a)) = (ap@(c_2Ering_2Ering__R0@A_27a)@V0r)))) & (( ! [V2vm:$i] : ((mem@V2vm@(ty_2Equote_2Evarmap@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_2EringNorm_2Er__interp__cs@A_27a)@V0r)@V2vm)@(ap@(ap@(c_2Ecanonical_2ECons__varlist@A_27a)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l))@V4t)) = (ap@(ap@(ap@(ap@(c_2EringNorm_2Er__ics__aux@A_27a)@V0r)@V2vm)@(ap@(ap@(ap@(c_2EringNorm_2Er__interp__vl@A_27a)@V0r)@V2vm)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V3l)))@V4t))))))) & ( ! [V5vm:$i] : ((mem@V5vm@(ty_2Equote_2Evarmap@A_27a)) => ( ! [V6c:$i] : ((mem@V6c@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_2EringNorm_2Er__interp__cs@A_27a)@V0r)@V5vm)@(ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V6c)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V7l))@V8t)) = (ap@(ap@(ap@(ap@(c_2EringNorm_2Er__ics__aux@A_27a)@V0r)@V5vm)@(ap@(ap@(ap@(ap@(c_2EringNorm_2Er__interp__m@A_27a)@V0r)@V5vm)@V6c)@(inj__c_ty_2Elist_2Elist_ty_2Equote_2Eindex @ V7l)))@V8t))))))))))))))).
thf(conj_thm_2EringNorm_2Espolynom__normalize__def,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => (( ! [V1i:tp__ty_2Equote_2Eindex] : ((ap@(ap@(c_2EringNorm_2Er__spolynom__normalize@A_27a)@V0r)@(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)))) & (( ! [V2c:$i] : ((mem@V2c@A_27a) => ((ap@(ap@(c_2EringNorm_2Er__spolynom__normalize@A_27a)@V0r)@(ap@(c_2Ecanonical_2ESPconst@A_27a)@V2c)) = (ap@(ap@(ap@(c_2Ecanonical_2ECons__monom@A_27a)@V2c)@(c_2Elist_2ENIL@ty_2Equote_2Eindex))@(c_2Ecanonical_2ENil__monom@A_27a))))) & (( ! [V3l:$i] : ((mem@V3l@(ty_2Ecanonical_2Espolynom@A_27a)) => ( ! [V4r_27:$i] : ((mem@V4r_27@(ty_2Ecanonical_2Espolynom@A_27a)) => ((ap@(ap@(c_2EringNorm_2Er__spolynom__normalize@A_27a)@V0r)@(ap@(ap@(c_2Ecanonical_2ESPplus@A_27a)@V3l)@V4r_27)) = (ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__merge@A_27a)@V0r)@(ap@(ap@(c_2EringNorm_2Er__spolynom__normalize@A_27a)@V0r)@V3l))@(ap@(ap@(c_2EringNorm_2Er__spolynom__normalize@A_27a)@V0r)@V4r_27))))))) & ( ! [V5l:$i] : ((mem@V5l@(ty_2Ecanonical_2Espolynom@A_27a)) => ( ! [V6r_27:$i] : ((mem@V6r_27@(ty_2Ecanonical_2Espolynom@A_27a)) => ((ap@(ap@(c_2EringNorm_2Er__spolynom__normalize@A_27a)@V0r)@(ap@(ap@(c_2Ecanonical_2ESPmult@A_27a)@V5l)@V6r_27)) = (ap@(ap@(ap@(c_2EringNorm_2Er__canonical__sum__prod@A_27a)@V0r)@(ap@(ap@(c_2EringNorm_2Er__spolynom__normalize@A_27a)@V0r)@V5l))@(ap@(ap@(c_2EringNorm_2Er__spolynom__normalize@A_27a)@V0r)@V6r_27)))))))))))))).
thf(conj_thm_2EringNorm_2Espolynom__simplify__def,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ( ! [V1x:$i] : ((mem@V1x@(ty_2Ecanonical_2Espolynom@A_27a)) => ((ap@(ap@(c_2EringNorm_2Er__spolynom__simplify@A_27a)@V0r)@V1x) = (ap@(ap@(c_2EringNorm_2Er__canonical__sum__simplify@A_27a)@V0r)@(ap@(ap@(c_2EringNorm_2Er__spolynom__normalize@A_27a)@V0r)@V1x))))))))).
thf(ax_thm_2EringNorm_2Epolynom__TY__DEF,axiom,( ! [A_27a:del]: (? [V0rep:$i] : ((mem@V0rep@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a)))) & (p@(ap@(ap@(c_2Ebool_2ETYPE__DEFINITION@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a))@(ty_2EringNorm_2Epolynom@A_27a))@(lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a))@(^ [V1a0_27:$i] : (ap@(c_2Ebool_2E_21@(arr@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a))@bool))@(lam@(arr@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a))@bool)@(^ [V2_27polynom_27:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(c_2Ebool_2E_21@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a)))@(lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a))@(^ [V3a0_27:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(c_2Ebool_2E_3F@ty_2Equote_2Eindex)@(lam@ty_2Equote_2Eindex@(^ [V4a:$i] : (ap@(ap@(c_2Emin_2E_3D@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a)))@V3a0_27)@(ap@(lam@ty_2Equote_2Eindex@(^ [V5a:$i] : (ap@(ap@(ap@(c_2Eind__type_2ECONSTR@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@(ap@(c_2Epair_2E_2C@ty_2Equote_2Eindex@A_27a)@V5a)@(c_2Ebool_2EARB@A_27a)))@(lam@ty_2Enum_2Enum@(^ [V6n:$i] : (c_2Eind__type_2EBOTTOM@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a)))))))@V4a))))))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(c_2Ebool_2E_3F@A_27a)@(lam@A_27a@(^ [V7a:$i] : (ap@(ap@(c_2Emin_2E_3D@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a)))@V3a0_27)@(ap@(lam@A_27a@(^ [V8a:$i] : (ap@(ap@(ap@(c_2Eind__type_2ECONSTR@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(ap@(c_2Epair_2E_2C@ty_2Equote_2Eindex@A_27a)@(c_2Ebool_2EARB@ty_2Equote_2Eindex))@V8a))@(lam@ty_2Enum_2Enum@(^ [V9n:$i] : (c_2Eind__type_2EBOTTOM@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a)))))))@V7a))))))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(c_2Ebool_2E_3F@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a)))@(lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a))@(^ [V10a0:$i] : (ap@(c_2Ebool_2E_3F@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a)))@(lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a))@(^ [V11a1:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a)))@V3a0_27)@(ap@(ap@(lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a))@(^ [V12a0:$i] : (lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a))@(^ [V13a1:$i] : (ap@(ap@(ap@(c_2Eind__type_2ECONSTR@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a))@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))@(ap@(ap@(c_2Epair_2E_2C@ty_2Equote_2Eindex@A_27a)@(c_2Ebool_2EARB@ty_2Equote_2Eindex))@(c_2Ebool_2EARB@A_27a)))@(ap@(ap@(c_2Eind__type_2EFCONS@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a)))@V12a0)@(ap@(ap@(c_2Eind__type_2EFCONS@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a)))@V13a1)@(lam@ty_2Enum_2Enum@(^ [V14n:$i] : (c_2Eind__type_2EBOTTOM@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a)))))))))))@V10a0)@V11a1)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V2_27polynom_27@V10a0))@(ap@V2_27polynom_27@V11a1))))))))))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(c_2Ebool_2E_3F@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a)))@(lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a))@(^ [V15a0:$i] : (ap@(c_2Ebool_2E_3F@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a)))@(lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a))@(^ [V16a1:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a)))@V3a0_27)@(ap@(ap@(lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a))@(^ [V17a0:$i] : (lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a))@(^ [V18a1:$i] : (ap@(ap@(ap@(c_2Eind__type_2ECONSTR@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a))@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))@(ap@(ap@(c_2Epair_2E_2C@ty_2Equote_2Eindex@A_27a)@(c_2Ebool_2EARB@ty_2Equote_2Eindex))@(c_2Ebool_2EARB@A_27a)))@(ap@(ap@(c_2Eind__type_2EFCONS@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a)))@V17a0)@(ap@(ap@(c_2Eind__type_2EFCONS@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a)))@V18a1)@(lam@ty_2Enum_2Enum@(^ [V19n:$i] : (c_2Eind__type_2EBOTTOM@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a)))))))))))@V15a0)@V16a1)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V2_27polynom_27@V15a0))@(ap@V2_27polynom_27@V16a1))))))))))@(ap@(c_2Ebool_2E_3F@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a)))@(lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a))@(^ [V20a:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a)))@V3a0_27)@(ap@(lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a))@(^ [V21a:$i] : (ap@(ap@(ap@(c_2Eind__type_2ECONSTR@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a))@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))@(ap@(ap@(c_2Epair_2E_2C@ty_2Equote_2Eindex@A_27a)@(c_2Ebool_2EARB@ty_2Equote_2Eindex))@(c_2Ebool_2EARB@A_27a)))@(ap@(ap@(c_2Eind__type_2EFCONS@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a)))@V21a)@(lam@ty_2Enum_2Enum@(^ [V22n:$i] : (c_2Eind__type_2EBOTTOM@(ty_2Epair_2Eprod@ty_2Equote_2Eindex@A_27a))))))))@V20a)))@(ap@V2_27polynom_27@V20a))))))))))@(ap@V2_27polynom_27@V3a0_27))))))@(ap@V2_27polynom_27@V1a0_27))))))))@V0rep)))))).
thf(ax_thm_2EringNorm_2Epolynom__case__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0a:tp__ty_2Equote_2Eindex] : ( ! [V1f:$i] : ((mem@V1f@(arr@ty_2Equote_2Eindex@A_27b)) => ( ! [V2f1:$i] : ((mem@V2f1@(arr@A_27a@A_27b)) => ( ! [V3f2:$i] : ((mem@V3f2@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(arr@(ty_2EringNorm_2Epolynom@A_27a)@A_27b))) => ( ! [V4f3:$i] : ((mem@V4f3@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(arr@(ty_2EringNorm_2Epolynom@A_27a)@A_27b))) => ( ! [V5f4:$i] : ((mem@V5f4@(arr@(ty_2EringNorm_2Epolynom@A_27a)@A_27b)) => ((ap@(ap@(ap@(ap@(ap@(ap@(c_2EringNorm_2Epolynom__CASE@A_27a@A_27b)@(ap@(c_2EringNorm_2EPvar@A_27a)@(inj__ty_2Equote_2Eindex @ V0a)))@V1f)@V2f1)@V3f2)@V4f3)@V5f4) = (ap@V1f@(inj__ty_2Equote_2Eindex @ V0a)))))))))))))) & (( ! [V6a:$i] : ((mem@V6a@A_27a) => ( ! [V7f:$i] : ((mem@V7f@(arr@ty_2Equote_2Eindex@A_27b)) => ( ! [V8f1:$i] : ((mem@V8f1@(arr@A_27a@A_27b)) => ( ! [V9f2:$i] : ((mem@V9f2@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(arr@(ty_2EringNorm_2Epolynom@A_27a)@A_27b))) => ( ! [V10f3:$i] : ((mem@V10f3@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(arr@(ty_2EringNorm_2Epolynom@A_27a)@A_27b))) => ( ! [V11f4:$i] : ((mem@V11f4@(arr@(ty_2EringNorm_2Epolynom@A_27a)@A_27b)) => ((ap@(ap@(ap@(ap@(ap@(ap@(c_2EringNorm_2Epolynom__CASE@A_27a@A_27b)@(ap@(c_2EringNorm_2EPconst@A_27a)@V6a))@V7f)@V8f1)@V9f2)@V10f3)@V11f4) = (ap@V8f1@V6a)))))))))))))) & (( ! [V12a0:$i] : ((mem@V12a0@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V13a1:$i] : ((mem@V13a1@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V14f:$i] : ((mem@V14f@(arr@ty_2Equote_2Eindex@A_27b)) => ( ! [V15f1:$i] : ((mem@V15f1@(arr@A_27a@A_27b)) => ( ! [V16f2:$i] : ((mem@V16f2@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(arr@(ty_2EringNorm_2Epolynom@A_27a)@A_27b))) => ( ! [V17f3:$i] : ((mem@V17f3@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(arr@(ty_2EringNorm_2Epolynom@A_27a)@A_27b))) => ( ! [V18f4:$i] : ((mem@V18f4@(arr@(ty_2EringNorm_2Epolynom@A_27a)@A_27b)) => ((ap@(ap@(ap@(ap@(ap@(ap@(c_2EringNorm_2Epolynom__CASE@A_27a@A_27b)@(ap@(ap@(c_2EringNorm_2EPplus@A_27a)@V12a0)@V13a1))@V14f)@V15f1)@V16f2)@V17f3)@V18f4) = (ap@(ap@V16f2@V12a0)@V13a1)))))))))))))))) & (( ! [V19a0:$i] : ((mem@V19a0@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V20a1:$i] : ((mem@V20a1@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V21f:$i] : ((mem@V21f@(arr@ty_2Equote_2Eindex@A_27b)) => ( ! [V22f1:$i] : ((mem@V22f1@(arr@A_27a@A_27b)) => ( ! [V23f2:$i] : ((mem@V23f2@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(arr@(ty_2EringNorm_2Epolynom@A_27a)@A_27b))) => ( ! [V24f3:$i] : ((mem@V24f3@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(arr@(ty_2EringNorm_2Epolynom@A_27a)@A_27b))) => ( ! [V25f4:$i] : ((mem@V25f4@(arr@(ty_2EringNorm_2Epolynom@A_27a)@A_27b)) => ((ap@(ap@(ap@(ap@(ap@(ap@(c_2EringNorm_2Epolynom__CASE@A_27a@A_27b)@(ap@(ap@(c_2EringNorm_2EPmult@A_27a)@V19a0)@V20a1))@V21f)@V22f1)@V23f2)@V24f3)@V25f4) = (ap@(ap@V24f3@V19a0)@V20a1)))))))))))))))) & ( ! [V26a:$i] : ((mem@V26a@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V27f:$i] : ((mem@V27f@(arr@ty_2Equote_2Eindex@A_27b)) => ( ! [V28f1:$i] : ((mem@V28f1@(arr@A_27a@A_27b)) => ( ! [V29f2:$i] : ((mem@V29f2@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(arr@(ty_2EringNorm_2Epolynom@A_27a)@A_27b))) => ( ! [V30f3:$i] : ((mem@V30f3@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(arr@(ty_2EringNorm_2Epolynom@A_27a)@A_27b))) => ( ! [V31f4:$i] : ((mem@V31f4@(arr@(ty_2EringNorm_2Epolynom@A_27a)@A_27b)) => ((ap@(ap@(ap@(ap@(ap@(ap@(c_2EringNorm_2Epolynom__CASE@A_27a@A_27b)@(ap@(c_2EringNorm_2EPopp@A_27a)@V26a))@V27f)@V28f1)@V29f2)@V30f3)@V31f4) = (ap@V31f4@V26a))))))))))))))))))))).
thf(ax_thm_2EringNorm_2Epolynom__size__def,axiom,( ! [A_27a:del]: (( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1a:tp__ty_2Equote_2Eindex] : ((surj__ty_2Enum_2Enum @ (ap@(ap@(c_2EringNorm_2Epolynom__size@A_27a)@V0f)@(ap@(c_2EringNorm_2EPvar@A_27a)@(inj__ty_2Equote_2Eindex @ V1a)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@c_2Equote_2Eindex__size@(inj__ty_2Equote_2Eindex @ V1a)))))))) & (( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V3a:$i] : ((mem@V3a@A_27a) => ((surj__ty_2Enum_2Enum @ (ap@(ap@(c_2EringNorm_2Epolynom__size@A_27a)@V2f)@(ap@(c_2EringNorm_2EPconst@A_27a)@V3a))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@V2f@V3a)))))))) & (( ! [V4f:$i] : ((mem@V4f@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V5a0:$i] : ((mem@V5a0@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V6a1:$i] : ((mem@V6a1@(ty_2EringNorm_2Epolynom@A_27a)) => ((surj__ty_2Enum_2Enum @ (ap@(ap@(c_2EringNorm_2Epolynom__size@A_27a)@V4f)@(ap@(ap@(c_2EringNorm_2EPplus@A_27a)@V5a0)@V6a1))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@(c_2EringNorm_2Epolynom__size@A_27a)@V4f)@V5a0))@(ap@(ap@(c_2EringNorm_2Epolynom__size@A_27a)@V4f)@V6a1))))))))))) & (( ! [V7f:$i] : ((mem@V7f@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V8a0:$i] : ((mem@V8a0@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V9a1:$i] : ((mem@V9a1@(ty_2EringNorm_2Epolynom@A_27a)) => ((surj__ty_2Enum_2Enum @ (ap@(ap@(c_2EringNorm_2Epolynom__size@A_27a)@V7f)@(ap@(ap@(c_2EringNorm_2EPmult@A_27a)@V8a0)@V9a1))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@(c_2EringNorm_2Epolynom__size@A_27a)@V7f)@V8a0))@(ap@(ap@(c_2EringNorm_2Epolynom__size@A_27a)@V7f)@V9a1))))))))))) & ( ! [V10f:$i] : ((mem@V10f@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V11a:$i] : ((mem@V11a@(ty_2EringNorm_2Epolynom@A_27a)) => ((surj__ty_2Enum_2Enum @ (ap@(ap@(c_2EringNorm_2Epolynom__size@A_27a)@V10f)@(ap@(c_2EringNorm_2EPopp@A_27a)@V11a))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@(ap@(c_2EringNorm_2Epolynom__size@A_27a)@V10f)@V11a)))))))))))))).
thf(conj_thm_2EringNorm_2Edatatype__polynom,lemma,( ! [A_27a:del]: ( ! [V0polynom:$i] : ((mem@V0polynom@(arr@(arr@ty_2Equote_2Eindex@(ty_2EringNorm_2Epolynom@A_27a))@(arr@(arr@A_27a@(ty_2EringNorm_2Epolynom@A_27a))@(arr@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(ty_2EringNorm_2Epolynom@A_27a)))@(arr@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(ty_2EringNorm_2Epolynom@A_27a)))@(arr@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(ty_2EringNorm_2Epolynom@A_27a))@bool)))))) => (p@(ap@(c_2Ebool_2EDATATYPE@bool)@(ap@(ap@(ap@(ap@(ap@V0polynom@(c_2EringNorm_2EPvar@A_27a))@(c_2EringNorm_2EPconst@A_27a))@(c_2EringNorm_2EPplus@A_27a))@(c_2EringNorm_2EPmult@A_27a))@(c_2EringNorm_2EPopp@A_27a)))))))).
thf(conj_thm_2EringNorm_2Epolynom__11,lemma,( ! [A_27a:del]: (( ! [V0a:tp__ty_2Equote_2Eindex] : ( ! [V1a_27:tp__ty_2Equote_2Eindex] : (((ap@(c_2EringNorm_2EPvar@A_27a)@(inj__ty_2Equote_2Eindex @ V0a)) = (ap@(c_2EringNorm_2EPvar@A_27a)@(inj__ty_2Equote_2Eindex @ V1a_27))) <=> (V0a = V1a_27)))) & (( ! [V2a:$i] : ((mem@V2a@A_27a) => ( ! [V3a_27:$i] : ((mem@V3a_27@A_27a) => (((ap@(c_2EringNorm_2EPconst@A_27a)@V2a) = (ap@(c_2EringNorm_2EPconst@A_27a)@V3a_27)) <=> (V2a = V3a_27)))))) & (( ! [V4a0:$i] : ((mem@V4a0@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V5a1:$i] : ((mem@V5a1@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V6a0_27:$i] : ((mem@V6a0_27@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V7a1_27:$i] : ((mem@V7a1_27@(ty_2EringNorm_2Epolynom@A_27a)) => (((ap@(ap@(c_2EringNorm_2EPplus@A_27a)@V4a0)@V5a1) = (ap@(ap@(c_2EringNorm_2EPplus@A_27a)@V6a0_27)@V7a1_27)) <=> ((V4a0 = V6a0_27) & (V5a1 = V7a1_27))))))))))) & (( ! [V8a0:$i] : ((mem@V8a0@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V9a1:$i] : ((mem@V9a1@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V10a0_27:$i] : ((mem@V10a0_27@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V11a1_27:$i] : ((mem@V11a1_27@(ty_2EringNorm_2Epolynom@A_27a)) => (((ap@(ap@(c_2EringNorm_2EPmult@A_27a)@V8a0)@V9a1) = (ap@(ap@(c_2EringNorm_2EPmult@A_27a)@V10a0_27)@V11a1_27)) <=> ((V8a0 = V10a0_27) & (V9a1 = V11a1_27))))))))))) & ( ! [V12a:$i] : ((mem@V12a@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V13a_27:$i] : ((mem@V13a_27@(ty_2EringNorm_2Epolynom@A_27a)) => (((ap@(c_2EringNorm_2EPopp@A_27a)@V12a) = (ap@(c_2EringNorm_2EPopp@A_27a)@V13a_27)) <=> (V12a = V13a_27)))))))))))).
thf(conj_thm_2EringNorm_2Epolynom__distinct,lemma,( ! [A_27a:del]: (( ! [V0a_27:$i] : ((mem@V0a_27@A_27a) => ( ! [V1a:tp__ty_2Equote_2Eindex] : (~~ ((ap@(c_2EringNorm_2EPvar@A_27a)@(inj__ty_2Equote_2Eindex @ V1a)) = (ap@(c_2EringNorm_2EPconst@A_27a)@V0a_27)))))) & (( ! [V2a1:$i] : ((mem@V2a1@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V3a0:$i] : ((mem@V3a0@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V4a:tp__ty_2Equote_2Eindex] : (~~ ((ap@(c_2EringNorm_2EPvar@A_27a)@(inj__ty_2Equote_2Eindex @ V4a)) = (ap@(ap@(c_2EringNorm_2EPplus@A_27a)@V3a0)@V2a1)))))))) & (( ! [V5a1:$i] : ((mem@V5a1@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V6a0:$i] : ((mem@V6a0@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V7a:tp__ty_2Equote_2Eindex] : (~~ ((ap@(c_2EringNorm_2EPvar@A_27a)@(inj__ty_2Equote_2Eindex @ V7a)) = (ap@(ap@(c_2EringNorm_2EPmult@A_27a)@V6a0)@V5a1)))))))) & (( ! [V8a_27:$i] : ((mem@V8a_27@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V9a:tp__ty_2Equote_2Eindex] : (~~ ((ap@(c_2EringNorm_2EPvar@A_27a)@(inj__ty_2Equote_2Eindex @ V9a)) = (ap@(c_2EringNorm_2EPopp@A_27a)@V8a_27)))))) & (( ! [V10a1:$i] : ((mem@V10a1@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V11a0:$i] : ((mem@V11a0@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V12a:$i] : ((mem@V12a@A_27a) => (~~ ((ap@(c_2EringNorm_2EPconst@A_27a)@V12a) = (ap@(ap@(c_2EringNorm_2EPplus@A_27a)@V11a0)@V10a1))))))))) & (( ! [V13a1:$i] : ((mem@V13a1@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V14a0:$i] : ((mem@V14a0@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V15a:$i] : ((mem@V15a@A_27a) => (~~ ((ap@(c_2EringNorm_2EPconst@A_27a)@V15a) = (ap@(ap@(c_2EringNorm_2EPmult@A_27a)@V14a0)@V13a1))))))))) & (( ! [V16a_27:$i] : ((mem@V16a_27@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V17a:$i] : ((mem@V17a@A_27a) => (~~ ((ap@(c_2EringNorm_2EPconst@A_27a)@V17a) = (ap@(c_2EringNorm_2EPopp@A_27a)@V16a_27))))))) & (( ! [V18a1_27:$i] : ((mem@V18a1_27@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V19a1:$i] : ((mem@V19a1@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V20a0_27:$i] : ((mem@V20a0_27@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V21a0:$i] : ((mem@V21a0@(ty_2EringNorm_2Epolynom@A_27a)) => (~~ ((ap@(ap@(c_2EringNorm_2EPplus@A_27a)@V21a0)@V19a1) = (ap@(ap@(c_2EringNorm_2EPmult@A_27a)@V20a0_27)@V18a1_27))))))))))) & (( ! [V22a1:$i] : ((mem@V22a1@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V23a0:$i] : ((mem@V23a0@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V24a:$i] : ((mem@V24a@(ty_2EringNorm_2Epolynom@A_27a)) => (~~ ((ap@(ap@(c_2EringNorm_2EPplus@A_27a)@V23a0)@V22a1) = (ap@(c_2EringNorm_2EPopp@A_27a)@V24a))))))))) & ( ! [V25a1:$i] : ((mem@V25a1@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V26a0:$i] : ((mem@V26a0@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V27a:$i] : ((mem@V27a@(ty_2EringNorm_2Epolynom@A_27a)) => (~~ ((ap@(ap@(c_2EringNorm_2EPmult@A_27a)@V26a0)@V25a1) = (ap@(c_2EringNorm_2EPopp@A_27a)@V27a)))))))))))))))))))).
thf(conj_thm_2EringNorm_2Epolynom__nchotomy,lemma,( ! [A_27a:del]: ( ! [V0pp:$i] : ((mem@V0pp@(ty_2EringNorm_2Epolynom@A_27a)) => ((? [V1i:tp__ty_2Equote_2Eindex] : (V0pp = (ap@(c_2EringNorm_2EPvar@A_27a)@(inj__ty_2Equote_2Eindex @ V1i)))) | ((? [V2a:$i] : ((mem@V2a@A_27a) & (V0pp = (ap@(c_2EringNorm_2EPconst@A_27a)@V2a)))) | ((? [V3p:$i] : ((mem@V3p@(ty_2EringNorm_2Epolynom@A_27a)) & (? [V4p0:$i] : ((mem@V4p0@(ty_2EringNorm_2Epolynom@A_27a)) & (V0pp = (ap@(ap@(c_2EringNorm_2EPplus@A_27a)@V3p)@V4p0)))))) | ((? [V5p:$i] : ((mem@V5p@(ty_2EringNorm_2Epolynom@A_27a)) & (? [V6p0:$i] : ((mem@V6p0@(ty_2EringNorm_2Epolynom@A_27a)) & (V0pp = (ap@(ap@(c_2EringNorm_2EPmult@A_27a)@V5p)@V6p0)))))) | (? [V7p:$i] : ((mem@V7p@(ty_2EringNorm_2Epolynom@A_27a)) & (V0pp = (ap@(c_2EringNorm_2EPopp@A_27a)@V7p)))))))))))).
thf(conj_thm_2EringNorm_2Epolynom__Axiom,conjecture,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f0:$i] : ((mem@V0f0@(arr@ty_2Equote_2Eindex@A_27b)) => ( ! [V1f1:$i] : ((mem@V1f1@(arr@A_27a@A_27b)) => ( ! [V2f2:$i] : ((mem@V2f2@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(arr@A_27b@(arr@A_27b@A_27b))))) => ( ! [V3f3:$i] : ((mem@V3f3@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(arr@A_27b@(arr@A_27b@A_27b))))) => ( ! [V4f4:$i] : ((mem@V4f4@(arr@(ty_2EringNorm_2Epolynom@A_27a)@(arr@A_27b@A_27b))) => (? [V5fn:$i] : ((mem@V5fn@(arr@(ty_2EringNorm_2Epolynom@A_27a)@A_27b)) & (( ! [V6a:tp__ty_2Equote_2Eindex] : ((ap@V5fn@(ap@(c_2EringNorm_2EPvar@A_27a)@(inj__ty_2Equote_2Eindex @ V6a))) = (ap@V0f0@(inj__ty_2Equote_2Eindex @ V6a)))) & (( ! [V7a:$i] : ((mem@V7a@A_27a) => ((ap@V5fn@(ap@(c_2EringNorm_2EPconst@A_27a)@V7a)) = (ap@V1f1@V7a)))) & (( ! [V8a0:$i] : ((mem@V8a0@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V9a1:$i] : ((mem@V9a1@(ty_2EringNorm_2Epolynom@A_27a)) => ((ap@V5fn@(ap@(ap@(c_2EringNorm_2EPplus@A_27a)@V8a0)@V9a1)) = (ap@(ap@(ap@(ap@V2f2@V8a0)@V9a1)@(ap@V5fn@V8a0))@(ap@V5fn@V9a1))))))) & (( ! [V10a0:$i] : ((mem@V10a0@(ty_2EringNorm_2Epolynom@A_27a)) => ( ! [V11a1:$i] : ((mem@V11a1@(ty_2EringNorm_2Epolynom@A_27a)) => ((ap@V5fn@(ap@(ap@(c_2EringNorm_2EPmult@A_27a)@V10a0)@V11a1)) = (ap@(ap@(ap@(ap@V3f3@V10a0)@V11a1)@(ap@V5fn@V10a0))@(ap@V5fn@V11a1))))))) & ( ! [V12a:$i] : ((mem@V12a@(ty_2EringNorm_2Epolynom@A_27a)) => ((ap@V5fn@(ap@(c_2EringNorm_2EPopp@A_27a)@V12a)) = (ap@(ap@V4f4@V12a)@(ap@V5fn@V12a)))))))))))))))))))))))).
