include('Axioms/fmapal_2.ax').
tff(tp_ty_2EringNorm_2Epolynom,type,( ty_2EringNorm_2Epolynom: del > del )).
tff(tp_c_2EringNorm_2EPconst,type,(c_2EringNorm_2EPconst:del > $i)).
tff(mem_c_2EringNorm_2EPconst,axiom,( ! [A_27a:del] : mem(c_2EringNorm_2EPconst(A_27a),arr(A_27a,ty_2EringNorm_2Epolynom(A_27a))))).
tff(tp_c_2EringNorm_2EPmult,type,(c_2EringNorm_2EPmult:del > $i)).
tff(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)))))).
tff(tp_c_2EringNorm_2EPopp,type,(c_2EringNorm_2EPopp:del > $i)).
tff(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))))).
tff(tp_c_2EringNorm_2EPplus,type,(c_2EringNorm_2EPplus:del > $i)).
tff(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)))))).
tff(tp_c_2EringNorm_2EPvar,type,(c_2EringNorm_2EPvar:del > $i)).
tff(mem_c_2EringNorm_2EPvar,axiom,( ! [A_27a:del] : mem(c_2EringNorm_2EPvar(A_27a),arr(ty_2Equote_2Eindex,ty_2EringNorm_2Epolynom(A_27a))))).
tff(tp_c_2EringNorm_2Einterp__p,type,(c_2EringNorm_2Einterp__p:del > $i)).
tff(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)))))).
tff(tp_c_2EringNorm_2Epolynom__CASE,type,(c_2EringNorm_2Epolynom__CASE:(del * del) > $i)).
tff(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)))))))))).
tff(tp_c_2EringNorm_2Epolynom__normalize,type,(c_2EringNorm_2Epolynom__normalize:del > $i)).
tff(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)))))).
tff(tp_c_2EringNorm_2Epolynom__simplify,type,(c_2EringNorm_2Epolynom__simplify:del > $i)).
tff(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)))))).
tff(tp_c_2EringNorm_2Epolynom__size,type,(c_2EringNorm_2Epolynom__size:del > $i)).
tff(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))))).
tff(tp_c_2EringNorm_2Er__canonical__sum__merge,type,(c_2EringNorm_2Er__canonical__sum__merge:del > $i)).
tff(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))))))).
tff(tp_c_2EringNorm_2Er__canonical__sum__prod,type,(c_2EringNorm_2Er__canonical__sum__prod:del > $i)).
tff(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))))))).
tff(tp_c_2EringNorm_2Er__canonical__sum__scalar,type,(c_2EringNorm_2Er__canonical__sum__scalar:del > $i)).
tff(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))))))).
tff(tp_c_2EringNorm_2Er__canonical__sum__scalar2,type,(c_2EringNorm_2Er__canonical__sum__scalar2:del > $i)).
tff(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))))))).
tff(tp_c_2EringNorm_2Er__canonical__sum__scalar3,type,(c_2EringNorm_2Er__canonical__sum__scalar3:del > $i)).
tff(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)))))))).
tff(tp_c_2EringNorm_2Er__canonical__sum__simplify,type,(c_2EringNorm_2Er__canonical__sum__simplify:del > $i)).
tff(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)))))).
tff(tp_c_2EringNorm_2Er__ics__aux,type,(c_2EringNorm_2Er__ics__aux:del > $i)).
tff(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))))))).
tff(tp_c_2EringNorm_2Er__interp__cs,type,(c_2EringNorm_2Er__interp__cs:del > $i)).
tff(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)))))).
tff(tp_c_2EringNorm_2Er__interp__m,type,(c_2EringNorm_2Er__interp__m:del > $i)).
tff(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))))))).
tff(tp_c_2EringNorm_2Er__interp__sp,type,(c_2EringNorm_2Er__interp__sp:del > $i)).
tff(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)))))).
tff(tp_c_2EringNorm_2Er__interp__vl,type,(c_2EringNorm_2Er__interp__vl:del > $i)).
tff(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)))))).
tff(tp_c_2EringNorm_2Er__ivl__aux,type,(c_2EringNorm_2Er__ivl__aux:del > $i)).
tff(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))))))).
tff(tp_c_2EringNorm_2Er__monom__insert,type,(c_2EringNorm_2Er__monom__insert:del > $i)).
tff(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)))))))).
tff(tp_c_2EringNorm_2Er__spolynom__normalize,type,(c_2EringNorm_2Er__spolynom__normalize:del > $i)).
tff(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)))))).
tff(tp_c_2EringNorm_2Er__spolynom__simplify,type,(c_2EringNorm_2Er__spolynom__simplify:del > $i)).
tff(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)))))).
tff(tp_c_2EringNorm_2Er__varlist__insert,type,(c_2EringNorm_2Er__varlist__insert:del > $i)).
tff(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))))))).
tff(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))))))).
tff(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))))))).
tff(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))))))).
tff(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))))))).
tff(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))))))).
tff(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))))))).
tff(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))))))).
tff(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))))))).
tff(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))))))).
tff(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))))))).
tff(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))))))).
tff(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))))))).
tff(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))))))).
tff(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))))))).
tff(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))))))).
tff(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))))))).
tff(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))))))))))))))))).
tff(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)))))))))))))))).
tff(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))))))))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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)))))))))).
tff(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)))))))))))).
tff(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))))))))))).
tff(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))))))))).
tff(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))))))))))))))).
tff(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))))))))))))).
tff(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)))))))))))))))).
tff(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))))))))))))))))))).
tff(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)))))))))))))))).
tff(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))))))))))))))).
tff(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)))))))))).
tff(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)),f2667(A_27a)),V0rep)))))).
tff(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))))))))))))))))))))).
tff(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)))))))))))))).
tff(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))))))))).
tff(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))))))))))))).
tff(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))))))))))))))))))))).
tff(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))))))))))))).
tff(conj_thm_2EringNorm_2Epolynom__Axiom,lemma,(( ! [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))))))))))))))))))))))))).
tff(conj_thm_2EringNorm_2Epolynom__induction,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2EringNorm_2Epolynom(A_27a),bool)) => ((( ! [V1i:tp__ty_2Equote_2Eindex] : p(ap(V0P,ap(c_2EringNorm_2EPvar(A_27a),inj__ty_2Equote_2Eindex(V1i))))) & (( ! [V2a:$i] : (mem(V2a,A_27a) => p(ap(V0P,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)) => ((p(ap(V0P,V3p)) & p(ap(V0P,V4p0))) => p(ap(V0P,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)) => ((p(ap(V0P,V5p)) & p(ap(V0P,V6p0))) => p(ap(V0P,ap(ap(c_2EringNorm_2EPmult(A_27a),V5p),V6p0)))))))) & ( ! [V7p:$i] : (mem(V7p,ty_2EringNorm_2Epolynom(A_27a)) => (p(ap(V0P,V7p)) => p(ap(V0P,ap(c_2EringNorm_2EPopp(A_27a),V7p)))))))))) => ( ! [V8p:$i] : (mem(V8p,ty_2EringNorm_2Epolynom(A_27a)) => p(ap(V0P,V8p)))))))))).
tff(conj_thm_2EringNorm_2Epolynom__case__cong,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f_27:$i] : (mem(V0f_27,arr(ty_2Equote_2Eindex,A_27b)) => ( ! [V1f1_27:$i] : (mem(V1f1_27,arr(A_27a,A_27b)) => ( ! [V2f2_27:$i] : (mem(V2f2_27,arr(ty_2EringNorm_2Epolynom(A_27a),arr(ty_2EringNorm_2Epolynom(A_27a),A_27b))) => ( ! [V3f3_27:$i] : (mem(V3f3_27,arr(ty_2EringNorm_2Epolynom(A_27a),arr(ty_2EringNorm_2Epolynom(A_27a),A_27b))) => ( ! [V4f4_27:$i] : (mem(V4f4_27,arr(ty_2EringNorm_2Epolynom(A_27a),A_27b)) => ( ! [V5M:$i] : (mem(V5M,ty_2EringNorm_2Epolynom(A_27a)) => ( ! [V6M_27:$i] : (mem(V6M_27,ty_2EringNorm_2Epolynom(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)) => (((V5M = V6M_27) & (( ! [V12a:tp__ty_2Equote_2Eindex] : ((V6M_27 = ap(c_2EringNorm_2EPvar(A_27a),inj__ty_2Equote_2Eindex(V12a))) => (ap(V7f,inj__ty_2Equote_2Eindex(V12a)) = ap(V0f_27,inj__ty_2Equote_2Eindex(V12a))))) & (( ! [V13a:$i] : (mem(V13a,A_27a) => ((V6M_27 = ap(c_2EringNorm_2EPconst(A_27a),V13a)) => (ap(V8f1,V13a) = ap(V1f1_27,V13a))))) & (( ! [V14a0:$i] : (mem(V14a0,ty_2EringNorm_2Epolynom(A_27a)) => ( ! [V15a1:$i] : (mem(V15a1,ty_2EringNorm_2Epolynom(A_27a)) => ((V6M_27 = ap(ap(c_2EringNorm_2EPplus(A_27a),V14a0),V15a1)) => (ap(ap(V9f2,V14a0),V15a1) = ap(ap(V2f2_27,V14a0),V15a1))))))) & (( ! [V16a0:$i] : (mem(V16a0,ty_2EringNorm_2Epolynom(A_27a)) => ( ! [V17a1:$i] : (mem(V17a1,ty_2EringNorm_2Epolynom(A_27a)) => ((V6M_27 = ap(ap(c_2EringNorm_2EPmult(A_27a),V16a0),V17a1)) => (ap(ap(V10f3,V16a0),V17a1) = ap(ap(V3f3_27,V16a0),V17a1))))))) & ( ! [V18a:$i] : (mem(V18a,ty_2EringNorm_2Epolynom(A_27a)) => ((V6M_27 = ap(c_2EringNorm_2EPopp(A_27a),V18a)) => (ap(V11f4,V18a) = ap(V4f4_27,V18a)))))))))) => (ap(ap(ap(ap(ap(ap(c_2EringNorm_2Epolynom__CASE(A_27a,A_27b),V5M),V7f),V8f1),V9f2),V10f3),V11f4) = ap(ap(ap(ap(ap(ap(c_2EringNorm_2Epolynom__CASE(A_27a,A_27b),V6M_27),V0f_27),V1f1_27),V2f2_27),V3f3_27),V4f4_27))))))))))))))))))))))))))))))).
tff(conj_thm_2EringNorm_2Epolynom__case__eq,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,ty_2EringNorm_2Epolynom(A_27a)) => ( ! [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)) => ( ! [V6v:$i] : (mem(V6v,A_27b) => ((ap(ap(ap(ap(ap(ap(c_2EringNorm_2Epolynom__CASE(A_27a,A_27b),V0x),V1f),V2f1),V3f2),V4f3),V5f4) = V6v) <=> ((? [V7i:tp__ty_2Equote_2Eindex] : ((V0x = ap(c_2EringNorm_2EPvar(A_27a),inj__ty_2Equote_2Eindex(V7i))) & (ap(V1f,inj__ty_2Equote_2Eindex(V7i)) = V6v))) | ((? [V8a:$i] : (mem(V8a,A_27a) & ((V0x = ap(c_2EringNorm_2EPconst(A_27a),V8a)) & (ap(V2f1,V8a) = V6v)))) | ((? [V9p:$i] : (mem(V9p,ty_2EringNorm_2Epolynom(A_27a)) & (? [V10p0:$i] : (mem(V10p0,ty_2EringNorm_2Epolynom(A_27a)) & ((V0x = ap(ap(c_2EringNorm_2EPplus(A_27a),V9p),V10p0)) & (ap(ap(V3f2,V9p),V10p0) = V6v)))))) | ((? [V11p:$i] : (mem(V11p,ty_2EringNorm_2Epolynom(A_27a)) & (? [V12p0:$i] : (mem(V12p0,ty_2EringNorm_2Epolynom(A_27a)) & ((V0x = ap(ap(c_2EringNorm_2EPmult(A_27a),V11p),V12p0)) & (ap(ap(V4f3,V11p),V12p0) = V6v)))))) | (? [V13p:$i] : (mem(V13p,ty_2EringNorm_2Epolynom(A_27a)) & ((V0x = ap(c_2EringNorm_2EPopp(A_27a),V13p)) & (ap(V5f4,V13p) = V6v))))))))))))))))))))))))))).
tff(ax_thm_2EringNorm_2Epolynom__normalize__def,axiom,( ! [A_27a:del]: (( ! [V0r:$i] : (mem(V0r,ty_2Ering_2Ering(A_27a)) => ( ! [V1i:tp__ty_2Equote_2Eindex] : (ap(ap(c_2EringNorm_2Epolynom__normalize(A_27a),V0r),ap(c_2EringNorm_2EPvar(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)))))) & (( ! [V2r:$i] : (mem(V2r,ty_2Ering_2Ering(A_27a)) => ( ! [V3c:$i] : (mem(V3c,A_27a) => (ap(ap(c_2EringNorm_2Epolynom__normalize(A_27a),V2r),ap(c_2EringNorm_2EPconst(A_27a),V3c)) = ap(ap(ap(c_2Ecanonical_2ECons__monom(A_27a),V3c),c_2Elist_2ENIL(ty_2Equote_2Eindex)),c_2Ecanonical_2ENil__monom(A_27a))))))) & (( ! [V4r:$i] : (mem(V4r,ty_2Ering_2Ering(A_27a)) => ( ! [V5pl:$i] : (mem(V5pl,ty_2EringNorm_2Epolynom(A_27a)) => ( ! [V6pr:$i] : (mem(V6pr,ty_2EringNorm_2Epolynom(A_27a)) => (ap(ap(c_2EringNorm_2Epolynom__normalize(A_27a),V4r),ap(ap(c_2EringNorm_2EPplus(A_27a),V5pl),V6pr)) = ap(ap(ap(c_2EringNorm_2Er__canonical__sum__merge(A_27a),V4r),ap(ap(c_2EringNorm_2Epolynom__normalize(A_27a),V4r),V5pl)),ap(ap(c_2EringNorm_2Epolynom__normalize(A_27a),V4r),V6pr))))))))) & (( ! [V7r:$i] : (mem(V7r,ty_2Ering_2Ering(A_27a)) => ( ! [V8pl:$i] : (mem(V8pl,ty_2EringNorm_2Epolynom(A_27a)) => ( ! [V9pr:$i] : (mem(V9pr,ty_2EringNorm_2Epolynom(A_27a)) => (ap(ap(c_2EringNorm_2Epolynom__normalize(A_27a),V7r),ap(ap(c_2EringNorm_2EPmult(A_27a),V8pl),V9pr)) = ap(ap(ap(c_2EringNorm_2Er__canonical__sum__prod(A_27a),V7r),ap(ap(c_2EringNorm_2Epolynom__normalize(A_27a),V7r),V8pl)),ap(ap(c_2EringNorm_2Epolynom__normalize(A_27a),V7r),V9pr))))))))) & ( ! [V10r:$i] : (mem(V10r,ty_2Ering_2Ering(A_27a)) => ( ! [V11p:$i] : (mem(V11p,ty_2EringNorm_2Epolynom(A_27a)) => (ap(ap(c_2EringNorm_2Epolynom__normalize(A_27a),V10r),ap(c_2EringNorm_2EPopp(A_27a),V11p)) = ap(ap(ap(ap(c_2EringNorm_2Er__canonical__sum__scalar3(A_27a),V10r),ap(ap(c_2Ering_2Ering__RN(A_27a),V10r),ap(c_2Ering_2Ering__R1(A_27a),V10r))),c_2Elist_2ENIL(ty_2Equote_2Eindex)),ap(ap(c_2EringNorm_2Epolynom__normalize(A_27a),V10r),V11p))))))))))))).
tff(ax_thm_2EringNorm_2Epolynom__simplify__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,ty_2Ering_2Ering(A_27a)) => ( ! [V1x:$i] : (mem(V1x,ty_2EringNorm_2Epolynom(A_27a)) => (ap(ap(c_2EringNorm_2Epolynom__simplify(A_27a),V0r),V1x) = ap(ap(c_2EringNorm_2Er__canonical__sum__simplify(A_27a),V0r),ap(ap(c_2EringNorm_2Epolynom__normalize(A_27a),V0r),V1x))))))))).
tff(ax_thm_2EringNorm_2Einterp__p__def,axiom,( ! [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_2Einterp__p(A_27a),V0r),V1vm),ap(c_2EringNorm_2EPconst(A_27a),V2c)) = V2c))))))) & (( ! [V3r:$i] : (mem(V3r,ty_2Ering_2Ering(A_27a)) => ( ! [V4vm:$i] : (mem(V4vm,ty_2Equote_2Evarmap(A_27a)) => ( ! [V5i:tp__ty_2Equote_2Eindex] : (ap(ap(ap(c_2EringNorm_2Einterp__p(A_27a),V3r),V4vm),ap(c_2EringNorm_2EPvar(A_27a),inj__ty_2Equote_2Eindex(V5i))) = ap(ap(c_2Equote_2Evarmap__find(A_27a),inj__ty_2Equote_2Eindex(V5i)),V4vm))))))) & (( ! [V6r:$i] : (mem(V6r,ty_2Ering_2Ering(A_27a)) => ( ! [V7vm:$i] : (mem(V7vm,ty_2Equote_2Evarmap(A_27a)) => ( ! [V8p1:$i] : (mem(V8p1,ty_2EringNorm_2Epolynom(A_27a)) => ( ! [V9p2:$i] : (mem(V9p2,ty_2EringNorm_2Epolynom(A_27a)) => (ap(ap(ap(c_2EringNorm_2Einterp__p(A_27a),V6r),V7vm),ap(ap(c_2EringNorm_2EPplus(A_27a),V8p1),V9p2)) = ap(ap(ap(c_2Ering_2Ering__RP(A_27a),V6r),ap(ap(ap(c_2EringNorm_2Einterp__p(A_27a),V6r),V7vm),V8p1)),ap(ap(ap(c_2EringNorm_2Einterp__p(A_27a),V6r),V7vm),V9p2))))))))))) & (( ! [V10r:$i] : (mem(V10r,ty_2Ering_2Ering(A_27a)) => ( ! [V11vm:$i] : (mem(V11vm,ty_2Equote_2Evarmap(A_27a)) => ( ! [V12p1:$i] : (mem(V12p1,ty_2EringNorm_2Epolynom(A_27a)) => ( ! [V13p2:$i] : (mem(V13p2,ty_2EringNorm_2Epolynom(A_27a)) => (ap(ap(ap(c_2EringNorm_2Einterp__p(A_27a),V10r),V11vm),ap(ap(c_2EringNorm_2EPmult(A_27a),V12p1),V13p2)) = ap(ap(ap(c_2Ering_2Ering__RM(A_27a),V10r),ap(ap(ap(c_2EringNorm_2Einterp__p(A_27a),V10r),V11vm),V12p1)),ap(ap(ap(c_2EringNorm_2Einterp__p(A_27a),V10r),V11vm),V13p2))))))))))) & ( ! [V14r:$i] : (mem(V14r,ty_2Ering_2Ering(A_27a)) => ( ! [V15vm:$i] : (mem(V15vm,ty_2Equote_2Evarmap(A_27a)) => ( ! [V16p1:$i] : (mem(V16p1,ty_2EringNorm_2Epolynom(A_27a)) => (ap(ap(ap(c_2EringNorm_2Einterp__p(A_27a),V14r),V15vm),ap(c_2EringNorm_2EPopp(A_27a),V16p1)) = ap(ap(c_2Ering_2Ering__RN(A_27a),V14r),ap(ap(ap(c_2EringNorm_2Einterp__p(A_27a),V14r),V15vm),V16p1))))))))))))))).
tff(conj_thm_2EringNorm_2Epolynom__normalize__ok,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,ty_2Ering_2Ering(A_27a)) => (p(ap(c_2Ering_2Eis__ring(A_27a),V0r)) => ( ! [V1vm:$i] : (mem(V1vm,ty_2Equote_2Evarmap(A_27a)) => ( ! [V2p:$i] : (mem(V2p,ty_2EringNorm_2Epolynom(A_27a)) => (ap(ap(ap(c_2EringNorm_2Er__interp__cs(A_27a),V0r),V1vm),ap(ap(c_2EringNorm_2Epolynom__normalize(A_27a),V0r),V2p)) = ap(ap(ap(c_2EringNorm_2Einterp__p(A_27a),V0r),V1vm),V2p)))))))))))).
tff(conj_thm_2EringNorm_2Epolynom__simplify__ok,conjecture,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,ty_2Ering_2Ering(A_27a)) => (p(ap(c_2Ering_2Eis__ring(A_27a),V0r)) => ( ! [V1vm:$i] : (mem(V1vm,ty_2Equote_2Evarmap(A_27a)) => ( ! [V2p:$i] : (mem(V2p,ty_2EringNorm_2Epolynom(A_27a)) => (ap(ap(ap(c_2EringNorm_2Er__interp__cs(A_27a),V0r),V1vm),ap(ap(c_2EringNorm_2Epolynom__simplify(A_27a),V0r),V2p)) = ap(ap(ap(c_2EringNorm_2Einterp__p(A_27a),V0r),V1vm),V2p)))))))))))).
