include('Axioms/string_num^2.ax').
thf(tp_ty_2Ering_2Ering,type,( ty_2Ering_2Ering: del >del )).
thf(tp_c_2Ering_2Eis__ring,type,(c_2Ering_2Eis__ring:(del>$i))).
thf(mem_c_2Ering_2Eis__ring,axiom,( ! [A_27a:del] : (mem@(c_2Ering_2Eis__ring@A_27a)@(arr@(ty_2Ering_2Ering@A_27a)@bool)))).
thf(tp_c_2Ering_2Erecordtype_2Ering,type,(c_2Ering_2Erecordtype_2Ering:(del>$i))).
thf(mem_c_2Ering_2Erecordtype_2Ering,axiom,( ! [A_27a:del] : (mem@(c_2Ering_2Erecordtype_2Ering@A_27a)@(arr@A_27a@(arr@A_27a@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@(arr@A_27a@A_27a)@(ty_2Ering_2Ering@A_27a))))))))).
thf(tp_c_2Ering_2Ering__CASE,type,(c_2Ering_2Ering__CASE:(del>(del>$i)))).
thf(mem_c_2Ering_2Ering__CASE,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Ering_2Ering__CASE@A_27a@A_27b)@(arr@(ty_2Ering_2Ering@A_27a)@(arr@(arr@A_27a@(arr@A_27a@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@(arr@A_27a@A_27a)@A_27b)))))@A_27b)))))).
thf(tp_c_2Ering_2Ering__R0,type,(c_2Ering_2Ering__R0:(del>$i))).
thf(mem_c_2Ering_2Ering__R0,axiom,( ! [A_27a:del] : (mem@(c_2Ering_2Ering__R0@A_27a)@(arr@(ty_2Ering_2Ering@A_27a)@A_27a)))).
thf(tp_c_2Ering_2Ering__R0__fupd,type,(c_2Ering_2Ering__R0__fupd:(del>$i))).
thf(mem_c_2Ering_2Ering__R0__fupd,axiom,( ! [A_27a:del] : (mem@(c_2Ering_2Ering__R0__fupd@A_27a)@(arr@(arr@A_27a@A_27a)@(arr@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)))))).
thf(tp_c_2Ering_2Ering__R1,type,(c_2Ering_2Ering__R1:(del>$i))).
thf(mem_c_2Ering_2Ering__R1,axiom,( ! [A_27a:del] : (mem@(c_2Ering_2Ering__R1@A_27a)@(arr@(ty_2Ering_2Ering@A_27a)@A_27a)))).
thf(tp_c_2Ering_2Ering__R1__fupd,type,(c_2Ering_2Ering__R1__fupd:(del>$i))).
thf(mem_c_2Ering_2Ering__R1__fupd,axiom,( ! [A_27a:del] : (mem@(c_2Ering_2Ering__R1__fupd@A_27a)@(arr@(arr@A_27a@A_27a)@(arr@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)))))).
thf(tp_c_2Ering_2Ering__RM,type,(c_2Ering_2Ering__RM:(del>$i))).
thf(mem_c_2Ering_2Ering__RM,axiom,( ! [A_27a:del] : (mem@(c_2Ering_2Ering__RM@A_27a)@(arr@(ty_2Ering_2Ering@A_27a)@(arr@A_27a@(arr@A_27a@A_27a)))))).
thf(tp_c_2Ering_2Ering__RM__fupd,type,(c_2Ering_2Ering__RM__fupd:(del>$i))).
thf(mem_c_2Ering_2Ering__RM__fupd,axiom,( ! [A_27a:del] : (mem@(c_2Ering_2Ering__RM__fupd@A_27a)@(arr@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))@(arr@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)))))).
thf(tp_c_2Ering_2Ering__RN,type,(c_2Ering_2Ering__RN:(del>$i))).
thf(mem_c_2Ering_2Ering__RN,axiom,( ! [A_27a:del] : (mem@(c_2Ering_2Ering__RN@A_27a)@(arr@(ty_2Ering_2Ering@A_27a)@(arr@A_27a@A_27a))))).
thf(tp_c_2Ering_2Ering__RN__fupd,type,(c_2Ering_2Ering__RN__fupd:(del>$i))).
thf(mem_c_2Ering_2Ering__RN__fupd,axiom,( ! [A_27a:del] : (mem@(c_2Ering_2Ering__RN__fupd@A_27a)@(arr@(arr@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))@(arr@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)))))).
thf(tp_c_2Ering_2Ering__RP,type,(c_2Ering_2Ering__RP:(del>$i))).
thf(mem_c_2Ering_2Ering__RP,axiom,( ! [A_27a:del] : (mem@(c_2Ering_2Ering__RP@A_27a)@(arr@(ty_2Ering_2Ering@A_27a)@(arr@A_27a@(arr@A_27a@A_27a)))))).
thf(tp_c_2Ering_2Ering__RP__fupd,type,(c_2Ering_2Ering__RP__fupd:(del>$i))).
thf(mem_c_2Ering_2Ering__RP__fupd,axiom,( ! [A_27a:del] : (mem@(c_2Ering_2Ering__RP__fupd@A_27a)@(arr@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))@(arr@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)))))).
thf(tp_c_2Ering_2Ering__size,type,(c_2Ering_2Ering__size:(del>$i))).
thf(mem_c_2Ering_2Ering__size,axiom,( ! [A_27a:del] : (mem@(c_2Ering_2Ering__size@A_27a)@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@(ty_2Ering_2Ering@A_27a)@ty_2Enum_2Enum))))).
thf(tp_c_2Ering_2Esemi__ring__of,type,(c_2Ering_2Esemi__ring__of:(del>$i))).
thf(mem_c_2Ering_2Esemi__ring__of,axiom,( ! [A_27a:del] : (mem@(c_2Ering_2Esemi__ring__of@A_27a)@(arr@(ty_2Ering_2Ering@A_27a)@(ty_2Esemi__ring_2Esemi__ring@A_27a))))).
thf(ax_thm_2Ering_2Ering__TY__DEF,axiom,( ! [A_27a:del]: (? [V0rep:$i] : ((mem@V0rep@(arr@(ty_2Ering_2Ering@A_27a)@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@A_27a@(ty_2Epair_2Eprod@A_27a@(ty_2Epair_2Eprod@(arr@A_27a@(arr@A_27a@A_27a))@(ty_2Epair_2Eprod@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@A_27a)))))))) & (p@(ap@(ap@(c_2Ebool_2ETYPE__DEFINITION@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@A_27a@(ty_2Epair_2Eprod@A_27a@(ty_2Epair_2Eprod@(arr@A_27a@(arr@A_27a@A_27a))@(ty_2Epair_2Eprod@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@A_27a))))))@(ty_2Ering_2Ering@A_27a))@(lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@A_27a@(ty_2Epair_2Eprod@A_27a@(ty_2Epair_2Eprod@(arr@A_27a@(arr@A_27a@A_27a))@(ty_2Epair_2Eprod@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@A_27a))))))@(^ [V1a0_27:$i] : (ap@(c_2Ebool_2E_21@(arr@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@A_27a@(ty_2Epair_2Eprod@A_27a@(ty_2Epair_2Eprod@(arr@A_27a@(arr@A_27a@A_27a))@(ty_2Epair_2Eprod@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@A_27a))))))@bool))@(lam@(arr@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@A_27a@(ty_2Epair_2Eprod@A_27a@(ty_2Epair_2Eprod@(arr@A_27a@(arr@A_27a@A_27a))@(ty_2Epair_2Eprod@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@A_27a))))))@bool)@(^ [V2_27ring_27:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(c_2Ebool_2E_21@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@A_27a@(ty_2Epair_2Eprod@A_27a@(ty_2Epair_2Eprod@(arr@A_27a@(arr@A_27a@A_27a))@(ty_2Epair_2Eprod@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@A_27a)))))))@(lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@A_27a@(ty_2Epair_2Eprod@A_27a@(ty_2Epair_2Eprod@(arr@A_27a@(arr@A_27a@A_27a))@(ty_2Epair_2Eprod@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@A_27a))))))@(^ [V3a0_27:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(c_2Ebool_2E_3F@A_27a)@(lam@A_27a@(^ [V4a0:$i] : (ap@(c_2Ebool_2E_3F@A_27a)@(lam@A_27a@(^ [V5a1:$i] : (ap@(c_2Ebool_2E_3F@(arr@A_27a@(arr@A_27a@A_27a)))@(lam@(arr@A_27a@(arr@A_27a@A_27a))@(^ [V6a2:$i] : (ap@(c_2Ebool_2E_3F@(arr@A_27a@(arr@A_27a@A_27a)))@(lam@(arr@A_27a@(arr@A_27a@A_27a))@(^ [V7a3:$i] : (ap@(c_2Ebool_2E_3F@(arr@A_27a@A_27a))@(lam@(arr@A_27a@A_27a)@(^ [V8a4:$i] : (ap@(ap@(c_2Emin_2E_3D@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@A_27a@(ty_2Epair_2Eprod@A_27a@(ty_2Epair_2Eprod@(arr@A_27a@(arr@A_27a@A_27a))@(ty_2Epair_2Eprod@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@A_27a)))))))@V3a0_27)@(ap@(ap@(ap@(ap@(ap@(lam@A_27a@(^ [V9a0:$i] : (lam@A_27a@(^ [V10a1:$i] : (lam@(arr@A_27a@(arr@A_27a@A_27a))@(^ [V11a2:$i] : (lam@(arr@A_27a@(arr@A_27a@A_27a))@(^ [V12a3:$i] : (lam@(arr@A_27a@A_27a)@(^ [V13a4:$i] : (ap@(ap@(ap@(c_2Eind__type_2ECONSTR@(ty_2Epair_2Eprod@A_27a@(ty_2Epair_2Eprod@A_27a@(ty_2Epair_2Eprod@(arr@A_27a@(arr@A_27a@A_27a))@(ty_2Epair_2Eprod@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@A_27a))))))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@(ap@(c_2Epair_2E_2C@A_27a@(ty_2Epair_2Eprod@A_27a@(ty_2Epair_2Eprod@(arr@A_27a@(arr@A_27a@A_27a))@(ty_2Epair_2Eprod@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@A_27a)))))@V9a0)@(ap@(ap@(c_2Epair_2E_2C@A_27a@(ty_2Epair_2Eprod@(arr@A_27a@(arr@A_27a@A_27a))@(ty_2Epair_2Eprod@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@A_27a))))@V10a1)@(ap@(ap@(c_2Epair_2E_2C@(arr@A_27a@(arr@A_27a@A_27a))@(ty_2Epair_2Eprod@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@A_27a)))@V11a2)@(ap@(ap@(c_2Epair_2E_2C@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@A_27a))@V12a3)@V13a4)))))@(lam@ty_2Enum_2Enum@(^ [V14n:$i] : (c_2Eind__type_2EBOTTOM@(ty_2Epair_2Eprod@A_27a@(ty_2Epair_2Eprod@A_27a@(ty_2Epair_2Eprod@(arr@A_27a@(arr@A_27a@A_27a))@(ty_2Epair_2Eprod@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@A_27a)))))))))))))))))))@V4a0)@V5a1)@V6a2)@V7a3)@V8a4))))))))))))))))))@(ap@V2_27ring_27@V3a0_27))))))@(ap@V2_27ring_27@V1a0_27))))))))@V0rep)))))).
thf(ax_thm_2Ering_2Ering__case__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0a0:$i] : ((mem@V0a0@A_27a) => ( ! [V1a1:$i] : ((mem@V1a1@A_27a) => ( ! [V2a2:$i] : ((mem@V2a2@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V3a3:$i] : ((mem@V3a3@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V4a4:$i] : ((mem@V4a4@(arr@A_27a@A_27a)) => ( ! [V5f:$i] : ((mem@V5f@(arr@A_27a@(arr@A_27a@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@(arr@A_27a@A_27a)@A_27b)))))) => ((ap@(ap@(c_2Ering_2Ering__CASE@A_27a@A_27b)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V0a0)@V1a1)@V2a2)@V3a3)@V4a4))@V5f) = (ap@(ap@(ap@(ap@(ap@V5f@V0a0)@V1a1)@V2a2)@V3a3)@V4a4))))))))))))))))).
thf(ax_thm_2Ering_2Ering__size__def,axiom,( ! [A_27a:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1a0:$i] : ((mem@V1a0@A_27a) => ( ! [V2a1:$i] : ((mem@V2a1@A_27a) => ( ! [V3a2:$i] : ((mem@V3a2@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V4a3:$i] : ((mem@V4a3@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V5a4:$i] : ((mem@V5a4@(arr@A_27a@A_27a)) => ((surj__ty_2Enum_2Enum @ (ap@(ap@(c_2Ering_2Ering__size@A_27a)@V0f)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V1a0)@V2a1)@V3a2)@V4a3)@V5a4))) = (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@V0f@V1a0))@(ap@V0f@V2a1))))))))))))))))))).
thf(ax_thm_2Ering_2Ering__R0,axiom,( ! [A_27a:del]: ( ! [V0a:$i] : ((mem@V0a@A_27a) => ( ! [V1a0:$i] : ((mem@V1a0@A_27a) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V3f0:$i] : ((mem@V3f0@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V4f1:$i] : ((mem@V4f1@(arr@A_27a@A_27a)) => ((ap@(c_2Ering_2Ering__R0@A_27a)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V0a)@V1a0)@V2f)@V3f0)@V4f1)) = V0a))))))))))))).
thf(ax_thm_2Ering_2Ering__R1,axiom,( ! [A_27a:del]: ( ! [V0a:$i] : ((mem@V0a@A_27a) => ( ! [V1a0:$i] : ((mem@V1a0@A_27a) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V3f0:$i] : ((mem@V3f0@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V4f1:$i] : ((mem@V4f1@(arr@A_27a@A_27a)) => ((ap@(c_2Ering_2Ering__R1@A_27a)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V0a)@V1a0)@V2f)@V3f0)@V4f1)) = V1a0))))))))))))).
thf(ax_thm_2Ering_2Ering__RP,axiom,( ! [A_27a:del]: ( ! [V0a:$i] : ((mem@V0a@A_27a) => ( ! [V1a0:$i] : ((mem@V1a0@A_27a) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V3f0:$i] : ((mem@V3f0@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V4f1:$i] : ((mem@V4f1@(arr@A_27a@A_27a)) => ((ap@(c_2Ering_2Ering__RP@A_27a)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V0a)@V1a0)@V2f)@V3f0)@V4f1)) = V2f))))))))))))).
thf(ax_thm_2Ering_2Ering__RM,axiom,( ! [A_27a:del]: ( ! [V0a:$i] : ((mem@V0a@A_27a) => ( ! [V1a0:$i] : ((mem@V1a0@A_27a) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V3f0:$i] : ((mem@V3f0@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V4f1:$i] : ((mem@V4f1@(arr@A_27a@A_27a)) => ((ap@(c_2Ering_2Ering__RM@A_27a)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V0a)@V1a0)@V2f)@V3f0)@V4f1)) = V3f0))))))))))))).
thf(ax_thm_2Ering_2Ering__RN,axiom,( ! [A_27a:del]: ( ! [V0a:$i] : ((mem@V0a@A_27a) => ( ! [V1a0:$i] : ((mem@V1a0@A_27a) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V3f0:$i] : ((mem@V3f0@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V4f1:$i] : ((mem@V4f1@(arr@A_27a@A_27a)) => ((ap@(c_2Ering_2Ering__RN@A_27a)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V0a)@V1a0)@V2f)@V3f0)@V4f1)) = V4f1))))))))))))).
thf(conj_thm_2Ering_2Ering__accessors,lemma,( ! [A_27a:del]: (( ! [V0a:$i] : ((mem@V0a@A_27a) => ( ! [V1a0:$i] : ((mem@V1a0@A_27a) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V3f0:$i] : ((mem@V3f0@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V4f1:$i] : ((mem@V4f1@(arr@A_27a@A_27a)) => ((ap@(c_2Ering_2Ering__R0@A_27a)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V0a)@V1a0)@V2f)@V3f0)@V4f1)) = V0a))))))))))) & (( ! [V5a:$i] : ((mem@V5a@A_27a) => ( ! [V6a0:$i] : ((mem@V6a0@A_27a) => ( ! [V7f:$i] : ((mem@V7f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V8f0:$i] : ((mem@V8f0@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V9f1:$i] : ((mem@V9f1@(arr@A_27a@A_27a)) => ((ap@(c_2Ering_2Ering__R1@A_27a)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V5a)@V6a0)@V7f)@V8f0)@V9f1)) = V6a0))))))))))) & (( ! [V10a:$i] : ((mem@V10a@A_27a) => ( ! [V11a0:$i] : ((mem@V11a0@A_27a) => ( ! [V12f:$i] : ((mem@V12f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V13f0:$i] : ((mem@V13f0@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V14f1:$i] : ((mem@V14f1@(arr@A_27a@A_27a)) => ((ap@(c_2Ering_2Ering__RP@A_27a)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V10a)@V11a0)@V12f)@V13f0)@V14f1)) = V12f))))))))))) & (( ! [V15a:$i] : ((mem@V15a@A_27a) => ( ! [V16a0:$i] : ((mem@V16a0@A_27a) => ( ! [V17f:$i] : ((mem@V17f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V18f0:$i] : ((mem@V18f0@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V19f1:$i] : ((mem@V19f1@(arr@A_27a@A_27a)) => ((ap@(c_2Ering_2Ering__RM@A_27a)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V15a)@V16a0)@V17f)@V18f0)@V19f1)) = V18f0))))))))))) & ( ! [V20a:$i] : ((mem@V20a@A_27a) => ( ! [V21a0:$i] : ((mem@V21a0@A_27a) => ( ! [V22f:$i] : ((mem@V22f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V23f0:$i] : ((mem@V23f0@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V24f1:$i] : ((mem@V24f1@(arr@A_27a@A_27a)) => ((ap@(c_2Ering_2Ering__RN@A_27a)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V20a)@V21a0)@V22f)@V23f0)@V24f1)) = V24f1))))))))))))))))).
thf(ax_thm_2Ering_2Ering__R0__fupd,axiom,( ! [A_27a:del]: ( ! [V0f2:$i] : ((mem@V0f2@(arr@A_27a@A_27a)) => ( ! [V1a:$i] : ((mem@V1a@A_27a) => ( ! [V2a0:$i] : ((mem@V2a0@A_27a) => ( ! [V3f:$i] : ((mem@V3f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V4f0:$i] : ((mem@V4f0@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V5f1:$i] : ((mem@V5f1@(arr@A_27a@A_27a)) => ((ap@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V0f2)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V1a)@V2a0)@V3f)@V4f0)@V5f1)) = (ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@(ap@V0f2@V1a))@V2a0)@V3f)@V4f0)@V5f1)))))))))))))))).
thf(ax_thm_2Ering_2Ering__R1__fupd,axiom,( ! [A_27a:del]: ( ! [V0f2:$i] : ((mem@V0f2@(arr@A_27a@A_27a)) => ( ! [V1a:$i] : ((mem@V1a@A_27a) => ( ! [V2a0:$i] : ((mem@V2a0@A_27a) => ( ! [V3f:$i] : ((mem@V3f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V4f0:$i] : ((mem@V4f0@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V5f1:$i] : ((mem@V5f1@(arr@A_27a@A_27a)) => ((ap@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V0f2)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V1a)@V2a0)@V3f)@V4f0)@V5f1)) = (ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V1a)@(ap@V0f2@V2a0))@V3f)@V4f0)@V5f1)))))))))))))))).
thf(ax_thm_2Ering_2Ering__RP__fupd,axiom,( ! [A_27a:del]: ( ! [V0f2:$i] : ((mem@V0f2@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ( ! [V1a:$i] : ((mem@V1a@A_27a) => ( ! [V2a0:$i] : ((mem@V2a0@A_27a) => ( ! [V3f:$i] : ((mem@V3f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V4f0:$i] : ((mem@V4f0@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V5f1:$i] : ((mem@V5f1@(arr@A_27a@A_27a)) => ((ap@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V0f2)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V1a)@V2a0)@V3f)@V4f0)@V5f1)) = (ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V1a)@V2a0)@(ap@V0f2@V3f))@V4f0)@V5f1)))))))))))))))).
thf(ax_thm_2Ering_2Ering__RM__fupd,axiom,( ! [A_27a:del]: ( ! [V0f2:$i] : ((mem@V0f2@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ( ! [V1a:$i] : ((mem@V1a@A_27a) => ( ! [V2a0:$i] : ((mem@V2a0@A_27a) => ( ! [V3f:$i] : ((mem@V3f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V4f0:$i] : ((mem@V4f0@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V5f1:$i] : ((mem@V5f1@(arr@A_27a@A_27a)) => ((ap@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V0f2)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V1a)@V2a0)@V3f)@V4f0)@V5f1)) = (ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V1a)@V2a0)@V3f)@(ap@V0f2@V4f0))@V5f1)))))))))))))))).
thf(ax_thm_2Ering_2Ering__RN__fupd,axiom,( ! [A_27a:del]: ( ! [V0f2:$i] : ((mem@V0f2@(arr@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))) => ( ! [V1a:$i] : ((mem@V1a@A_27a) => ( ! [V2a0:$i] : ((mem@V2a0@A_27a) => ( ! [V3f:$i] : ((mem@V3f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V4f0:$i] : ((mem@V4f0@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V5f1:$i] : ((mem@V5f1@(arr@A_27a@A_27a)) => ((ap@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V0f2)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V1a)@V2a0)@V3f)@V4f0)@V5f1)) = (ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V1a)@V2a0)@V3f)@V4f0)@(ap@V0f2@V5f1))))))))))))))))).
thf(conj_thm_2Ering_2Ering__fn__updates,lemma,( ! [A_27a:del]: (( ! [V0f2:$i] : ((mem@V0f2@(arr@A_27a@A_27a)) => ( ! [V1a:$i] : ((mem@V1a@A_27a) => ( ! [V2a0:$i] : ((mem@V2a0@A_27a) => ( ! [V3f:$i] : ((mem@V3f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V4f0:$i] : ((mem@V4f0@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V5f1:$i] : ((mem@V5f1@(arr@A_27a@A_27a)) => ((ap@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V0f2)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V1a)@V2a0)@V3f)@V4f0)@V5f1)) = (ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@(ap@V0f2@V1a))@V2a0)@V3f)@V4f0)@V5f1)))))))))))))) & (( ! [V6f2:$i] : ((mem@V6f2@(arr@A_27a@A_27a)) => ( ! [V7a:$i] : ((mem@V7a@A_27a) => ( ! [V8a0:$i] : ((mem@V8a0@A_27a) => ( ! [V9f:$i] : ((mem@V9f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V10f0:$i] : ((mem@V10f0@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V11f1:$i] : ((mem@V11f1@(arr@A_27a@A_27a)) => ((ap@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V6f2)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V7a)@V8a0)@V9f)@V10f0)@V11f1)) = (ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V7a)@(ap@V6f2@V8a0))@V9f)@V10f0)@V11f1)))))))))))))) & (( ! [V12f2:$i] : ((mem@V12f2@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ( ! [V13a:$i] : ((mem@V13a@A_27a) => ( ! [V14a0:$i] : ((mem@V14a0@A_27a) => ( ! [V15f:$i] : ((mem@V15f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V16f0:$i] : ((mem@V16f0@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V17f1:$i] : ((mem@V17f1@(arr@A_27a@A_27a)) => ((ap@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V12f2)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V13a)@V14a0)@V15f)@V16f0)@V17f1)) = (ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V13a)@V14a0)@(ap@V12f2@V15f))@V16f0)@V17f1)))))))))))))) & (( ! [V18f2:$i] : ((mem@V18f2@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ( ! [V19a:$i] : ((mem@V19a@A_27a) => ( ! [V20a0:$i] : ((mem@V20a0@A_27a) => ( ! [V21f:$i] : ((mem@V21f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V22f0:$i] : ((mem@V22f0@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V23f1:$i] : ((mem@V23f1@(arr@A_27a@A_27a)) => ((ap@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V18f2)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V19a)@V20a0)@V21f)@V22f0)@V23f1)) = (ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V19a)@V20a0)@V21f)@(ap@V18f2@V22f0))@V23f1)))))))))))))) & ( ! [V24f2:$i] : ((mem@V24f2@(arr@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))) => ( ! [V25a:$i] : ((mem@V25a@A_27a) => ( ! [V26a0:$i] : ((mem@V26a0@A_27a) => ( ! [V27f:$i] : ((mem@V27f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V28f0:$i] : ((mem@V28f0@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V29f1:$i] : ((mem@V29f1@(arr@A_27a@A_27a)) => ((ap@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V24f2)@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V25a)@V26a0)@V27f)@V28f0)@V29f1)) = (ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V25a)@V26a0)@V27f)@V28f0)@(ap@V24f2@V29f1))))))))))))))))))))).
thf(conj_thm_2Ering_2Ering__accfupds,lemma,( ! [A_27a:del]: (( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27a)) => ((ap@(c_2Ering_2Ering__R0@A_27a)@(ap@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V1f)@V0r)) = (ap@(c_2Ering_2Ering__R0@A_27a)@V0r)))))) & (( ! [V2r:$i] : ((mem@V2r@(ty_2Ering_2Ering@A_27a)) => ( ! [V3f:$i] : ((mem@V3f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(c_2Ering_2Ering__R0@A_27a)@(ap@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V3f)@V2r)) = (ap@(c_2Ering_2Ering__R0@A_27a)@V2r)))))) & (( ! [V4r:$i] : ((mem@V4r@(ty_2Ering_2Ering@A_27a)) => ( ! [V5f:$i] : ((mem@V5f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(c_2Ering_2Ering__R0@A_27a)@(ap@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V5f)@V4r)) = (ap@(c_2Ering_2Ering__R0@A_27a)@V4r)))))) & (( ! [V6r:$i] : ((mem@V6r@(ty_2Ering_2Ering@A_27a)) => ( ! [V7f:$i] : ((mem@V7f@(arr@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))) => ((ap@(c_2Ering_2Ering__R0@A_27a)@(ap@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V7f)@V6r)) = (ap@(c_2Ering_2Ering__R0@A_27a)@V6r)))))) & (( ! [V8r:$i] : ((mem@V8r@(ty_2Ering_2Ering@A_27a)) => ( ! [V9f:$i] : ((mem@V9f@(arr@A_27a@A_27a)) => ((ap@(c_2Ering_2Ering__R1@A_27a)@(ap@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V9f)@V8r)) = (ap@(c_2Ering_2Ering__R1@A_27a)@V8r)))))) & (( ! [V10r:$i] : ((mem@V10r@(ty_2Ering_2Ering@A_27a)) => ( ! [V11f:$i] : ((mem@V11f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(c_2Ering_2Ering__R1@A_27a)@(ap@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V11f)@V10r)) = (ap@(c_2Ering_2Ering__R1@A_27a)@V10r)))))) & (( ! [V12r:$i] : ((mem@V12r@(ty_2Ering_2Ering@A_27a)) => ( ! [V13f:$i] : ((mem@V13f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(c_2Ering_2Ering__R1@A_27a)@(ap@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V13f)@V12r)) = (ap@(c_2Ering_2Ering__R1@A_27a)@V12r)))))) & (( ! [V14r:$i] : ((mem@V14r@(ty_2Ering_2Ering@A_27a)) => ( ! [V15f:$i] : ((mem@V15f@(arr@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))) => ((ap@(c_2Ering_2Ering__R1@A_27a)@(ap@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V15f)@V14r)) = (ap@(c_2Ering_2Ering__R1@A_27a)@V14r)))))) & (( ! [V16r:$i] : ((mem@V16r@(ty_2Ering_2Ering@A_27a)) => ( ! [V17f:$i] : ((mem@V17f@(arr@A_27a@A_27a)) => ((ap@(c_2Ering_2Ering__RP@A_27a)@(ap@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V17f)@V16r)) = (ap@(c_2Ering_2Ering__RP@A_27a)@V16r)))))) & (( ! [V18r:$i] : ((mem@V18r@(ty_2Ering_2Ering@A_27a)) => ( ! [V19f:$i] : ((mem@V19f@(arr@A_27a@A_27a)) => ((ap@(c_2Ering_2Ering__RP@A_27a)@(ap@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V19f)@V18r)) = (ap@(c_2Ering_2Ering__RP@A_27a)@V18r)))))) & (( ! [V20r:$i] : ((mem@V20r@(ty_2Ering_2Ering@A_27a)) => ( ! [V21f:$i] : ((mem@V21f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(c_2Ering_2Ering__RP@A_27a)@(ap@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V21f)@V20r)) = (ap@(c_2Ering_2Ering__RP@A_27a)@V20r)))))) & (( ! [V22r:$i] : ((mem@V22r@(ty_2Ering_2Ering@A_27a)) => ( ! [V23f:$i] : ((mem@V23f@(arr@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))) => ((ap@(c_2Ering_2Ering__RP@A_27a)@(ap@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V23f)@V22r)) = (ap@(c_2Ering_2Ering__RP@A_27a)@V22r)))))) & (( ! [V24r:$i] : ((mem@V24r@(ty_2Ering_2Ering@A_27a)) => ( ! [V25f:$i] : ((mem@V25f@(arr@A_27a@A_27a)) => ((ap@(c_2Ering_2Ering__RM@A_27a)@(ap@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V25f)@V24r)) = (ap@(c_2Ering_2Ering__RM@A_27a)@V24r)))))) & (( ! [V26r:$i] : ((mem@V26r@(ty_2Ering_2Ering@A_27a)) => ( ! [V27f:$i] : ((mem@V27f@(arr@A_27a@A_27a)) => ((ap@(c_2Ering_2Ering__RM@A_27a)@(ap@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V27f)@V26r)) = (ap@(c_2Ering_2Ering__RM@A_27a)@V26r)))))) & (( ! [V28r:$i] : ((mem@V28r@(ty_2Ering_2Ering@A_27a)) => ( ! [V29f:$i] : ((mem@V29f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(c_2Ering_2Ering__RM@A_27a)@(ap@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V29f)@V28r)) = (ap@(c_2Ering_2Ering__RM@A_27a)@V28r)))))) & (( ! [V30r:$i] : ((mem@V30r@(ty_2Ering_2Ering@A_27a)) => ( ! [V31f:$i] : ((mem@V31f@(arr@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))) => ((ap@(c_2Ering_2Ering__RM@A_27a)@(ap@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V31f)@V30r)) = (ap@(c_2Ering_2Ering__RM@A_27a)@V30r)))))) & (( ! [V32r:$i] : ((mem@V32r@(ty_2Ering_2Ering@A_27a)) => ( ! [V33f:$i] : ((mem@V33f@(arr@A_27a@A_27a)) => ((ap@(c_2Ering_2Ering__RN@A_27a)@(ap@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V33f)@V32r)) = (ap@(c_2Ering_2Ering__RN@A_27a)@V32r)))))) & (( ! [V34r:$i] : ((mem@V34r@(ty_2Ering_2Ering@A_27a)) => ( ! [V35f:$i] : ((mem@V35f@(arr@A_27a@A_27a)) => ((ap@(c_2Ering_2Ering__RN@A_27a)@(ap@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V35f)@V34r)) = (ap@(c_2Ering_2Ering__RN@A_27a)@V34r)))))) & (( ! [V36r:$i] : ((mem@V36r@(ty_2Ering_2Ering@A_27a)) => ( ! [V37f:$i] : ((mem@V37f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(c_2Ering_2Ering__RN@A_27a)@(ap@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V37f)@V36r)) = (ap@(c_2Ering_2Ering__RN@A_27a)@V36r)))))) & (( ! [V38r:$i] : ((mem@V38r@(ty_2Ering_2Ering@A_27a)) => ( ! [V39f:$i] : ((mem@V39f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(c_2Ering_2Ering__RN@A_27a)@(ap@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V39f)@V38r)) = (ap@(c_2Ering_2Ering__RN@A_27a)@V38r)))))) & (( ! [V40r:$i] : ((mem@V40r@(ty_2Ering_2Ering@A_27a)) => ( ! [V41f:$i] : ((mem@V41f@(arr@A_27a@A_27a)) => ((ap@(c_2Ering_2Ering__R0@A_27a)@(ap@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V41f)@V40r)) = (ap@V41f@(ap@(c_2Ering_2Ering__R0@A_27a)@V40r))))))) & (( ! [V42r:$i] : ((mem@V42r@(ty_2Ering_2Ering@A_27a)) => ( ! [V43f:$i] : ((mem@V43f@(arr@A_27a@A_27a)) => ((ap@(c_2Ering_2Ering__R1@A_27a)@(ap@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V43f)@V42r)) = (ap@V43f@(ap@(c_2Ering_2Ering__R1@A_27a)@V42r))))))) & (( ! [V44r:$i] : ((mem@V44r@(ty_2Ering_2Ering@A_27a)) => ( ! [V45f:$i] : ((mem@V45f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(c_2Ering_2Ering__RP@A_27a)@(ap@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V45f)@V44r)) = (ap@V45f@(ap@(c_2Ering_2Ering__RP@A_27a)@V44r))))))) & (( ! [V46r:$i] : ((mem@V46r@(ty_2Ering_2Ering@A_27a)) => ( ! [V47f:$i] : ((mem@V47f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(c_2Ering_2Ering__RM@A_27a)@(ap@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V47f)@V46r)) = (ap@V47f@(ap@(c_2Ering_2Ering__RM@A_27a)@V46r))))))) & ( ! [V48r:$i] : ((mem@V48r@(ty_2Ering_2Ering@A_27a)) => ( ! [V49f:$i] : ((mem@V49f@(arr@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))) => ((ap@(c_2Ering_2Ering__RN@A_27a)@(ap@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V49f)@V48r)) = (ap@V49f@(ap@(c_2Ering_2Ering__RN@A_27a)@V48r))))))))))))))))))))))))))))))))).
thf(conj_thm_2Ering_2Ering__fupdfupds,lemma,( ! [A_27a:del]: (( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ( ! [V1g:$i] : ((mem@V1g@(arr@A_27a@A_27a)) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27a)) => ((ap@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V2f)@(ap@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V1g)@V0r)) = (ap@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@(ap@(ap@(c_2Ecombin_2Eo@A_27a@A_27a@A_27a)@V2f)@V1g))@V0r)))))))) & (( ! [V3r:$i] : ((mem@V3r@(ty_2Ering_2Ering@A_27a)) => ( ! [V4g:$i] : ((mem@V4g@(arr@A_27a@A_27a)) => ( ! [V5f:$i] : ((mem@V5f@(arr@A_27a@A_27a)) => ((ap@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V5f)@(ap@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V4g)@V3r)) = (ap@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@(ap@(ap@(c_2Ecombin_2Eo@A_27a@A_27a@A_27a)@V5f)@V4g))@V3r)))))))) & (( ! [V6r:$i] : ((mem@V6r@(ty_2Ering_2Ering@A_27a)) => ( ! [V7g:$i] : ((mem@V7g@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ( ! [V8f:$i] : ((mem@V8f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V8f)@(ap@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V7g)@V6r)) = (ap@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@(ap@(ap@(c_2Ecombin_2Eo@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))@V8f)@V7g))@V6r)))))))) & (( ! [V9r:$i] : ((mem@V9r@(ty_2Ering_2Ering@A_27a)) => ( ! [V10g:$i] : ((mem@V10g@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ( ! [V11f:$i] : ((mem@V11f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V11f)@(ap@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V10g)@V9r)) = (ap@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@(ap@(ap@(c_2Ecombin_2Eo@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))@V11f)@V10g))@V9r)))))))) & ( ! [V12r:$i] : ((mem@V12r@(ty_2Ering_2Ering@A_27a)) => ( ! [V13g:$i] : ((mem@V13g@(arr@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))) => ( ! [V14f:$i] : ((mem@V14f@(arr@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))) => ((ap@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V14f)@(ap@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V13g)@V12r)) = (ap@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@(ap@(ap@(c_2Ecombin_2Eo@(arr@A_27a@A_27a)@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))@V14f)@V13g))@V12r)))))))))))))).
thf(conj_thm_2Ering_2Ering__fupdfupds__comp,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ((( ! [V0g:$i] : ((mem@V0g@(arr@A_27a@A_27a)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27a)) => ((ap@(ap@(c_2Ecombin_2Eo@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V1f))@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V0g)) = (ap@(c_2Ering_2Ering__R0__fupd@A_27a)@(ap@(ap@(c_2Ecombin_2Eo@A_27a@A_27a@A_27a)@V1f)@V0g))))))) & ( ! [V2h:$i] : ((mem@V2h@(arr@A_27b@(ty_2Ering_2Ering@A_27a))) => ( ! [V3g:$i] : ((mem@V3g@(arr@A_27a@A_27a)) => ( ! [V4f:$i] : ((mem@V4f@(arr@A_27a@A_27a)) => ((ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V4f))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V3g))@V2h)) = (ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@(ap@(ap@(c_2Ecombin_2Eo@A_27a@A_27a@A_27a)@V4f)@V3g)))@V2h))))))))) & ((( ! [V5g:$i] : ((mem@V5g@(arr@A_27a@A_27a)) => ( ! [V6f:$i] : ((mem@V6f@(arr@A_27a@A_27a)) => ((ap@(ap@(c_2Ecombin_2Eo@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V6f))@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V5g)) = (ap@(c_2Ering_2Ering__R1__fupd@A_27a)@(ap@(ap@(c_2Ecombin_2Eo@A_27a@A_27a@A_27a)@V6f)@V5g))))))) & ( ! [V7h:$i] : ((mem@V7h@(arr@A_27b@(ty_2Ering_2Ering@A_27a))) => ( ! [V8g:$i] : ((mem@V8g@(arr@A_27a@A_27a)) => ( ! [V9f:$i] : ((mem@V9f@(arr@A_27a@A_27a)) => ((ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V9f))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V8g))@V7h)) = (ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@(ap@(ap@(c_2Ecombin_2Eo@A_27a@A_27a@A_27a)@V9f)@V8g)))@V7h))))))))) & ((( ! [V10g:$i] : ((mem@V10g@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ( ! [V11f:$i] : ((mem@V11f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(ap@(c_2Ecombin_2Eo@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V11f))@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V10g)) = (ap@(c_2Ering_2Ering__RP__fupd@A_27a)@(ap@(ap@(c_2Ecombin_2Eo@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))@V11f)@V10g))))))) & ( ! [V12h:$i] : ((mem@V12h@(arr@A_27b@(ty_2Ering_2Ering@A_27a))) => ( ! [V13g:$i] : ((mem@V13g@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ( ! [V14f:$i] : ((mem@V14f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V14f))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V13g))@V12h)) = (ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@(ap@(ap@(c_2Ecombin_2Eo@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))@V14f)@V13g)))@V12h))))))))) & ((( ! [V15g:$i] : ((mem@V15g@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ( ! [V16f:$i] : ((mem@V16f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(ap@(c_2Ecombin_2Eo@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V16f))@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V15g)) = (ap@(c_2Ering_2Ering__RM__fupd@A_27a)@(ap@(ap@(c_2Ecombin_2Eo@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))@V16f)@V15g))))))) & ( ! [V17h:$i] : ((mem@V17h@(arr@A_27b@(ty_2Ering_2Ering@A_27a))) => ( ! [V18g:$i] : ((mem@V18g@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ( ! [V19f:$i] : ((mem@V19f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V19f))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V18g))@V17h)) = (ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@(ap@(ap@(c_2Ecombin_2Eo@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))@V19f)@V18g)))@V17h))))))))) & (( ! [V20g:$i] : ((mem@V20g@(arr@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))) => ( ! [V21f:$i] : ((mem@V21f@(arr@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))) => ((ap@(ap@(c_2Ecombin_2Eo@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V21f))@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V20g)) = (ap@(c_2Ering_2Ering__RN__fupd@A_27a)@(ap@(ap@(c_2Ecombin_2Eo@(arr@A_27a@A_27a)@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))@V21f)@V20g))))))) & ( ! [V22h:$i] : ((mem@V22h@(arr@A_27b@(ty_2Ering_2Ering@A_27a))) => ( ! [V23g:$i] : ((mem@V23g@(arr@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))) => ( ! [V24f:$i] : ((mem@V24f@(arr@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))) => ((ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V24f))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V23g))@V22h)) = (ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@(ap@(ap@(c_2Ecombin_2Eo@(arr@A_27a@A_27a)@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))@V24f)@V23g)))@V22h)))))))))))))))).
thf(conj_thm_2Ering_2Ering__fupdcanon,lemma,( ! [A_27a:del]: (( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ( ! [V1g:$i] : ((mem@V1g@(arr@A_27a@A_27a)) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27a)) => ((ap@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V2f)@(ap@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V1g)@V0r)) = (ap@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V1g)@(ap@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V2f)@V0r))))))))) & (( ! [V3r:$i] : ((mem@V3r@(ty_2Ering_2Ering@A_27a)) => ( ! [V4g:$i] : ((mem@V4g@(arr@A_27a@A_27a)) => ( ! [V5f:$i] : ((mem@V5f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V5f)@(ap@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V4g)@V3r)) = (ap@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V4g)@(ap@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V5f)@V3r))))))))) & (( ! [V6r:$i] : ((mem@V6r@(ty_2Ering_2Ering@A_27a)) => ( ! [V7g:$i] : ((mem@V7g@(arr@A_27a@A_27a)) => ( ! [V8f:$i] : ((mem@V8f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V8f)@(ap@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V7g)@V6r)) = (ap@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V7g)@(ap@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V8f)@V6r))))))))) & (( ! [V9r:$i] : ((mem@V9r@(ty_2Ering_2Ering@A_27a)) => ( ! [V10g:$i] : ((mem@V10g@(arr@A_27a@A_27a)) => ( ! [V11f:$i] : ((mem@V11f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V11f)@(ap@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V10g)@V9r)) = (ap@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V10g)@(ap@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V11f)@V9r))))))))) & (( ! [V12r:$i] : ((mem@V12r@(ty_2Ering_2Ering@A_27a)) => ( ! [V13g:$i] : ((mem@V13g@(arr@A_27a@A_27a)) => ( ! [V14f:$i] : ((mem@V14f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V14f)@(ap@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V13g)@V12r)) = (ap@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V13g)@(ap@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V14f)@V12r))))))))) & (( ! [V15r:$i] : ((mem@V15r@(ty_2Ering_2Ering@A_27a)) => ( ! [V16g:$i] : ((mem@V16g@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ( ! [V17f:$i] : ((mem@V17f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V17f)@(ap@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V16g)@V15r)) = (ap@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V16g)@(ap@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V17f)@V15r))))))))) & (( ! [V18r:$i] : ((mem@V18r@(ty_2Ering_2Ering@A_27a)) => ( ! [V19g:$i] : ((mem@V19g@(arr@A_27a@A_27a)) => ( ! [V20f:$i] : ((mem@V20f@(arr@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))) => ((ap@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V20f)@(ap@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V19g)@V18r)) = (ap@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V19g)@(ap@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V20f)@V18r))))))))) & (( ! [V21r:$i] : ((mem@V21r@(ty_2Ering_2Ering@A_27a)) => ( ! [V22g:$i] : ((mem@V22g@(arr@A_27a@A_27a)) => ( ! [V23f:$i] : ((mem@V23f@(arr@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))) => ((ap@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V23f)@(ap@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V22g)@V21r)) = (ap@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V22g)@(ap@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V23f)@V21r))))))))) & (( ! [V24r:$i] : ((mem@V24r@(ty_2Ering_2Ering@A_27a)) => ( ! [V25g:$i] : ((mem@V25g@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ( ! [V26f:$i] : ((mem@V26f@(arr@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))) => ((ap@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V26f)@(ap@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V25g)@V24r)) = (ap@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V25g)@(ap@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V26f)@V24r))))))))) & ( ! [V27r:$i] : ((mem@V27r@(ty_2Ering_2Ering@A_27a)) => ( ! [V28g:$i] : ((mem@V28g@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ( ! [V29f:$i] : ((mem@V29f@(arr@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))) => ((ap@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V29f)@(ap@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V28g)@V27r)) = (ap@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V28g)@(ap@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V29f)@V27r)))))))))))))))))))).
thf(conj_thm_2Ering_2Ering__fupdcanon__comp,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ((( ! [V0g:$i] : ((mem@V0g@(arr@A_27a@A_27a)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27a)) => ((ap@(ap@(c_2Ecombin_2Eo@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V1f))@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V0g)) = (ap@(ap@(c_2Ecombin_2Eo@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V0g))@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V1f))))))) & ( ! [V2h:$i] : ((mem@V2h@(arr@A_27b@(ty_2Ering_2Ering@A_27a))) => ( ! [V3g:$i] : ((mem@V3g@(arr@A_27a@A_27a)) => ( ! [V4f:$i] : ((mem@V4f@(arr@A_27a@A_27a)) => ((ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V4f))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V3g))@V2h)) = (ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V3g))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V4f))@V2h)))))))))) & ((( ! [V5g:$i] : ((mem@V5g@(arr@A_27a@A_27a)) => ( ! [V6f:$i] : ((mem@V6f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(ap@(c_2Ecombin_2Eo@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V6f))@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V5g)) = (ap@(ap@(c_2Ecombin_2Eo@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V5g))@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V6f))))))) & ( ! [V7h:$i] : ((mem@V7h@(arr@A_27b@(ty_2Ering_2Ering@A_27a))) => ( ! [V8g:$i] : ((mem@V8g@(arr@A_27a@A_27a)) => ( ! [V9f:$i] : ((mem@V9f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V9f))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V8g))@V7h)) = (ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V8g))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V9f))@V7h)))))))))) & ((( ! [V10g:$i] : ((mem@V10g@(arr@A_27a@A_27a)) => ( ! [V11f:$i] : ((mem@V11f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(ap@(c_2Ecombin_2Eo@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V11f))@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V10g)) = (ap@(ap@(c_2Ecombin_2Eo@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V10g))@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V11f))))))) & ( ! [V12h:$i] : ((mem@V12h@(arr@A_27b@(ty_2Ering_2Ering@A_27a))) => ( ! [V13g:$i] : ((mem@V13g@(arr@A_27a@A_27a)) => ( ! [V14f:$i] : ((mem@V14f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V14f))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V13g))@V12h)) = (ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V13g))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V14f))@V12h)))))))))) & ((( ! [V15g:$i] : ((mem@V15g@(arr@A_27a@A_27a)) => ( ! [V16f:$i] : ((mem@V16f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(ap@(c_2Ecombin_2Eo@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V16f))@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V15g)) = (ap@(ap@(c_2Ecombin_2Eo@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V15g))@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V16f))))))) & ( ! [V17h:$i] : ((mem@V17h@(arr@A_27b@(ty_2Ering_2Ering@A_27a))) => ( ! [V18g:$i] : ((mem@V18g@(arr@A_27a@A_27a)) => ( ! [V19f:$i] : ((mem@V19f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V19f))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V18g))@V17h)) = (ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V18g))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V19f))@V17h)))))))))) & ((( ! [V20g:$i] : ((mem@V20g@(arr@A_27a@A_27a)) => ( ! [V21f:$i] : ((mem@V21f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(ap@(c_2Ecombin_2Eo@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V21f))@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V20g)) = (ap@(ap@(c_2Ecombin_2Eo@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V20g))@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V21f))))))) & ( ! [V22h:$i] : ((mem@V22h@(arr@A_27b@(ty_2Ering_2Ering@A_27a))) => ( ! [V23g:$i] : ((mem@V23g@(arr@A_27a@A_27a)) => ( ! [V24f:$i] : ((mem@V24f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V24f))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V23g))@V22h)) = (ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V23g))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V24f))@V22h)))))))))) & ((( ! [V25g:$i] : ((mem@V25g@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ( ! [V26f:$i] : ((mem@V26f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(ap@(c_2Ecombin_2Eo@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V26f))@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V25g)) = (ap@(ap@(c_2Ecombin_2Eo@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V25g))@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V26f))))))) & ( ! [V27h:$i] : ((mem@V27h@(arr@A_27b@(ty_2Ering_2Ering@A_27a))) => ( ! [V28g:$i] : ((mem@V28g@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ( ! [V29f:$i] : ((mem@V29f@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ((ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V29f))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V28g))@V27h)) = (ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V28g))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V29f))@V27h)))))))))) & ((( ! [V30g:$i] : ((mem@V30g@(arr@A_27a@A_27a)) => ( ! [V31f:$i] : ((mem@V31f@(arr@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))) => ((ap@(ap@(c_2Ecombin_2Eo@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V31f))@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V30g)) = (ap@(ap@(c_2Ecombin_2Eo@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V30g))@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V31f))))))) & ( ! [V32h:$i] : ((mem@V32h@(arr@A_27b@(ty_2Ering_2Ering@A_27a))) => ( ! [V33g:$i] : ((mem@V33g@(arr@A_27a@A_27a)) => ( ! [V34f:$i] : ((mem@V34f@(arr@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))) => ((ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V34f))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V33g))@V32h)) = (ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@V33g))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V34f))@V32h)))))))))) & ((( ! [V35g:$i] : ((mem@V35g@(arr@A_27a@A_27a)) => ( ! [V36f:$i] : ((mem@V36f@(arr@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))) => ((ap@(ap@(c_2Ecombin_2Eo@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V36f))@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V35g)) = (ap@(ap@(c_2Ecombin_2Eo@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V35g))@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V36f))))))) & ( ! [V37h:$i] : ((mem@V37h@(arr@A_27b@(ty_2Ering_2Ering@A_27a))) => ( ! [V38g:$i] : ((mem@V38g@(arr@A_27a@A_27a)) => ( ! [V39f:$i] : ((mem@V39f@(arr@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))) => ((ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V39f))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V38g))@V37h)) = (ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@V38g))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V39f))@V37h)))))))))) & ((( ! [V40g:$i] : ((mem@V40g@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ( ! [V41f:$i] : ((mem@V41f@(arr@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))) => ((ap@(ap@(c_2Ecombin_2Eo@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V41f))@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V40g)) = (ap@(ap@(c_2Ecombin_2Eo@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V40g))@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V41f))))))) & ( ! [V42h:$i] : ((mem@V42h@(arr@A_27b@(ty_2Ering_2Ering@A_27a))) => ( ! [V43g:$i] : ((mem@V43g@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ( ! [V44f:$i] : ((mem@V44f@(arr@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))) => ((ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V44f))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V43g))@V42h)) = (ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@V43g))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V44f))@V42h)))))))))) & (( ! [V45g:$i] : ((mem@V45g@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ( ! [V46f:$i] : ((mem@V46f@(arr@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))) => ((ap@(ap@(c_2Ecombin_2Eo@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V46f))@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V45g)) = (ap@(ap@(c_2Ecombin_2Eo@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V45g))@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V46f))))))) & ( ! [V47h:$i] : ((mem@V47h@(arr@A_27b@(ty_2Ering_2Ering@A_27a))) => ( ! [V48g:$i] : ((mem@V48g@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))) => ( ! [V49f:$i] : ((mem@V49f@(arr@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))) => ((ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V49f))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V48g))@V47h)) = (ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@V48g))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@(ty_2Ering_2Ering@A_27a)@(ty_2Ering_2Ering@A_27a))@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@V49f))@V47h)))))))))))))))))))))).
thf(conj_thm_2Ering_2Ering__component__equality,lemma,( ! [A_27a:del]: ( ! [V0r1:$i] : ((mem@V0r1@(ty_2Ering_2Ering@A_27a)) => ( ! [V1r2:$i] : ((mem@V1r2@(ty_2Ering_2Ering@A_27a)) => ((V0r1 = V1r2) <=> (((ap@(c_2Ering_2Ering__R0@A_27a)@V0r1) = (ap@(c_2Ering_2Ering__R0@A_27a)@V1r2)) & (((ap@(c_2Ering_2Ering__R1@A_27a)@V0r1) = (ap@(c_2Ering_2Ering__R1@A_27a)@V1r2)) & (((ap@(c_2Ering_2Ering__RP@A_27a)@V0r1) = (ap@(c_2Ering_2Ering__RP@A_27a)@V1r2)) & (((ap@(c_2Ering_2Ering__RM@A_27a)@V0r1) = (ap@(c_2Ering_2Ering__RM@A_27a)@V1r2)) & ((ap@(c_2Ering_2Ering__RN@A_27a)@V0r1) = (ap@(c_2Ering_2Ering__RN@A_27a)@V1r2))))))))))))).
thf(conj_thm_2Ering_2Ering__updates__eq__literal,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ( ! [V1a0:$i] : ((mem@V1a0@A_27a) => ( ! [V2a:$i] : ((mem@V2a@A_27a) => ( ! [V3f1:$i] : ((mem@V3f1@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V4f0:$i] : ((mem@V4f0@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V5f:$i] : ((mem@V5f@(arr@A_27a@A_27a)) => ((ap@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@(ap@(c_2Ecombin_2EK@A_27a@A_27a)@V1a0))@(ap@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@(ap@(c_2Ecombin_2EK@A_27a@A_27a)@V2a))@(ap@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@(ap@(c_2Ecombin_2EK@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))@V3f1))@(ap@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@(ap@(c_2Ecombin_2EK@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))@V4f0))@(ap@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@(ap@(c_2Ecombin_2EK@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))@V5f))@V0r))))) = (ap@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@(ap@(c_2Ecombin_2EK@A_27a@A_27a)@V1a0))@(ap@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@(ap@(c_2Ecombin_2EK@A_27a@A_27a)@V2a))@(ap@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@(ap@(c_2Ecombin_2EK@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))@V3f1))@(ap@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@(ap@(c_2Ecombin_2EK@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))@V4f0))@(ap@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@(ap@(c_2Ecombin_2EK@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))@V5f))@(c_2Ebool_2EARB@(ty_2Ering_2Ering@A_27a)))))))))))))))))))))).
thf(conj_thm_2Ering_2Ering__literal__nchotomy,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => (? [V1a0:$i] : ((mem@V1a0@A_27a) & (? [V2a:$i] : ((mem@V2a@A_27a) & (? [V3f1:$i] : ((mem@V3f1@(arr@A_27a@(arr@A_27a@A_27a))) & (? [V4f0:$i] : ((mem@V4f0@(arr@A_27a@(arr@A_27a@A_27a))) & (? [V5f:$i] : ((mem@V5f@(arr@A_27a@A_27a)) & (V0r = (ap@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@(ap@(c_2Ecombin_2EK@A_27a@A_27a)@V1a0))@(ap@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@(ap@(c_2Ecombin_2EK@A_27a@A_27a)@V2a))@(ap@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@(ap@(c_2Ecombin_2EK@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))@V3f1))@(ap@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@(ap@(c_2Ecombin_2EK@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))@V4f0))@(ap@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@(ap@(c_2Ecombin_2EK@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))@V5f))@(c_2Ebool_2EARB@(ty_2Ering_2Ering@A_27a)))))))))))))))))))))).
thf(conj_thm_2Ering_2EFORALL__ring,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Ering_2Ering@A_27a)@bool)) => (( ! [V1r:$i] : ((mem@V1r@(ty_2Ering_2Ering@A_27a)) => (p@(ap@V0P@V1r)))) <=> ( ! [V2a0:$i] : ((mem@V2a0@A_27a) => ( ! [V3a:$i] : ((mem@V3a@A_27a) => ( ! [V4f1:$i] : ((mem@V4f1@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V5f0:$i] : ((mem@V5f0@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V6f:$i] : ((mem@V6f@(arr@A_27a@A_27a)) => (p@(ap@V0P@(ap@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@(ap@(c_2Ecombin_2EK@A_27a@A_27a)@V2a0))@(ap@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@(ap@(c_2Ecombin_2EK@A_27a@A_27a)@V3a))@(ap@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@(ap@(c_2Ecombin_2EK@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))@V4f1))@(ap@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@(ap@(c_2Ecombin_2EK@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))@V5f0))@(ap@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@(ap@(c_2Ecombin_2EK@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))@V6f))@(c_2Ebool_2EARB@(ty_2Ering_2Ering@A_27a)))))))))))))))))))))))).
thf(conj_thm_2Ering_2EEXISTS__ring,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Ering_2Ering@A_27a)@bool)) => ((? [V1r:$i] : ((mem@V1r@(ty_2Ering_2Ering@A_27a)) & (p@(ap@V0P@V1r)))) <=> (? [V2a0:$i] : ((mem@V2a0@A_27a) & (? [V3a:$i] : ((mem@V3a@A_27a) & (? [V4f1:$i] : ((mem@V4f1@(arr@A_27a@(arr@A_27a@A_27a))) & (? [V5f0:$i] : ((mem@V5f0@(arr@A_27a@(arr@A_27a@A_27a))) & (? [V6f:$i] : ((mem@V6f@(arr@A_27a@A_27a)) & (p@(ap@V0P@(ap@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@(ap@(c_2Ecombin_2EK@A_27a@A_27a)@V2a0))@(ap@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@(ap@(c_2Ecombin_2EK@A_27a@A_27a)@V3a))@(ap@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@(ap@(c_2Ecombin_2EK@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))@V4f1))@(ap@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@(ap@(c_2Ecombin_2EK@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))@V5f0))@(ap@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@(ap@(c_2Ecombin_2EK@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))@V6f))@(c_2Ebool_2EARB@(ty_2Ering_2Ering@A_27a)))))))))))))))))))))))).
thf(conj_thm_2Ering_2Ering__literal__11,lemma,( ! [A_27a:del]: ( ! [V0a01:$i] : ((mem@V0a01@A_27a) => ( ! [V1a1:$i] : ((mem@V1a1@A_27a) => ( ! [V2f11:$i] : ((mem@V2f11@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V3f01:$i] : ((mem@V3f01@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V4f1:$i] : ((mem@V4f1@(arr@A_27a@A_27a)) => ( ! [V5a02:$i] : ((mem@V5a02@A_27a) => ( ! [V6a2:$i] : ((mem@V6a2@A_27a) => ( ! [V7f12:$i] : ((mem@V7f12@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V8f02:$i] : ((mem@V8f02@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V9f2:$i] : ((mem@V9f2@(arr@A_27a@A_27a)) => (((ap@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@(ap@(c_2Ecombin_2EK@A_27a@A_27a)@V0a01))@(ap@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@(ap@(c_2Ecombin_2EK@A_27a@A_27a)@V1a1))@(ap@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@(ap@(c_2Ecombin_2EK@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))@V2f11))@(ap@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@(ap@(c_2Ecombin_2EK@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))@V3f01))@(ap@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@(ap@(c_2Ecombin_2EK@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))@V4f1))@(c_2Ebool_2EARB@(ty_2Ering_2Ering@A_27a))))))) = (ap@(ap@(c_2Ering_2Ering__R0__fupd@A_27a)@(ap@(c_2Ecombin_2EK@A_27a@A_27a)@V5a02))@(ap@(ap@(c_2Ering_2Ering__R1__fupd@A_27a)@(ap@(c_2Ecombin_2EK@A_27a@A_27a)@V6a2))@(ap@(ap@(c_2Ering_2Ering__RP__fupd@A_27a)@(ap@(c_2Ecombin_2EK@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))@V7f12))@(ap@(ap@(c_2Ering_2Ering__RM__fupd@A_27a)@(ap@(c_2Ecombin_2EK@(arr@A_27a@(arr@A_27a@A_27a))@(arr@A_27a@(arr@A_27a@A_27a)))@V8f02))@(ap@(ap@(c_2Ering_2Ering__RN__fupd@A_27a)@(ap@(c_2Ecombin_2EK@(arr@A_27a@A_27a)@(arr@A_27a@A_27a))@V9f2))@(c_2Ebool_2EARB@(ty_2Ering_2Ering@A_27a)))))))) <=> ((V0a01 = V5a02) & ((V1a1 = V6a2) & ((V2f11 = V7f12) & ((V3f01 = V8f02) & (V4f1 = V9f2)))))))))))))))))))))))))))).
thf(conj_thm_2Ering_2Edatatype__ring,lemma,( ! [A_27a:del]: ( ! [V0record:$i] : ((mem@V0record@(arr@(ty_2Ering_2Ering@A_27a)@(arr@A_27a@(arr@A_27a@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@(arr@A_27a@A_27a)@bool))))))) => ( ! [V1ring:$i] : ((mem@V1ring@(ty_2Ering_2Ering@A_27a)) => ( ! [V2R0:$i] : ((mem@V2R0@A_27a) => ( ! [V3R1:$i] : ((mem@V3R1@A_27a) => ( ! [V4RP:$i] : ((mem@V4RP@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V5RM:$i] : ((mem@V5RM@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V6RN:$i] : ((mem@V6RN@(arr@A_27a@A_27a)) => (p@(ap@(c_2Ebool_2EDATATYPE@bool)@(ap@(ap@(ap@(ap@(ap@(ap@V0record@V1ring)@V2R0)@V3R1)@V4RP)@V5RM)@V6RN))))))))))))))))))).
thf(conj_thm_2Ering_2Ering__11,lemma,( ! [A_27a:del]: ( ! [V0a0:$i] : ((mem@V0a0@A_27a) => ( ! [V1a1:$i] : ((mem@V1a1@A_27a) => ( ! [V2a2:$i] : ((mem@V2a2@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V3a3:$i] : ((mem@V3a3@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V4a4:$i] : ((mem@V4a4@(arr@A_27a@A_27a)) => ( ! [V5a0_27:$i] : ((mem@V5a0_27@A_27a) => ( ! [V6a1_27:$i] : ((mem@V6a1_27@A_27a) => ( ! [V7a2_27:$i] : ((mem@V7a2_27@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V8a3_27:$i] : ((mem@V8a3_27@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V9a4_27:$i] : ((mem@V9a4_27@(arr@A_27a@A_27a)) => (((ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V0a0)@V1a1)@V2a2)@V3a3)@V4a4) = (ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V5a0_27)@V6a1_27)@V7a2_27)@V8a3_27)@V9a4_27)) <=> ((V0a0 = V5a0_27) & ((V1a1 = V6a1_27) & ((V2a2 = V7a2_27) & ((V3a3 = V8a3_27) & (V4a4 = V9a4_27)))))))))))))))))))))))))))).
thf(conj_thm_2Ering_2Ering__nchotomy,lemma,( ! [A_27a:del]: ( ! [V0rr:$i] : ((mem@V0rr@(ty_2Ering_2Ering@A_27a)) => (? [V1a:$i] : ((mem@V1a@A_27a) & (? [V2a0:$i] : ((mem@V2a0@A_27a) & (? [V3f:$i] : ((mem@V3f@(arr@A_27a@(arr@A_27a@A_27a))) & (? [V4f0:$i] : ((mem@V4f0@(arr@A_27a@(arr@A_27a@A_27a))) & (? [V5f1:$i] : ((mem@V5f1@(arr@A_27a@A_27a)) & (V0rr = (ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V1a)@V2a0)@V3f)@V4f0)@V5f1)))))))))))))))).
thf(conj_thm_2Ering_2Ering__Axiom,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27a@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@(arr@A_27a@A_27a)@A_27b)))))) => (? [V1fn:$i] : ((mem@V1fn@(arr@(ty_2Ering_2Ering@A_27a)@A_27b)) & ( ! [V2a0:$i] : ((mem@V2a0@A_27a) => ( ! [V3a1:$i] : ((mem@V3a1@A_27a) => ( ! [V4a2:$i] : ((mem@V4a2@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V5a3:$i] : ((mem@V5a3@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V6a4:$i] : ((mem@V6a4@(arr@A_27a@A_27a)) => ((ap@V1fn@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V2a0)@V3a1)@V4a2)@V5a3)@V6a4)) = (ap@(ap@(ap@(ap@(ap@V0f@V2a0)@V3a1)@V4a2)@V5a3)@V6a4))))))))))))))))))).
thf(conj_thm_2Ering_2Ering__induction,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Ering_2Ering@A_27a)@bool)) => (( ! [V1a:$i] : ((mem@V1a@A_27a) => ( ! [V2a0:$i] : ((mem@V2a0@A_27a) => ( ! [V3f:$i] : ((mem@V3f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V4f0:$i] : ((mem@V4f0@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V5f1:$i] : ((mem@V5f1@(arr@A_27a@A_27a)) => (p@(ap@V0P@(ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V1a)@V2a0)@V3f)@V4f0)@V5f1))))))))))))) => ( ! [V6r:$i] : ((mem@V6r@(ty_2Ering_2Ering@A_27a)) => (p@(ap@V0P@V6r))))))))).
thf(conj_thm_2Ering_2Ering__case__cong,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f_27:$i] : ((mem@V0f_27@(arr@A_27a@(arr@A_27a@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@(arr@A_27a@A_27a)@A_27b)))))) => ( ! [V1M:$i] : ((mem@V1M@(ty_2Ering_2Ering@A_27a)) => ( ! [V2M_27:$i] : ((mem@V2M_27@(ty_2Ering_2Ering@A_27a)) => ( ! [V3f:$i] : ((mem@V3f@(arr@A_27a@(arr@A_27a@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@(arr@A_27a@A_27a)@A_27b)))))) => (((V1M = V2M_27) & ( ! [V4a0:$i] : ((mem@V4a0@A_27a) => ( ! [V5a1:$i] : ((mem@V5a1@A_27a) => ( ! [V6a2:$i] : ((mem@V6a2@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V7a3:$i] : ((mem@V7a3@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V8a4:$i] : ((mem@V8a4@(arr@A_27a@A_27a)) => ((V2M_27 = (ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V4a0)@V5a1)@V6a2)@V7a3)@V8a4)) => ((ap@(ap@(ap@(ap@(ap@V3f@V4a0)@V5a1)@V6a2)@V7a3)@V8a4) = (ap@(ap@(ap@(ap@(ap@V0f_27@V4a0)@V5a1)@V6a2)@V7a3)@V8a4)))))))))))))) => ((ap@(ap@(c_2Ering_2Ering__CASE@A_27a@A_27b)@V1M)@V3f) = (ap@(ap@(c_2Ering_2Ering__CASE@A_27a@A_27b)@V2M_27)@V0f_27)))))))))))))).
thf(conj_thm_2Ering_2Ering__case__eq,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : ((mem@V0x@(ty_2Ering_2Ering@A_27a)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@(arr@A_27a@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@(arr@A_27a@A_27a)@A_27b)))))) => ( ! [V2v:$i] : ((mem@V2v@A_27b) => (((ap@(ap@(c_2Ering_2Ering__CASE@A_27a@A_27b)@V0x)@V1f) = V2v) <=> (? [V3a:$i] : ((mem@V3a@A_27a) & (? [V4a0:$i] : ((mem@V4a0@A_27a) & (? [V5f_27:$i] : ((mem@V5f_27@(arr@A_27a@(arr@A_27a@A_27a))) & (? [V6f0:$i] : ((mem@V6f0@(arr@A_27a@(arr@A_27a@A_27a))) & (? [V7f1:$i] : ((mem@V7f1@(arr@A_27a@A_27a)) & ((V0x = (ap@(ap@(ap@(ap@(ap@(c_2Ering_2Erecordtype_2Ering@A_27a)@V3a)@V4a0)@V5f_27)@V6f0)@V7f1)) & ((ap@(ap@(ap@(ap@(ap@V1f@V3a)@V4a0)@V5f_27)@V6f0)@V7f1) = V2v)))))))))))))))))))))).
thf(ax_thm_2Ering_2Eis__ring__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((p@(ap@(c_2Ering_2Eis__ring@A_27a)@V0r)) <=> (( ! [V1n:$i] : ((mem@V1n@A_27a) => ( ! [V2m:$i] : ((mem@V2m@A_27a) => ((ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@V1n)@V2m) = (ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@V2m)@V1n)))))) & (( ! [V3n:$i] : ((mem@V3n@A_27a) => ( ! [V4m:$i] : ((mem@V4m@A_27a) => ( ! [V5p:$i] : ((mem@V5p@A_27a) => ((ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@V3n)@(ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@V4m)@V5p)) = (ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@(ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@V3n)@V4m))@V5p)))))))) & (( ! [V6n:$i] : ((mem@V6n@A_27a) => ( ! [V7m:$i] : ((mem@V7m@A_27a) => ((ap@(ap@(ap@(c_2Ering_2Ering__RM@A_27a)@V0r)@V6n)@V7m) = (ap@(ap@(ap@(c_2Ering_2Ering__RM@A_27a)@V0r)@V7m)@V6n)))))) & (( ! [V8n:$i] : ((mem@V8n@A_27a) => ( ! [V9m:$i] : ((mem@V9m@A_27a) => ( ! [V10p:$i] : ((mem@V10p@A_27a) => ((ap@(ap@(ap@(c_2Ering_2Ering__RM@A_27a)@V0r)@V8n)@(ap@(ap@(ap@(c_2Ering_2Ering__RM@A_27a)@V0r)@V9m)@V10p)) = (ap@(ap@(ap@(c_2Ering_2Ering__RM@A_27a)@V0r)@(ap@(ap@(ap@(c_2Ering_2Ering__RM@A_27a)@V0r)@V8n)@V9m))@V10p)))))))) & (( ! [V11n:$i] : ((mem@V11n@A_27a) => ((ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@(ap@(c_2Ering_2Ering__R0@A_27a)@V0r))@V11n) = V11n))) & (( ! [V12n:$i] : ((mem@V12n@A_27a) => ((ap@(ap@(ap@(c_2Ering_2Ering__RM@A_27a)@V0r)@(ap@(c_2Ering_2Ering__R1@A_27a)@V0r))@V12n) = V12n))) & (( ! [V13n:$i] : ((mem@V13n@A_27a) => ((ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@V13n)@(ap@(ap@(c_2Ering_2Ering__RN@A_27a)@V0r)@V13n)) = (ap@(c_2Ering_2Ering__R0@A_27a)@V0r)))) & ( ! [V14n:$i] : ((mem@V14n@A_27a) => ( ! [V15m:$i] : ((mem@V15m@A_27a) => ( ! [V16p:$i] : ((mem@V16p@A_27a) => ((ap@(ap@(ap@(c_2Ering_2Ering__RM@A_27a)@V0r)@(ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@V14n)@V15m))@V16p) = (ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@(ap@(ap@(ap@(c_2Ering_2Ering__RM@A_27a)@V0r)@V14n)@V16p))@(ap@(ap@(ap@(c_2Ering_2Ering__RM@A_27a)@V0r)@V15m)@V16p))))))))))))))))))))).
thf(conj_thm_2Ering_2Eplus__sym,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((p@(ap@(c_2Ering_2Eis__ring@A_27a)@V0r)) => ( ! [V1n:$i] : ((mem@V1n@A_27a) => ( ! [V2m:$i] : ((mem@V2m@A_27a) => ((ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@V1n)@V2m) = (ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@V2m)@V1n))))))))))).
thf(conj_thm_2Ering_2Eplus__assoc,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((p@(ap@(c_2Ering_2Eis__ring@A_27a)@V0r)) => ( ! [V1n:$i] : ((mem@V1n@A_27a) => ( ! [V2m:$i] : ((mem@V2m@A_27a) => ( ! [V3p:$i] : ((mem@V3p@A_27a) => ((ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@V1n)@(ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@V2m)@V3p)) = (ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@(ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@V1n)@V2m))@V3p))))))))))))).
thf(conj_thm_2Ering_2Emult__sym,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((p@(ap@(c_2Ering_2Eis__ring@A_27a)@V0r)) => ( ! [V1n:$i] : ((mem@V1n@A_27a) => ( ! [V2m:$i] : ((mem@V2m@A_27a) => ((ap@(ap@(ap@(c_2Ering_2Ering__RM@A_27a)@V0r)@V1n)@V2m) = (ap@(ap@(ap@(c_2Ering_2Ering__RM@A_27a)@V0r)@V2m)@V1n))))))))))).
thf(conj_thm_2Ering_2Emult__assoc,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((p@(ap@(c_2Ering_2Eis__ring@A_27a)@V0r)) => ( ! [V1n:$i] : ((mem@V1n@A_27a) => ( ! [V2m:$i] : ((mem@V2m@A_27a) => ( ! [V3p:$i] : ((mem@V3p@A_27a) => ((ap@(ap@(ap@(c_2Ering_2Ering__RM@A_27a)@V0r)@V1n)@(ap@(ap@(ap@(c_2Ering_2Ering__RM@A_27a)@V0r)@V2m)@V3p)) = (ap@(ap@(ap@(c_2Ering_2Ering__RM@A_27a)@V0r)@(ap@(ap@(ap@(c_2Ering_2Ering__RM@A_27a)@V0r)@V1n)@V2m))@V3p))))))))))))).
thf(conj_thm_2Ering_2Eplus__zero__left,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((p@(ap@(c_2Ering_2Eis__ring@A_27a)@V0r)) => ( ! [V1n:$i] : ((mem@V1n@A_27a) => ((ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@(ap@(c_2Ering_2Ering__R0@A_27a)@V0r))@V1n) = V1n)))))))).
thf(conj_thm_2Ering_2Emult__one__left,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((p@(ap@(c_2Ering_2Eis__ring@A_27a)@V0r)) => ( ! [V1n:$i] : ((mem@V1n@A_27a) => ((ap@(ap@(ap@(c_2Ering_2Ering__RM@A_27a)@V0r)@(ap@(c_2Ering_2Ering__R1@A_27a)@V0r))@V1n) = V1n)))))))).
thf(conj_thm_2Ering_2Eopp__def,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((p@(ap@(c_2Ering_2Eis__ring@A_27a)@V0r)) => ( ! [V1n:$i] : ((mem@V1n@A_27a) => ((ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@V1n)@(ap@(ap@(c_2Ering_2Ering__RN@A_27a)@V0r)@V1n)) = (ap@(c_2Ering_2Ering__R0@A_27a)@V0r))))))))).
thf(conj_thm_2Ering_2Edistr__left,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((p@(ap@(c_2Ering_2Eis__ring@A_27a)@V0r)) => ( ! [V1n:$i] : ((mem@V1n@A_27a) => ( ! [V2m:$i] : ((mem@V2m@A_27a) => ( ! [V3p:$i] : ((mem@V3p@A_27a) => ((ap@(ap@(ap@(c_2Ering_2Ering__RM@A_27a)@V0r)@(ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@V1n)@V2m))@V3p) = (ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@(ap@(ap@(ap@(c_2Ering_2Ering__RM@A_27a)@V0r)@V1n)@V3p))@(ap@(ap@(ap@(c_2Ering_2Ering__RM@A_27a)@V0r)@V2m)@V3p)))))))))))))).
thf(conj_thm_2Ering_2Eplus__zero__right,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((p@(ap@(c_2Ering_2Eis__ring@A_27a)@V0r)) => ( ! [V1n:$i] : ((mem@V1n@A_27a) => ((ap@(ap@(ap@(c_2Ering_2Ering__RP@A_27a)@V0r)@V1n)@(ap@(c_2Ering_2Ering__R0@A_27a)@V0r)) = V1n)))))))).
thf(conj_thm_2Ering_2Emult__zero__left,conjecture,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(ty_2Ering_2Ering@A_27a)) => ((p@(ap@(c_2Ering_2Eis__ring@A_27a)@V0r)) => ( ! [V1n:$i] : ((mem@V1n@A_27a) => ((ap@(ap@(ap@(c_2Ering_2Ering__RM@A_27a)@V0r)@(ap@(c_2Ering_2Ering__R0@A_27a)@V0r))@V1n) = (ap@(c_2Ering_2Ering__R0@A_27a)@V0r))))))))).
