include('Axioms/ASCIInumbers^2.ax').
thf(tp_ty_2Efinite__map_2Efmap,type,( ty_2Efinite__map_2Efmap: del > del >del )).
thf(tp_c_2Efinite__map_2EDRESTRICT,type,(c_2Efinite__map_2EDRESTRICT:(del>(del>$i)))).
thf(mem_c_2Efinite__map_2EDRESTRICT,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27b)@(arr@(arr@A_27a@bool)@(ty_2Efinite__map_2Efmap@A_27a@A_27b))))))).
thf(tp_c_2Efinite__map_2EFAPPLY,type,(c_2Efinite__map_2EFAPPLY:(del>(del>$i)))).
thf(mem_c_2Efinite__map_2EFAPPLY,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27b)@(arr@A_27a@A_27b)))))).
thf(tp_c_2Efinite__map_2EFCARD,type,(c_2Efinite__map_2EFCARD:(del>(del>$i)))).
thf(mem_c_2Efinite__map_2EFCARD,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Efinite__map_2EFCARD@A_27a@A_27b)@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27b)@ty_2Enum_2Enum))))).
thf(tp_c_2Efinite__map_2EFDOM,type,(c_2Efinite__map_2EFDOM:(del>(del>$i)))).
thf(mem_c_2Efinite__map_2EFDOM,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27b)@(arr@A_27a@bool)))))).
thf(tp_c_2Efinite__map_2EFEMPTY,type,(c_2Efinite__map_2EFEMPTY:(del>(del>$i)))).
thf(mem_c_2Efinite__map_2EFEMPTY,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Efinite__map_2EFEMPTY@A_27a@A_27b)@(ty_2Efinite__map_2Efmap@A_27a@A_27b))))).
thf(tp_c_2Efinite__map_2EFEVERY,type,(c_2Efinite__map_2EFEVERY:(del>(del>$i)))).
thf(mem_c_2Efinite__map_2EFEVERY,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Efinite__map_2EFEVERY@A_27a@A_27b)@(arr@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27b)@bool)))))).
thf(tp_c_2Efinite__map_2EFLOOKUP,type,(c_2Efinite__map_2EFLOOKUP:(del>(del>$i)))).
thf(mem_c_2Efinite__map_2EFLOOKUP,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Efinite__map_2EFLOOKUP@A_27a@A_27b)@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27b)@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b))))))).
thf(tp_c_2Efinite__map_2EFMAP__MAP2,type,(c_2Efinite__map_2EFMAP__MAP2:(del>(del>(del>$i))))).
thf(mem_c_2Efinite__map_2EFMAP__MAP2,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : (mem@(c_2Efinite__map_2EFMAP__MAP2@A_27a@A_27b@A_27c)@(arr@(arr@(ty_2Epair_2Eprod@A_27a@A_27c)@A_27b)@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27c)@(ty_2Efinite__map_2Efmap@A_27a@A_27b)))))))).
thf(tp_c_2Efinite__map_2EFMERGE,type,(c_2Efinite__map_2EFMERGE:(del>(del>$i)))).
thf(mem_c_2Efinite__map_2EFMERGE,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Efinite__map_2EFMERGE@A_27a@A_27b)@(arr@(arr@A_27a@(arr@A_27a@A_27a))@(arr@(ty_2Efinite__map_2Efmap@A_27b@A_27a)@(arr@(ty_2Efinite__map_2Efmap@A_27b@A_27a)@(ty_2Efinite__map_2Efmap@A_27b@A_27a)))))))).
thf(tp_c_2Efinite__map_2EFRANGE,type,(c_2Efinite__map_2EFRANGE:(del>(del>$i)))).
thf(mem_c_2Efinite__map_2EFRANGE,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Efinite__map_2EFRANGE@A_27a@A_27b)@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27b)@(arr@A_27b@bool)))))).
thf(tp_c_2Efinite__map_2EFUNION,type,(c_2Efinite__map_2EFUNION:(del>(del>$i)))).
thf(mem_c_2Efinite__map_2EFUNION,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Efinite__map_2EFUNION@A_27a@A_27b)@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27b)@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27b)@(ty_2Efinite__map_2Efmap@A_27a@A_27b))))))).
thf(tp_c_2Efinite__map_2EFUN__FMAP,type,(c_2Efinite__map_2EFUN__FMAP:(del>(del>$i)))).
thf(mem_c_2Efinite__map_2EFUN__FMAP,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Efinite__map_2EFUN__FMAP@A_27a@A_27b)@(arr@(arr@A_27a@A_27b)@(arr@(arr@A_27a@bool)@(ty_2Efinite__map_2Efmap@A_27a@A_27b))))))).
thf(tp_c_2Efinite__map_2EFUPDATE,type,(c_2Efinite__map_2EFUPDATE:(del>(del>$i)))).
thf(mem_c_2Efinite__map_2EFUPDATE,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27b)@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@(ty_2Efinite__map_2Efmap@A_27a@A_27b))))))).
thf(tp_c_2Efinite__map_2EFUPDATE__LIST,type,(c_2Efinite__map_2EFUPDATE__LIST:(del>(del>$i)))).
thf(mem_c_2Efinite__map_2EFUPDATE__LIST,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Efinite__map_2EFUPDATE__LIST@A_27a@A_27b)@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27b)@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@A_27a@A_27b))@(ty_2Efinite__map_2Efmap@A_27a@A_27b))))))).
thf(tp_c_2Efinite__map_2EMAP__KEYS,type,(c_2Efinite__map_2EMAP__KEYS:(del>(del>(del>$i))))).
thf(mem_c_2Efinite__map_2EMAP__KEYS,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : (mem@(c_2Efinite__map_2EMAP__KEYS@A_27a@A_27b@A_27c)@(arr@(arr@A_27a@A_27b)@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27c)@(ty_2Efinite__map_2Efmap@A_27b@A_27c)))))))).
thf(tp_c_2Efinite__map_2ERRESTRICT,type,(c_2Efinite__map_2ERRESTRICT:(del>(del>$i)))).
thf(mem_c_2Efinite__map_2ERRESTRICT,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Efinite__map_2ERRESTRICT@A_27a@A_27b)@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27b)@(arr@(arr@A_27b@bool)@(ty_2Efinite__map_2Efmap@A_27a@A_27b))))))).
thf(tp_c_2Efinite__map_2ESUBMAP,type,(c_2Efinite__map_2ESUBMAP:(del>(del>$i)))).
thf(mem_c_2Efinite__map_2ESUBMAP,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Efinite__map_2ESUBMAP@A_27a@A_27b)@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27b)@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27b)@bool)))))).
thf(tp_c_2Efinite__map_2Ef__o,type,(c_2Efinite__map_2Ef__o:(del>(del>(del>$i))))).
thf(mem_c_2Efinite__map_2Ef__o,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : (mem@(c_2Efinite__map_2Ef__o@A_27a@A_27b@A_27c)@(arr@(ty_2Efinite__map_2Efmap@A_27b@A_27c)@(arr@(arr@A_27a@A_27b)@(ty_2Efinite__map_2Efmap@A_27a@A_27c)))))))).
thf(tp_c_2Efinite__map_2Ef__o__f,type,(c_2Efinite__map_2Ef__o__f:(del>(del>(del>$i))))).
thf(mem_c_2Efinite__map_2Ef__o__f,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : (mem@(c_2Efinite__map_2Ef__o__f@A_27a@A_27b@A_27c)@(arr@(ty_2Efinite__map_2Efmap@A_27b@A_27c)@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27b)@(ty_2Efinite__map_2Efmap@A_27a@A_27c)))))))).
thf(tp_c_2Efinite__map_2Efdomsub,type,(c_2Efinite__map_2Efdomsub:(del>(del>$i)))).
thf(mem_c_2Efinite__map_2Efdomsub,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Efinite__map_2Efdomsub@A_27a@A_27b)@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27b)@(arr@A_27a@(ty_2Efinite__map_2Efmap@A_27a@A_27b))))))).
thf(tp_c_2Efinite__map_2Efmap__ABS,type,(c_2Efinite__map_2Efmap__ABS:(del>(del>$i)))).
thf(mem_c_2Efinite__map_2Efmap__ABS,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Efinite__map_2Efmap__ABS@A_27a@A_27b)@(arr@(arr@A_27a@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone))@(ty_2Efinite__map_2Efmap@A_27a@A_27b)))))).
thf(tp_c_2Efinite__map_2Efmap__EQ__UPTO,type,(c_2Efinite__map_2Efmap__EQ__UPTO:(del>(del>$i)))).
thf(mem_c_2Efinite__map_2Efmap__EQ__UPTO,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Efinite__map_2Efmap__EQ__UPTO@A_27a@A_27b)@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27b)@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27b)@(arr@(arr@A_27a@bool)@bool))))))).
thf(tp_c_2Efinite__map_2Efmap__REP,type,(c_2Efinite__map_2Efmap__REP:(del>(del>$i)))).
thf(mem_c_2Efinite__map_2Efmap__REP,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Efinite__map_2Efmap__REP@A_27a@A_27b)@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27b)@(arr@A_27a@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone))))))).
thf(tp_c_2Efinite__map_2Efmap__inverse,type,(c_2Efinite__map_2Efmap__inverse:(del>(del>$i)))).
thf(mem_c_2Efinite__map_2Efmap__inverse,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Efinite__map_2Efmap__inverse@A_27a@A_27b)@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27b)@(arr@(ty_2Efinite__map_2Efmap@A_27b@A_27a)@bool)))))).
thf(tp_c_2Efinite__map_2Efmap__rel,type,(c_2Efinite__map_2Efmap__rel:(del>(del>(del>$i))))).
thf(mem_c_2Efinite__map_2Efmap__rel,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : (mem@(c_2Efinite__map_2Efmap__rel@A_27a@A_27b@A_27c)@(arr@(arr@A_27a@(arr@A_27b@bool))@(arr@(ty_2Efinite__map_2Efmap@A_27c@A_27a)@(arr@(ty_2Efinite__map_2Efmap@A_27c@A_27b)@bool)))))))).
thf(tp_c_2Efinite__map_2Efmap__size,type,(c_2Efinite__map_2Efmap__size:(del>(del>$i)))).
thf(mem_c_2Efinite__map_2Efmap__size,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Efinite__map_2Efmap__size@A_27a@A_27b)@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@(arr@A_27b@ty_2Enum_2Enum)@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27b)@ty_2Enum_2Enum))))))).
thf(tp_c_2Efinite__map_2Eis__fmap,type,(c_2Efinite__map_2Eis__fmap:(del>(del>$i)))).
thf(mem_c_2Efinite__map_2Eis__fmap,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Efinite__map_2Eis__fmap@A_27a@A_27b)@(arr@(arr@A_27a@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone))@bool))))).
thf(tp_c_2Efinite__map_2Eo__f,type,(c_2Efinite__map_2Eo__f:(del>(del>(del>$i))))).
thf(mem_c_2Efinite__map_2Eo__f,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : (mem@(c_2Efinite__map_2Eo__f@A_27a@A_27b@A_27c)@(arr@(arr@A_27b@A_27c)@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27b)@(ty_2Efinite__map_2Efmap@A_27a@A_27c)))))))).
thf(ax_thm_2Efinite__map_2Eis__fmap__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ((c_2Efinite__map_2Eis__fmap@A_27a@A_27b) = (lam@(arr@A_27a@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone))@(^ [V0a0:$i] : (ap@(c_2Ebool_2E_21@(arr@(arr@A_27a@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone))@bool))@(lam@(arr@(arr@A_27a@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone))@bool)@(^ [V1is__fmap_27:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(c_2Ebool_2E_21@(arr@A_27a@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone)))@(lam@(arr@A_27a@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone))@(^ [V2a0:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(c_2Emin_2E_3D@(arr@A_27a@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone)))@V2a0)@(lam@A_27a@(^ [V3a:$i] : (ap@(c_2Esum_2EINR@A_27b@ty_2Eone_2Eone)@(inj__ty_2Eone_2Eone @ fo__c_2Eone_2Eone))))))@(ap@(c_2Ebool_2E_3F@(arr@A_27a@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone)))@(lam@(arr@A_27a@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone))@(^ [V4f:$i] : (ap@(c_2Ebool_2E_3F@A_27a)@(lam@A_27a@(^ [V5a:$i] : (ap@(c_2Ebool_2E_3F@A_27b)@(lam@A_27b@(^ [V6b:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@(arr@A_27a@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone)))@V2a0)@(lam@A_27a@(^ [V7x:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone))@(ap@(ap@(c_2Emin_2E_3D@A_27a)@V7x)@V5a))@(ap@(c_2Esum_2EINL@A_27b@ty_2Eone_2Eone)@V6b))@(ap@V4f@V7x))))))@(ap@V1is__fmap_27@V4f)))))))))))))@(ap@V1is__fmap_27@V2a0))))))@(ap@V1is__fmap_27@V0a0))))))))))).
thf(conj_thm_2Efinite__map_2Eis__fmap__rules,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ((p@(ap@(c_2Efinite__map_2Eis__fmap@A_27a@A_27b)@(lam@A_27a@(^ [V0a:$i] : (ap@(c_2Esum_2EINR@A_27b@ty_2Eone_2Eone)@(inj__ty_2Eone_2Eone @ fo__c_2Eone_2Eone)))))) & ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone))) => ( ! [V2a:$i] : ((mem@V2a@A_27a) => ( ! [V3b:$i] : ((mem@V3b@A_27b) => ((p@(ap@(c_2Efinite__map_2Eis__fmap@A_27a@A_27b)@V1f)) => (p@(ap@(c_2Efinite__map_2Eis__fmap@A_27a@A_27b)@(lam@A_27a@(^ [V4x:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone))@(ap@(ap@(c_2Emin_2E_3D@A_27a)@V4x)@V2a))@(ap@(c_2Esum_2EINL@A_27b@ty_2Eone_2Eone)@V3b))@(ap@V1f@V4x))))))))))))))))).
thf(conj_thm_2Efinite__map_2Eis__fmap__ind,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0is__fmap_27:$i] : ((mem@V0is__fmap_27@(arr@(arr@A_27a@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone))@bool)) => (((p@(ap@V0is__fmap_27@(lam@A_27a@(^ [V1a:$i] : (ap@(c_2Esum_2EINR@A_27b@ty_2Eone_2Eone)@(inj__ty_2Eone_2Eone @ fo__c_2Eone_2Eone)))))) & ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone))) => ( ! [V3a:$i] : ((mem@V3a@A_27a) => ( ! [V4b:$i] : ((mem@V4b@A_27b) => ((p@(ap@V0is__fmap_27@V2f)) => (p@(ap@V0is__fmap_27@(lam@A_27a@(^ [V5x:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone))@(ap@(ap@(c_2Emin_2E_3D@A_27a)@V5x)@V3a))@(ap@(c_2Esum_2EINL@A_27b@ty_2Eone_2Eone)@V4b))@(ap@V2f@V5x)))))))))))))) => ( ! [V6a0:$i] : ((mem@V6a0@(arr@A_27a@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone))) => ((p@(ap@(c_2Efinite__map_2Eis__fmap@A_27a@A_27b)@V6a0)) => (p@(ap@V0is__fmap_27@V6a0))))))))))).
thf(conj_thm_2Efinite__map_2Eis__fmap__strongind,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0is__fmap_27:$i] : ((mem@V0is__fmap_27@(arr@(arr@A_27a@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone))@bool)) => (((p@(ap@V0is__fmap_27@(lam@A_27a@(^ [V1a:$i] : (ap@(c_2Esum_2EINR@A_27b@ty_2Eone_2Eone)@(inj__ty_2Eone_2Eone @ fo__c_2Eone_2Eone)))))) & ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone))) => ( ! [V3a:$i] : ((mem@V3a@A_27a) => ( ! [V4b:$i] : ((mem@V4b@A_27b) => (((p@(ap@(c_2Efinite__map_2Eis__fmap@A_27a@A_27b)@V2f)) & (p@(ap@V0is__fmap_27@V2f))) => (p@(ap@V0is__fmap_27@(lam@A_27a@(^ [V5x:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone))@(ap@(ap@(c_2Emin_2E_3D@A_27a)@V5x)@V3a))@(ap@(c_2Esum_2EINL@A_27b@ty_2Eone_2Eone)@V4b))@(ap@V2f@V5x)))))))))))))) => ( ! [V6a0:$i] : ((mem@V6a0@(arr@A_27a@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone))) => ((p@(ap@(c_2Efinite__map_2Eis__fmap@A_27a@A_27b)@V6a0)) => (p@(ap@V0is__fmap_27@V6a0))))))))))).
thf(conj_thm_2Efinite__map_2Eis__fmap__cases,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0a0:$i] : ((mem@V0a0@(arr@A_27a@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone))) => ((p@(ap@(c_2Efinite__map_2Eis__fmap@A_27a@A_27b)@V0a0)) <=> ((V0a0 = (lam@A_27a@(^ [V1a:$i] : (ap@(c_2Esum_2EINR@A_27b@ty_2Eone_2Eone)@(inj__ty_2Eone_2Eone @ fo__c_2Eone_2Eone))))) | (? [V2f:$i] : ((mem@V2f@(arr@A_27a@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone))) & (? [V3a:$i] : ((mem@V3a@A_27a) & (? [V4b:$i] : ((mem@V4b@A_27b) & ((V0a0 = (lam@A_27a@(^ [V5x:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone))@(ap@(ap@(c_2Emin_2E_3D@A_27a)@V5x)@V3a))@(ap@(c_2Esum_2EINL@A_27b@ty_2Eone_2Eone)@V4b))@(ap@V2f@V5x))))) & (p@(ap@(c_2Efinite__map_2Eis__fmap@A_27a@A_27b)@V2f)))))))))))))))).
thf(ax_thm_2Efinite__map_2Efmap__TY__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (? [V0rep:$i] : ((mem@V0rep@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27b)@(arr@A_27a@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone)))) & (p@(ap@(ap@(c_2Ebool_2ETYPE__DEFINITION@(arr@A_27a@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone))@(ty_2Efinite__map_2Efmap@A_27a@A_27b))@(c_2Efinite__map_2Eis__fmap@A_27a@A_27b))@V0rep))))))).
thf(ax_thm_2Efinite__map_2Efmap__ISO__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0a:$i] : ((mem@V0a@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ((ap@(c_2Efinite__map_2Efmap__ABS@A_27a@A_27b)@(ap@(c_2Efinite__map_2Efmap__REP@A_27a@A_27b)@V0a)) = V0a))) & ( ! [V1r:$i] : ((mem@V1r@(arr@A_27a@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone))) => ((p@(ap@(c_2Efinite__map_2Eis__fmap@A_27a@A_27b)@V1r)) <=> ((ap@(c_2Efinite__map_2Efmap__REP@A_27a@A_27b)@(ap@(c_2Efinite__map_2Efmap__ABS@A_27a@A_27b)@V1r)) = V1r)))))))).
thf(ax_thm_2Efinite__map_2EFUPDATE__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2y:$i] : ((mem@V2y@A_27b) => ((ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1x)@V2y)) = (ap@(c_2Efinite__map_2Efmap__ABS@A_27a@A_27b)@(lam@A_27a@(^ [V3a:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Esum_2Esum@A_27b@ty_2Eone_2Eone))@(ap@(ap@(c_2Emin_2E_3D@A_27a)@V3a)@V1x))@(ap@(c_2Esum_2EINL@A_27b@ty_2Eone_2Eone)@V2y))@(ap@(ap@(c_2Efinite__map_2Efmap__REP@A_27a@A_27b)@V0f)@V3a))))))))))))))).
thf(ax_thm_2Efinite__map_2EFEMPTY__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ((c_2Efinite__map_2EFEMPTY@A_27a@A_27b) = (ap@(c_2Efinite__map_2Efmap__ABS@A_27a@A_27b)@(lam@A_27a@(^ [V0a:$i] : (ap@(c_2Esum_2EINR@A_27b@ty_2Eone_2Eone)@(inj__ty_2Eone_2Eone @ fo__c_2Eone_2Eone))))))))).
thf(ax_thm_2Efinite__map_2EFAPPLY__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V0f)@V1x) = (ap@(c_2Esum_2EOUTL@A_27b@ty_2Eone_2Eone)@(ap@(ap@(c_2Efinite__map_2Efmap__REP@A_27a@A_27b)@V0f)@V1x)))))))))).
thf(ax_thm_2Efinite__map_2EFDOM__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((p@(ap@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f)@V1x)) <=> (p@(ap@(c_2Esum_2EISL@A_27b@ty_2Eone_2Eone)@(ap@(ap@(c_2Efinite__map_2Efmap__REP@A_27a@A_27b)@V0f)@V1x))))))))))).
thf(conj_thm_2Efinite__map_2EFAPPLY__FUPDATE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2y:$i] : ((mem@V2y@A_27b) => ((ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1x)@V2y)))@V1x) = V2y)))))))))).
thf(conj_thm_2Efinite__map_2ENOT__EQ__FAPPLY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1a:$i] : ((mem@V1a@A_27a) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3y:$i] : ((mem@V3y@A_27b) => ((~~ (V1a = V2x)) => ((ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V2x)@V3y)))@V1a) = (ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V0f)@V1a)))))))))))))).
thf(conj_thm_2Efinite__map_2EFUPDATE__COMMUTES,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1a:$i] : ((mem@V1a@A_27a) => ( ! [V2b:$i] : ((mem@V2b@A_27b) => ( ! [V3c:$i] : ((mem@V3c@A_27a) => ( ! [V4d:$i] : ((mem@V4d@A_27b) => ((~~ (V1a = V3c)) => ((ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1a)@V2b)))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V3c)@V4d)) = (ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V3c)@V4d)))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1a)@V2b))))))))))))))))).
thf(conj_thm_2Efinite__map_2EFUPDATE__EQ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1a:$i] : ((mem@V1a@A_27a) => ( ! [V2b:$i] : ((mem@V2b@A_27b) => ( ! [V3c:$i] : ((mem@V3c@A_27b) => ((ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1a)@V2b)))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1a)@V3c)) = (ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1a)@V3c)))))))))))))).
thf(conj_thm_2Efinite__map_2EFDOM__FEMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ((ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@(c_2Efinite__map_2EFEMPTY@A_27a@A_27b)) = (c_2Epred__set_2EEMPTY@A_27a))))).
thf(conj_thm_2Efinite__map_2EFDOM__FUPDATE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1a:$i] : ((mem@V1a@A_27a) => ( ! [V2b:$i] : ((mem@V2b@A_27b) => ((ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1a)@V2b))) = (ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1a)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f)))))))))))).
thf(conj_thm_2Efinite__map_2EFAPPLY__FUPDATE__THM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1a:$i] : ((mem@V1a@A_27a) => ( ! [V2b:$i] : ((mem@V2b@A_27b) => ( ! [V3x:$i] : ((mem@V3x@A_27a) => ((ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1a)@V2b)))@V3x) = (ap@(ap@(ap@(c_2Ebool_2ECOND@A_27b)@(ap@(ap@(c_2Emin_2E_3D@A_27a)@V3x)@V1a))@V2b)@(ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V0f)@V3x)))))))))))))).
thf(conj_thm_2Efinite__map_2ENOT__EQ__FEMPTY__FUPDATE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1a:$i] : ((mem@V1a@A_27a) => ( ! [V2b:$i] : ((mem@V2b@A_27b) => (~~ ((c_2Efinite__map_2EFEMPTY@A_27a@A_27b) = (ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1a)@V2b))))))))))))).
thf(conj_thm_2Efinite__map_2EFDOM__EQ__FDOM__FUPDATE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f))) => ( ! [V2y:$i] : ((mem@V2y@A_27b) => ((ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1x)@V2y))) = (ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f)))))))))))).
thf(conj_thm_2Efinite__map_2Efmap__SIMPLE__INDUCT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27b)@bool)) => (((p@(ap@V0P@(c_2Efinite__map_2EFEMPTY@A_27a@A_27b))) & ( ! [V1f:$i] : ((mem@V1f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ((p@(ap@V0P@V1f)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3y:$i] : ((mem@V3y@A_27b) => (p@(ap@V0P@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V1f)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V2x)@V3y)))))))))))) => ( ! [V4f:$i] : ((mem@V4f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => (p@(ap@V0P@V4f)))))))))).
thf(conj_thm_2Efinite__map_2EFDOM__EQ__EMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => (((ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f) = (c_2Epred__set_2EEMPTY@A_27a)) <=> (V0f = (c_2Efinite__map_2EFEMPTY@A_27a@A_27b)))))))).
thf(conj_thm_2Efinite__map_2EFDOM__EQ__EMPTY__SYM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => (((c_2Epred__set_2EEMPTY@A_27a) = (ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f)) <=> (V0f = (c_2Efinite__map_2EFEMPTY@A_27a@A_27b)))))))).
thf(conj_thm_2Efinite__map_2EFDOM__F__FEMPTY1,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => (( ! [V1a:$i] : ((mem@V1a@A_27a) => (~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1a)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f)))))) <=> (V0f = (c_2Efinite__map_2EFEMPTY@A_27a@A_27b)))))))).
thf(conj_thm_2Efinite__map_2EFDOM__FINITE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0fm:$i] : ((mem@V0fm@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0fm)))))))).
thf(ax_thm_2Efinite__map_2EFCARD__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0fm:$i] : ((mem@V0fm@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Efinite__map_2EFCARD@A_27a@A_27b)@V0fm)) = (surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0fm))))))))).
thf(conj_thm_2Efinite__map_2EFCARD__FEMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ((surj__ty_2Enum_2Enum @ (ap@(c_2Efinite__map_2EFCARD@A_27a@A_27b)@(c_2Efinite__map_2EFEMPTY@A_27a@A_27b))) = fo__c_2Enum_2E0)))).
thf(conj_thm_2Efinite__map_2EFCARD__FUPDATE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0fm:$i] : ((mem@V0fm@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1a:$i] : ((mem@V1a@A_27a) => ( ! [V2b:$i] : ((mem@V2b@A_27b) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Efinite__map_2EFCARD@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V0fm)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1a)@V2b)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1a)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0fm)))@(ap@(c_2Efinite__map_2EFCARD@A_27a@A_27b)@V0fm))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@(c_2Efinite__map_2EFCARD@A_27a@A_27b)@V0fm)))))))))))))).
thf(conj_thm_2Efinite__map_2EFCARD__0__FEMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => (((surj__ty_2Enum_2Enum @ (ap@(c_2Efinite__map_2EFCARD@A_27a@A_27b)@V0f)) = fo__c_2Enum_2E0) <=> (V0f = (c_2Efinite__map_2EFEMPTY@A_27a@A_27b)))))))).
thf(conj_thm_2Efinite__map_2EFCARD__SUC,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1n:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum @ (ap@(c_2Efinite__map_2EFCARD@A_27a@A_27b)@V0f)) = (surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))) <=> (? [V2f_27:$i] : ((mem@V2f_27@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) & (? [V3x:$i] : ((mem@V3x@A_27a) & (? [V4y:$i] : ((mem@V4y@A_27b) & ((~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V2f_27)))) & (((surj__ty_2Enum_2Enum @ (ap@(c_2Efinite__map_2EFCARD@A_27a@A_27b)@V2f_27)) = V1n) & (V0f = (ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V2f_27)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V3x)@V4y)))))))))))))))))).
thf(conj_thm_2Efinite__map_2Efmap__INDUCT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Efinite__map_2Efmap@A_27a@A_27b)@bool)) => (((p@(ap@V0P@(c_2Efinite__map_2EFEMPTY@A_27a@A_27b))) & ( ! [V1f:$i] : ((mem@V1f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ((p@(ap@V0P@V1f)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3y:$i] : ((mem@V3y@A_27b) => ((~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V1f)))) => (p@(ap@V0P@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V1f)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V2x)@V3y))))))))))))) => ( ! [V4f:$i] : ((mem@V4f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => (p@(ap@V0P@V4f)))))))))).
thf(conj_thm_2Efinite__map_2EFM__PULL__APART,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0fm:$i] : ((mem@V0fm@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1k:$i] : ((mem@V1k@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1k)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0fm))) => (? [V2fm0:$i] : ((mem@V2fm0@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) & (? [V3v:$i] : ((mem@V3v@A_27b) & ((V0fm = (ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V2fm0)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1k)@V3v))) & (~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1k)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V2fm0))))))))))))))))).
thf(conj_thm_2Efinite__map_2ENOT__FDOM__FAPPLY__FEMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f)))) => ((ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V0f)@V1x) = (ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@(c_2Efinite__map_2EFEMPTY@A_27a@A_27b))@V1x)))))))))).
thf(conj_thm_2Efinite__map_2Efmap__EQ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1g:$i] : ((mem@V1g@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ((((ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f) = (ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V1g)) & ((ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V0f) = (ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V1g))) <=> (V0f = V1g))))))))).
thf(conj_thm_2Efinite__map_2Efmap__EQ__THM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1g:$i] : ((mem@V1g@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ((((ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f) = (ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V1g)) & ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f))) => ((ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V0f)@V2x) = (ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V1g)@V2x)))))) <=> (V0f = V1g))))))))).
thf(conj_thm_2Efinite__map_2Efmap__EXT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1g:$i] : ((mem@V1g@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ((V0f = V1g) <=> (((ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f) = (ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V1g)) & ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f))) => ((ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V0f)@V2x) = (ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V1g)@V2x)))))))))))))).
thf(ax_thm_2Efinite__map_2ESUBMAP__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1g:$i] : ((mem@V1g@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ((p@(ap@(ap@(c_2Efinite__map_2ESUBMAP@A_27a@A_27b)@V0f)@V1g)) <=> ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f))) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V1g))) & ((ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V0f)@V2x) = (ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V1g)@V2x)))))))))))))).
thf(conj_thm_2Efinite__map_2ESUBMAP__FEMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => (p@(ap@(ap@(c_2Efinite__map_2ESUBMAP@A_27a@A_27b)@(c_2Efinite__map_2EFEMPTY@A_27a@A_27b))@V0f))))))).
thf(conj_thm_2Efinite__map_2ESUBMAP__REFL,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => (p@(ap@(ap@(c_2Efinite__map_2ESUBMAP@A_27a@A_27b)@V0f)@V0f))))))).
thf(conj_thm_2Efinite__map_2ESUBMAP__ANTISYM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1g:$i] : ((mem@V1g@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => (((p@(ap@(ap@(c_2Efinite__map_2ESUBMAP@A_27a@A_27b)@V0f)@V1g)) & (p@(ap@(ap@(c_2Efinite__map_2ESUBMAP@A_27a@A_27b)@V1g)@V0f))) <=> (V0f = V1g))))))))).
thf(conj_thm_2Efinite__map_2ESUBMAP__TRANS,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1g:$i] : ((mem@V1g@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V2h:$i] : ((mem@V2h@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => (((p@(ap@(ap@(c_2Efinite__map_2ESUBMAP@A_27a@A_27b)@V0f)@V1g)) & (p@(ap@(ap@(c_2Efinite__map_2ESUBMAP@A_27a@A_27b)@V1g)@V2h))) => (p@(ap@(ap@(c_2Efinite__map_2ESUBMAP@A_27a@A_27b)@V0f)@V2h)))))))))))).
thf(conj_thm_2Efinite__map_2EEQ__FDOM__SUBMAP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1g:$i] : ((mem@V1g@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ((V0f = V1g) <=> ((p@(ap@(ap@(c_2Efinite__map_2ESUBMAP@A_27a@A_27b)@V0f)@V1g)) & ((ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f) = (ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V1g))))))))))).
thf(conj_thm_2Efinite__map_2ESUBMAP__FUPDATE__EQN,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2y:$i] : ((mem@V2y@A_27b) => ((p@(ap@(ap@(c_2Efinite__map_2ESUBMAP@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1x)@V2y)))) <=> ((~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f)))) | (((ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V0f)@V1x) = V2y) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f))))))))))))))).
thf(ax_thm_2Efinite__map_2EDRESTRICT__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1r:$i] : ((mem@V1r@(arr@A_27a@bool)) => (((ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V0f)@V1r)) = (ap@(ap@(c_2Epred__set_2EINTER@A_27a)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f))@V1r)) & ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V0f)@V1r))@V2x) = (ap@(ap@(ap@(c_2Ebool_2ECOND@A_27b)@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f))@V1r)))@(ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V0f)@V2x))@(ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@(c_2Efinite__map_2EFEMPTY@A_27a@A_27b))@V2x))))))))))))).
thf(conj_thm_2Efinite__map_2EDRESTRICT__FEMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r:$i] : ((mem@V0r@(arr@A_27a@bool)) => ((ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@(c_2Efinite__map_2EFEMPTY@A_27a@A_27b))@V0r) = (c_2Efinite__map_2EFEMPTY@A_27a@A_27b))))))).
thf(conj_thm_2Efinite__map_2EDRESTRICT__FUPDATE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1r:$i] : ((mem@V1r@(arr@A_27a@bool)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3y:$i] : ((mem@V3y@A_27b) => ((ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V2x)@V3y)))@V1r) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Efinite__map_2Efmap@A_27a@A_27b))@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1r))@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V0f)@V1r))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V2x)@V3y)))@(ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V0f)@V1r)))))))))))))).
thf(conj_thm_2Efinite__map_2ESTRONG__DRESTRICT__FUPDATE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1r:$i] : ((mem@V1r@(arr@A_27a@bool)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3y:$i] : ((mem@V3y@A_27b) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1r)) => ((ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V2x)@V3y)))@V1r) = (ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V1r)@V2x)))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V2x)@V3y))))))))))))))).
thf(conj_thm_2Efinite__map_2EFDOM__DRESTRICT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1r:$i] : ((mem@V1r@(arr@A_27a@bool)) => ( ! [V2x:$i] : ((mem@V2x@A_27c) => ((ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V0f)@V1r)) = (ap@(ap@(c_2Epred__set_2EINTER@A_27a)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f))@V1r)))))))))))).
thf(conj_thm_2Efinite__map_2ENOT__FDOM__DRESTRICT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f)))) => ((ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V0f)@(ap@(c_2Epred__set_2ECOMPL@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1x)@(c_2Epred__set_2EEMPTY@A_27a)))) = V0f))))))))).
thf(conj_thm_2Efinite__map_2EDRESTRICT__SUBMAP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1r:$i] : ((mem@V1r@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Efinite__map_2ESUBMAP@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V0f)@V1r))@V0f))))))))).
thf(conj_thm_2Efinite__map_2EDRESTRICT__DRESTRICT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1P:$i] : ((mem@V1P@(arr@A_27a@bool)) => ( ! [V2Q:$i] : ((mem@V2Q@(arr@A_27a@bool)) => ((ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V0f)@V1P))@V2Q) = (ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V1P)@V2Q)))))))))))).
thf(conj_thm_2Efinite__map_2EDRESTRICT__IS__FEMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ((ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V0f)@(c_2Epred__set_2EEMPTY@A_27a)) = (c_2Efinite__map_2EFEMPTY@A_27a@A_27b))))))).
thf(conj_thm_2Efinite__map_2EFUPDATE__DRESTRICT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2y:$i] : ((mem@V2y@A_27b) => ((ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1x)@V2y)) = (ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V0f)@(ap@(c_2Epred__set_2ECOMPL@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1x)@(c_2Epred__set_2EEMPTY@A_27a)))))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1x)@V2y)))))))))))).
thf(conj_thm_2Efinite__map_2ESTRONG__DRESTRICT__FUPDATE__THM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1r:$i] : ((mem@V1r@(arr@A_27a@bool)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3y:$i] : ((mem@V3y@A_27b) => ((ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V2x)@V3y)))@V1r) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Efinite__map_2Efmap@A_27a@A_27b))@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1r))@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@(ap@(c_2Epred__set_2ECOMPL@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V2x)@(c_2Epred__set_2EEMPTY@A_27a))))@V1r)))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V2x)@V3y)))@(ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@(ap@(c_2Epred__set_2ECOMPL@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V2x)@(c_2Epred__set_2EEMPTY@A_27a))))@V1r))))))))))))))).
thf(conj_thm_2Efinite__map_2EDRESTRICT__UNIV,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ((ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V0f)@(c_2Epred__set_2EUNIV@A_27a)) = V0f)))))).
thf(conj_thm_2Efinite__map_2ESUBMAP__DRESTRICT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1P:$i] : ((mem@V1P@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Efinite__map_2ESUBMAP@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V0f)@V1P))@V0f))))))))).
thf(conj_thm_2Efinite__map_2EDRESTRICT__EQ__DRESTRICT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f1:$i] : ((mem@V0f1@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1f2:$i] : ((mem@V1f2@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V2s1:$i] : ((mem@V2s1@(arr@A_27a@bool)) => ( ! [V3s2:$i] : ((mem@V3s2@(arr@A_27a@bool)) => (((ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V0f1)@V2s1) = (ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V1f2)@V3s2)) <=> ((p@(ap@(ap@(c_2Efinite__map_2ESUBMAP@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V0f1)@V2s1))@V1f2)) & ((p@(ap@(ap@(c_2Efinite__map_2ESUBMAP@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V1f2)@V3s2))@V0f1)) & ((ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V2s1)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f1)) = (ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V3s2)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V1f2))))))))))))))))).
thf(ax_thm_2Efinite__map_2EFUNION__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1g:$i] : ((mem@V1g@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => (((ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUNION@A_27a@A_27b)@V0f)@V1g)) = (ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f))@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V1g))) & ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUNION@A_27a@A_27b)@V0f)@V1g))@V2x) = (ap@(ap@(ap@(c_2Ebool_2ECOND@A_27b)@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f)))@(ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V0f)@V2x))@(ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V1g)@V2x))))))))))))).
thf(conj_thm_2Efinite__map_2EFUNION__FEMPTY__1,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0g:$i] : ((mem@V0g@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ((ap@(ap@(c_2Efinite__map_2EFUNION@A_27a@A_27b)@(c_2Efinite__map_2EFEMPTY@A_27a@A_27b))@V0g) = V0g)))))).
thf(conj_thm_2Efinite__map_2EFUNION__FEMPTY__2,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ((ap@(ap@(c_2Efinite__map_2EFUNION@A_27a@A_27b)@V0f)@(c_2Efinite__map_2EFEMPTY@A_27a@A_27b)) = V0f)))))).
thf(conj_thm_2Efinite__map_2EFUNION__FUPDATE__1,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1g:$i] : ((mem@V1g@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3y:$i] : ((mem@V3y@A_27b) => ((ap@(ap@(c_2Efinite__map_2EFUNION@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V2x)@V3y)))@V1g) = (ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUNION@A_27a@A_27b)@V0f)@V1g))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V2x)@V3y)))))))))))))).
thf(conj_thm_2Efinite__map_2EFUNION__FUPDATE__2,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1g:$i] : ((mem@V1g@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3y:$i] : ((mem@V3y@A_27b) => ((ap@(ap@(c_2Efinite__map_2EFUNION@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V1g)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V2x)@V3y))) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Efinite__map_2Efmap@A_27a@A_27b))@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f)))@(ap@(ap@(c_2Efinite__map_2EFUNION@A_27a@A_27b)@V0f)@V1g))@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUNION@A_27a@A_27b)@V0f)@V1g))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V2x)@V3y))))))))))))))).
thf(conj_thm_2Efinite__map_2EFDOM__FUNION,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1g:$i] : ((mem@V1g@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V2x:$i] : ((mem@V2x@A_27c) => ((ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUNION@A_27a@A_27b)@V0f)@V1g)) = (ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f))@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V1g))))))))))))).
thf(conj_thm_2Efinite__map_2EFUNION__IDEMPOT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0fm:$i] : ((mem@V0fm@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ((ap@(ap@(c_2Efinite__map_2EFUNION@A_27a@A_27b)@V0fm)@V0fm) = V0fm)))))).
thf(ax_thm_2Efinite__map_2EFMERGE__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0m:$i] : ((mem@V0m@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V1f:$i] : ((mem@V1f@(ty_2Efinite__map_2Efmap@A_27b@A_27a)) => ( ! [V2g:$i] : ((mem@V2g@(ty_2Efinite__map_2Efmap@A_27b@A_27a)) => (((ap@(c_2Efinite__map_2EFDOM@A_27b@A_27a)@(ap@(ap@(ap@(c_2Efinite__map_2EFMERGE@A_27a@A_27b)@V0m)@V1f)@V2g)) = (ap@(ap@(c_2Epred__set_2EUNION@A_27b)@(ap@(c_2Efinite__map_2EFDOM@A_27b@A_27a)@V1f))@(ap@(c_2Efinite__map_2EFDOM@A_27b@A_27a)@V2g))) & ( ! [V3x:$i] : ((mem@V3x@A_27b) => ((ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27b@A_27a)@(ap@(ap@(ap@(c_2Efinite__map_2EFMERGE@A_27a@A_27b)@V0m)@V1f)@V2g))@V3x) = (ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@(ap@c_2Ebool_2E_7E@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V3x)@(ap@(c_2Efinite__map_2EFDOM@A_27b@A_27a)@V1f))))@(ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27b@A_27a)@V2g)@V3x))@(ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@(ap@c_2Ebool_2E_7E@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V3x)@(ap@(c_2Efinite__map_2EFDOM@A_27b@A_27a)@V2g))))@(ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27b@A_27a)@V1f)@V3x))@(ap@(ap@V0m@(ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27b@A_27a)@V1f)@V3x))@(ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27b@A_27a)@V2g)@V3x))))))))))))))))).
thf(conj_thm_2Efinite__map_2EFMERGE__FEMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0m:$i] : ((mem@V0m@(arr@A_27b@(arr@A_27b@A_27b))) => ( ! [V1f:$i] : ((mem@V1f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => (((ap@(ap@(ap@(c_2Efinite__map_2EFMERGE@A_27b@A_27a)@V0m)@V1f)@(c_2Efinite__map_2EFEMPTY@A_27a@A_27b)) = V1f) & ((ap@(ap@(ap@(c_2Efinite__map_2EFMERGE@A_27b@A_27a)@V0m)@(c_2Efinite__map_2EFEMPTY@A_27a@A_27b))@V1f) = V1f))))))))).
thf(conj_thm_2Efinite__map_2EFDOM__FMERGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0m:$i] : ((mem@V0m@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V1f:$i] : ((mem@V1f@(ty_2Efinite__map_2Efmap@A_27b@A_27a)) => ( ! [V2g:$i] : ((mem@V2g@(ty_2Efinite__map_2Efmap@A_27b@A_27a)) => ((ap@(c_2Efinite__map_2EFDOM@A_27b@A_27a)@(ap@(ap@(ap@(c_2Efinite__map_2EFMERGE@A_27a@A_27b)@V0m)@V1f)@V2g)) = (ap@(ap@(c_2Epred__set_2EUNION@A_27b)@(ap@(c_2Efinite__map_2EFDOM@A_27b@A_27a)@V1f))@(ap@(c_2Efinite__map_2EFDOM@A_27b@A_27a)@V2g)))))))))))).
thf(conj_thm_2Efinite__map_2EFMERGE__FUNION,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ((c_2Efinite__map_2EFUNION@A_27a@A_27b) = (ap@(c_2Efinite__map_2EFMERGE@A_27b@A_27a)@(lam@A_27b@(^ [V0x:$i] : (lam@A_27b@(^ [V1y:$i] : V0x))))))))).
thf(conj_thm_2Efinite__map_2EFUNION__FMERGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f1:$i] : ((mem@V0f1@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1f2:$i] : ((mem@V1f2@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V2m:$i] : ((mem@V2m@(arr@A_27b@(arr@A_27b@A_27b))) => ((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f1))@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V1f2))) => ((ap@(ap@(ap@(c_2Efinite__map_2EFMERGE@A_27b@A_27a)@V2m)@V0f1)@V1f2) = (ap@(ap@(c_2Efinite__map_2EFUNION@A_27a@A_27b)@V0f1)@V1f2)))))))))))).
thf(conj_thm_2Efinite__map_2EFMERGE__NO__CHANGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0m:$i] : ((mem@V0m@(arr@A_27b@(arr@A_27b@A_27b))) => ( ! [V1f1:$i] : ((mem@V1f1@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V2f2:$i] : ((mem@V2f2@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ((((ap@(ap@(ap@(c_2Efinite__map_2EFMERGE@A_27b@A_27a)@V0m)@V1f1)@V2f2) = V1f1) <=> ( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V2f2))) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V1f1))) & ((ap@(ap@V0m@(ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V1f1)@V3x))@(ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V2f2)@V3x)) = (ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V1f1)@V3x))))))) & (((ap@(ap@(ap@(c_2Efinite__map_2EFMERGE@A_27b@A_27a)@V0m)@V1f1)@V2f2) = V2f2) <=> ( ! [V4x:$i] : ((mem@V4x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V1f1))) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V2f2))) & ((ap@(ap@V0m@(ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V1f1)@V4x))@(ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V2f2)@V4x)) = (ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V2f2)@V4x))))))))))))))))).
thf(conj_thm_2Efinite__map_2EFMERGE__COMM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0m:$i] : ((mem@V0m@(arr@A_27b@(arr@A_27b@A_27b))) => ((p@(ap@(c_2Ecombin_2ECOMM@(ty_2Efinite__map_2Efmap@A_27a@A_27b)@(ty_2Efinite__map_2Efmap@A_27a@A_27b))@(ap@(c_2Efinite__map_2EFMERGE@A_27b@A_27a)@V0m))) <=> (p@(ap@(c_2Ecombin_2ECOMM@A_27b@A_27b)@V0m)))))))).
thf(conj_thm_2Efinite__map_2EFMERGE__ASSOC,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0m:$i] : ((mem@V0m@(arr@A_27b@(arr@A_27b@A_27b))) => ((p@(ap@(c_2Ecombin_2EASSOC@(ty_2Efinite__map_2Efmap@A_27a@A_27b))@(ap@(c_2Efinite__map_2EFMERGE@A_27b@A_27a)@V0m))) <=> (p@(ap@(c_2Ecombin_2EASSOC@A_27b)@V0m)))))))).
thf(conj_thm_2Efinite__map_2EFMERGE__DRESTRICT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27b@(arr@A_27b@A_27b))) => ( ! [V1st1:$i] : ((mem@V1st1@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V2st2:$i] : ((mem@V2st2@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V3vs:$i] : ((mem@V3vs@(arr@A_27a@bool)) => ((ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@(ap@(ap@(ap@(c_2Efinite__map_2EFMERGE@A_27b@A_27a)@V0f)@V1st1)@V2st2))@V3vs) = (ap@(ap@(ap@(c_2Efinite__map_2EFMERGE@A_27b@A_27a)@V0f)@(ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V1st1)@V3vs))@(ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V2st2)@V3vs)))))))))))))).
thf(conj_thm_2Efinite__map_2EFMERGE__EQ__FEMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0m:$i] : ((mem@V0m@(arr@A_27b@(arr@A_27b@A_27b))) => ( ! [V1f:$i] : ((mem@V1f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V2g:$i] : ((mem@V2g@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => (((ap@(ap@(ap@(c_2Efinite__map_2EFMERGE@A_27b@A_27a)@V0m)@V1f)@V2g) = (c_2Efinite__map_2EFEMPTY@A_27a@A_27b)) <=> ((V1f = (c_2Efinite__map_2EFEMPTY@A_27a@A_27b)) & (V2g = (c_2Efinite__map_2EFEMPTY@A_27a@A_27b))))))))))))).
thf(ax_thm_2Efinite__map_2EFLOOKUP__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((ap@(ap@(c_2Efinite__map_2EFLOOKUP@A_27a@A_27b)@V0f)@V1x) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@A_27b))@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f)))@(ap@(c_2Eoption_2ESOME@A_27b)@(ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V0f)@V1x)))@(c_2Eoption_2ENONE@A_27b)))))))))).
thf(conj_thm_2Efinite__map_2EFLOOKUP__EMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0k:$i] : ((mem@V0k@A_27b) => ((ap@(ap@(c_2Efinite__map_2EFLOOKUP@A_27b@A_27a)@(c_2Efinite__map_2EFEMPTY@A_27b@A_27a))@V0k) = (c_2Eoption_2ENONE@A_27a))))))).
thf(conj_thm_2Efinite__map_2EFLOOKUP__UPDATE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0fm:$i] : ((mem@V0fm@(ty_2Efinite__map_2Efmap@A_27b@A_27a)) => ( ! [V1k1:$i] : ((mem@V1k1@A_27b) => ( ! [V2v:$i] : ((mem@V2v@A_27a) => ( ! [V3k2:$i] : ((mem@V3k2@A_27b) => ((ap@(ap@(c_2Efinite__map_2EFLOOKUP@A_27b@A_27a)@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27b@A_27a)@V0fm)@(ap@(ap@(c_2Epair_2E_2C@A_27b@A_27a)@V1k1)@V2v)))@V3k2) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@A_27a))@(ap@(ap@(c_2Emin_2E_3D@A_27b)@V1k1)@V3k2))@(ap@(c_2Eoption_2ESOME@A_27a)@V2v))@(ap@(ap@(c_2Efinite__map_2EFLOOKUP@A_27b@A_27a)@V0fm)@V3k2)))))))))))))).
thf(conj_thm_2Efinite__map_2EFLOOKUP__SUBMAP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1g:$i] : ((mem@V1g@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V2k:$i] : ((mem@V2k@A_27a) => ( ! [V3v:$i] : ((mem@V3v@A_27b) => (((p@(ap@(ap@(c_2Efinite__map_2ESUBMAP@A_27a@A_27b)@V0f)@V1g)) & ((ap@(ap@(c_2Efinite__map_2EFLOOKUP@A_27a@A_27b)@V0f)@V2k) = (ap@(c_2Eoption_2ESOME@A_27b)@V3v))) => ((ap@(ap@(c_2Efinite__map_2EFLOOKUP@A_27a@A_27b)@V1g)@V2k) = (ap@(c_2Eoption_2ESOME@A_27b)@V3v)))))))))))))).
thf(conj_thm_2Efinite__map_2ESUBMAP__FUPDATE__FLOOKUP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2y:$i] : ((mem@V2y@A_27b) => ((p@(ap@(ap@(c_2Efinite__map_2ESUBMAP@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1x)@V2y)))) <=> (((ap@(ap@(c_2Efinite__map_2EFLOOKUP@A_27a@A_27b)@V0f)@V1x) = (c_2Eoption_2ENONE@A_27b)) | ((ap@(ap@(c_2Efinite__map_2EFLOOKUP@A_27a@A_27b)@V0f)@V1x) = (ap@(c_2Eoption_2ESOME@A_27b)@V2y))))))))))))).
thf(conj_thm_2Efinite__map_2EFLOOKUP__FUNION,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f1:$i] : ((mem@V0f1@(ty_2Efinite__map_2Efmap@A_27b@A_27a)) => ( ! [V1f2:$i] : ((mem@V1f2@(ty_2Efinite__map_2Efmap@A_27b@A_27a)) => ( ! [V2k:$i] : ((mem@V2k@A_27b) => ((ap@(ap@(c_2Efinite__map_2EFLOOKUP@A_27b@A_27a)@(ap@(ap@(c_2Efinite__map_2EFUNION@A_27b@A_27a)@V0f1)@V1f2))@V2k) = (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@A_27a@(ty_2Eoption_2Eoption@A_27a))@(ap@(ap@(c_2Efinite__map_2EFLOOKUP@A_27b@A_27a)@V0f1)@V2k))@(ap@(ap@(c_2Efinite__map_2EFLOOKUP@A_27b@A_27a)@V1f2)@V2k))@(lam@A_27a@(^ [V3v:$i] : (ap@(c_2Eoption_2ESOME@A_27a)@V3v)))))))))))))).
thf(conj_thm_2Efinite__map_2EFLOOKUP__EXT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f1:$i] : ((mem@V0f1@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1f2:$i] : ((mem@V1f2@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ((V0f1 = V1f2) <=> ((ap@(c_2Efinite__map_2EFLOOKUP@A_27a@A_27b)@V0f1) = (ap@(c_2Efinite__map_2EFLOOKUP@A_27a@A_27b)@V1f2)))))))))).
thf(conj_thm_2Efinite__map_2Efmap__eq__flookup,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f1:$i] : ((mem@V0f1@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1f2:$i] : ((mem@V1f2@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ((V0f1 = V1f2) <=> ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((ap@(ap@(c_2Efinite__map_2EFLOOKUP@A_27a@A_27b)@V0f1)@V2x) = (ap@(ap@(c_2Efinite__map_2EFLOOKUP@A_27a@A_27b)@V1f2)@V2x)))))))))))).
thf(conj_thm_2Efinite__map_2EFLOOKUP__DRESTRICT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0fm:$i] : ((mem@V0fm@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2k:$i] : ((mem@V2k@A_27a) => ((ap@(ap@(c_2Efinite__map_2EFLOOKUP@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V0fm)@V1s))@V2k) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@A_27b))@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2k)@V1s))@(ap@(ap@(c_2Efinite__map_2EFLOOKUP@A_27a@A_27b)@V0fm)@V2k))@(c_2Eoption_2ENONE@A_27b)))))))))))).
thf(ax_thm_2Efinite__map_2EFEVERY__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)) => ( ! [V1f:$i] : ((mem@V1f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ((p@(ap@(ap@(c_2Efinite__map_2EFEVERY@A_27a@A_27b)@V0P)@V1f)) <=> ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V1f))) => (p@(ap@V0P@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V2x)@(ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V1f)@V2x))))))))))))))).
thf(conj_thm_2Efinite__map_2EFEVERY__FEMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)) => (p@(ap@(ap@(c_2Efinite__map_2EFEVERY@A_27a@A_27b)@V0P)@(c_2Efinite__map_2EFEMPTY@A_27a@A_27b)))))))).
thf(conj_thm_2Efinite__map_2EFEVERY__FUPDATE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)) => ( ! [V1f:$i] : ((mem@V1f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3y:$i] : ((mem@V3y@A_27b) => ((p@(ap@(ap@(c_2Efinite__map_2EFEVERY@A_27a@A_27b)@V0P)@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V1f)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V2x)@V3y)))) <=> ((p@(ap@V0P@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V2x)@V3y))) & (p@(ap@(ap@(c_2Efinite__map_2EFEVERY@A_27a@A_27b)@V0P)@(ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V1f)@(ap@(c_2Epred__set_2ECOMPL@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V2x)@(c_2Epred__set_2EEMPTY@A_27a))))))))))))))))))).
thf(conj_thm_2Efinite__map_2EFEVERY__FLOOKUP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)) => ( ! [V1f:$i] : ((mem@V1f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V2k:$i] : ((mem@V2k@A_27a) => ( ! [V3v:$i] : ((mem@V3v@A_27b) => (((p@(ap@(ap@(c_2Efinite__map_2EFEVERY@A_27a@A_27b)@V0P)@V1f)) & ((ap@(ap@(c_2Efinite__map_2EFLOOKUP@A_27a@A_27b)@V1f)@V2k) = (ap@(c_2Eoption_2ESOME@A_27b)@V3v))) => (p@(ap@V0P@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V2k)@V3v))))))))))))))).
thf(ax_thm_2Efinite__map_2Ef__o__f__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27b@A_27c)) => ( ! [V1g:$i] : ((mem@V1g@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => (((ap@(c_2Efinite__map_2EFDOM@A_27a@A_27c)@(ap@(ap@(c_2Efinite__map_2Ef__o__f@A_27a@A_27b@A_27c)@V0f)@V1g)) = (ap@(ap@(c_2Epred__set_2EINTER@A_27a)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V1g))@(ap@(c_2Epred__set_2EGSPEC@A_27a@A_27a)@(lam@A_27a@(^ [V2x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V2x)@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V1g)@V2x))@(ap@(c_2Efinite__map_2EFDOM@A_27b@A_27c)@V0f)))))))) & ( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27c)@(ap@(ap@(c_2Efinite__map_2Ef__o__f@A_27a@A_27b@A_27c)@V0f)@V1g)))) => ((ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27c)@(ap@(ap@(c_2Efinite__map_2Ef__o__f@A_27a@A_27b@A_27c)@V0f)@V1g))@V3x) = (ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27b@A_27c)@V0f)@(ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V1g)@V3x))))))))))))))).
thf(conj_thm_2Efinite__map_2Ef__o__f__FEMPTY__1,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ((ap@(ap@(c_2Efinite__map_2Ef__o__f@A_27a@A_27b@A_27c)@(c_2Efinite__map_2EFEMPTY@A_27b@A_27c))@V0f) = (c_2Efinite__map_2EFEMPTY@A_27a@A_27c)))))))).
thf(conj_thm_2Efinite__map_2Ef__o__f__FEMPTY__2,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27b@A_27c)) => ((ap@(ap@(c_2Efinite__map_2Ef__o__f@A_27a@A_27b@A_27c)@V0f)@(c_2Efinite__map_2EFEMPTY@A_27a@A_27b)) = (c_2Efinite__map_2EFEMPTY@A_27a@A_27c)))))))).
thf(ax_thm_2Efinite__map_2Eo__f__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27b@A_27c)) => ( ! [V1g:$i] : ((mem@V1g@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => (((ap@(c_2Efinite__map_2EFDOM@A_27a@A_27c)@(ap@(ap@(c_2Efinite__map_2Eo__f@A_27a@A_27b@A_27c)@V0f)@V1g)) = (ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V1g)) & ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27c)@(ap@(ap@(c_2Efinite__map_2Eo__f@A_27a@A_27b@A_27c)@V0f)@V1g)))) => ((ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27c)@(ap@(ap@(c_2Efinite__map_2Eo__f@A_27a@A_27b@A_27c)@V0f)@V1g))@V2x) = (ap@V0f@(ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V1g)@V2x))))))))))))))).
thf(conj_thm_2Efinite__map_2Eo__f__FDOM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27b@A_27c)) => ( ! [V1g:$i] : ((mem@V1g@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ((ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V1g) = (ap@(c_2Efinite__map_2EFDOM@A_27a@A_27c)@(ap@(ap@(c_2Efinite__map_2Eo__f@A_27a@A_27b@A_27c)@V0f)@V1g))))))))))).
thf(conj_thm_2Efinite__map_2EFDOM__o__f,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27b@A_27c)) => ( ! [V1g:$i] : ((mem@V1g@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ((ap@(c_2Efinite__map_2EFDOM@A_27a@A_27c)@(ap@(ap@(c_2Efinite__map_2Eo__f@A_27a@A_27b@A_27c)@V0f)@V1g)) = (ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V1g)))))))))).
thf(conj_thm_2Efinite__map_2Eo__f__FAPPLY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27b@A_27c)) => ( ! [V1g:$i] : ((mem@V1g@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V1g))) => ((ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27c)@(ap@(ap@(c_2Efinite__map_2Eo__f@A_27a@A_27b@A_27c)@V0f)@V1g))@V2x) = (ap@V0f@(ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V1g)@V2x)))))))))))))).
thf(conj_thm_2Efinite__map_2Eo__f__FEMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27c@A_27b)) => ((ap@(ap@(c_2Efinite__map_2Eo__f@A_27a@A_27c@A_27b)@V0f)@(c_2Efinite__map_2EFEMPTY@A_27a@A_27c)) = (c_2Efinite__map_2EFEMPTY@A_27a@A_27b)))))))).
thf(conj_thm_2Efinite__map_2EFEVERY__o__f,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0m:$i] : ((mem@V0m@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1P:$i] : ((mem@V1P@(arr@(ty_2Epair_2Eprod@A_27a@A_27c)@bool)) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27b@A_27c)) => ((p@(ap@(ap@(c_2Efinite__map_2EFEVERY@A_27a@A_27c)@V1P)@(ap@(ap@(c_2Efinite__map_2Eo__f@A_27a@A_27b@A_27c)@V2f)@V0m))) <=> (p@(ap@(ap@(c_2Efinite__map_2EFEVERY@A_27a@A_27b)@(lam@(ty_2Epair_2Eprod@A_27a@A_27b)@(^ [V3x:$i] : (ap@V1P@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27c)@(ap@(c_2Epair_2EFST@A_27a@A_27b)@V3x))@(ap@V2f@(ap@(c_2Epair_2ESND@A_27a@A_27b)@V3x)))))))@V0m))))))))))))).
thf(conj_thm_2Efinite__map_2Eo__f__o__f,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27c@A_27b)) => ( ! [V1g:$i] : ((mem@V1g@(arr@A_27d@A_27c)) => ( ! [V2h:$i] : ((mem@V2h@(ty_2Efinite__map_2Efmap@A_27a@A_27d)) => ((ap@(ap@(c_2Efinite__map_2Eo__f@A_27a@A_27c@A_27b)@V0f)@(ap@(ap@(c_2Efinite__map_2Eo__f@A_27a@A_27d@A_27c)@V1g)@V2h)) = (ap@(ap@(c_2Efinite__map_2Eo__f@A_27a@A_27d@A_27b)@(ap@(ap@(c_2Ecombin_2Eo@A_27d@A_27b@A_27c)@V0f)@V1g))@V2h))))))))))))).
thf(conj_thm_2Efinite__map_2EFLOOKUP__o__f,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27c@A_27a)) => ( ! [V1fm:$i] : ((mem@V1fm@(ty_2Efinite__map_2Efmap@A_27b@A_27c)) => ( ! [V2k:$i] : ((mem@V2k@A_27b) => ((ap@(ap@(c_2Efinite__map_2EFLOOKUP@A_27b@A_27a)@(ap@(ap@(c_2Efinite__map_2Eo__f@A_27b@A_27c@A_27a)@V0f)@V1fm))@V2k) = (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@A_27c@(ty_2Eoption_2Eoption@A_27a))@(ap@(ap@(c_2Efinite__map_2EFLOOKUP@A_27b@A_27c)@V1fm)@V2k))@(c_2Eoption_2ENONE@A_27a))@(lam@A_27c@(^ [V3v:$i] : (ap@(c_2Eoption_2ESOME@A_27a)@(ap@V0f@V3v)))))))))))))))).
thf(ax_thm_2Efinite__map_2EFRANGE__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ((ap@(c_2Efinite__map_2EFRANGE@A_27a@A_27b)@V0f) = (ap@(c_2Epred__set_2EGSPEC@A_27b@A_27b)@(lam@A_27b@(^ [V1y:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27b@bool)@V1y)@(ap@(c_2Ebool_2E_3F@A_27a)@(lam@A_27a@(^ [V2x:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f)))@(ap@(ap@(c_2Emin_2E_3D@A_27b)@(ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V0f)@V2x))@V1y))))))))))))))).
thf(conj_thm_2Efinite__map_2EFRANGE__FEMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ((ap@(c_2Efinite__map_2EFRANGE@A_27b@A_27a)@(c_2Efinite__map_2EFEMPTY@A_27b@A_27a)) = (c_2Epred__set_2EEMPTY@A_27a))))).
thf(conj_thm_2Efinite__map_2EFRANGE__FUPDATE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2y:$i] : ((mem@V2y@A_27b) => ((ap@(c_2Efinite__map_2EFRANGE@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1x)@V2y))) = (ap@(ap@(c_2Epred__set_2EINSERT@A_27b)@V2y)@(ap@(c_2Efinite__map_2EFRANGE@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V0f)@(ap@(c_2Epred__set_2ECOMPL@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1x)@(c_2Epred__set_2EEMPTY@A_27a)))))))))))))))).
thf(conj_thm_2Efinite__map_2ESUBMAP__FRANGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1g:$i] : ((mem@V1g@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ((p@(ap@(ap@(c_2Efinite__map_2ESUBMAP@A_27a@A_27b)@V0f)@V1g)) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27b)@(ap@(c_2Efinite__map_2EFRANGE@A_27a@A_27b)@V0f))@(ap@(c_2Efinite__map_2EFRANGE@A_27a@A_27b)@V1g))))))))))).
thf(conj_thm_2Efinite__map_2EFINITE__FRANGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0fm:$i] : ((mem@V0fm@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => (p@(ap@(c_2Epred__set_2EFINITE@A_27b)@(ap@(c_2Efinite__map_2EFRANGE@A_27a@A_27b)@V0fm)))))))).
thf(conj_thm_2Efinite__map_2Eo__f__FRANGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1g:$i] : ((mem@V1g@(ty_2Efinite__map_2Efmap@A_27b@A_27a)) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27c)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@(ap@(c_2Efinite__map_2EFRANGE@A_27b@A_27a)@V1g))) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27c)@(ap@V2f@V0x))@(ap@(c_2Efinite__map_2EFRANGE@A_27b@A_27c)@(ap@(ap@(c_2Efinite__map_2Eo__f@A_27b@A_27a@A_27c)@V2f)@V1g))))))))))))))).
thf(conj_thm_2Efinite__map_2EFRANGE__FLOOKUP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : ((mem@V0v@A_27a) => ( ! [V1f:$i] : ((mem@V1f@(ty_2Efinite__map_2Efmap@A_27b@A_27a)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0v)@(ap@(c_2Efinite__map_2EFRANGE@A_27b@A_27a)@V1f))) <=> (? [V2k:$i] : ((mem@V2k@A_27b) & ((ap@(ap@(c_2Efinite__map_2EFLOOKUP@A_27b@A_27a)@V1f)@V2k) = (ap@(c_2Eoption_2ESOME@A_27a)@V0v)))))))))))).
thf(conj_thm_2Efinite__map_2EFRANGE__FUNION,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0fm1:$i] : ((mem@V0fm1@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1fm2:$i] : ((mem@V1fm2@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0fm1))@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V1fm2))) => ((ap@(c_2Efinite__map_2EFRANGE@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUNION@A_27a@A_27b)@V0fm1)@V1fm2)) = (ap@(ap@(c_2Epred__set_2EUNION@A_27b)@(ap@(c_2Efinite__map_2EFRANGE@A_27a@A_27b)@V0fm1))@(ap@(c_2Efinite__map_2EFRANGE@A_27a@A_27b)@V1fm2))))))))))).
thf(ax_thm_2Efinite__map_2ERRESTRICT__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1r:$i] : ((mem@V1r@(arr@A_27b@bool)) => (((ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2ERRESTRICT@A_27a@A_27b)@V0f)@V1r)) = (ap@(c_2Epred__set_2EGSPEC@A_27a@A_27a)@(lam@A_27a@(^ [V2x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V2x)@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f)))@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V0f)@V2x))@V1r))))))) & ( ! [V3x:$i] : ((mem@V3x@A_27a) => ((ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2ERRESTRICT@A_27a@A_27b)@V0f)@V1r))@V3x) = (ap@(ap@(ap@(c_2Ebool_2ECOND@A_27b)@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0f)))@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V0f)@V3x))@V1r)))@(ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V0f)@V3x))@(ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@(c_2Efinite__map_2EFEMPTY@A_27a@A_27b))@V3x))))))))))))).
thf(conj_thm_2Efinite__map_2ERRESTRICT__FEMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r:$i] : ((mem@V0r@(arr@A_27a@bool)) => ((ap@(ap@(c_2Efinite__map_2ERRESTRICT@A_27b@A_27a)@(c_2Efinite__map_2EFEMPTY@A_27b@A_27a))@V0r) = (c_2Efinite__map_2EFEMPTY@A_27b@A_27a))))))).
thf(conj_thm_2Efinite__map_2ERRESTRICT__FUPDATE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1r:$i] : ((mem@V1r@(arr@A_27b@bool)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3y:$i] : ((mem@V3y@A_27b) => ((ap@(ap@(c_2Efinite__map_2ERRESTRICT@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V2x)@V3y)))@V1r) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Efinite__map_2Efmap@A_27a@A_27b))@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V3y)@V1r))@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2ERRESTRICT@A_27a@A_27b)@V0f)@V1r))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V2x)@V3y)))@(ap@(ap@(c_2Efinite__map_2ERRESTRICT@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V0f)@(ap@(c_2Epred__set_2ECOMPL@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V2x)@(c_2Epred__set_2EEMPTY@A_27a)))))@V1r)))))))))))))).
thf(ax_thm_2Efinite__map_2EFUN__FMAP__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1P:$i] : ((mem@V1P@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1P)) => (((ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUN__FMAP@A_27a@A_27b)@V0f)@V1P)) = V1P) & ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1P)) => ((ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUN__FMAP@A_27a@A_27b)@V0f)@V1P))@V2x) = (ap@V0f@V2x)))))))))))))).
thf(conj_thm_2Efinite__map_2EFUN__FMAP__EMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ((ap@(ap@(c_2Efinite__map_2EFUN__FMAP@A_27a@A_27b)@V0f)@(c_2Epred__set_2EEMPTY@A_27a)) = (c_2Efinite__map_2EFEMPTY@A_27a@A_27b))))))).
thf(conj_thm_2Efinite__map_2EFRANGE__FMAP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27b)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0P)) => ((ap@(c_2Efinite__map_2EFRANGE@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUN__FMAP@A_27a@A_27b)@V1f)@V0P)) = (ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V1f)@V0P)))))))))).
thf(conj_thm_2Efinite__map_2EFDOM__FMAP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s)) => ((ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUN__FMAP@A_27a@A_27b)@V0f)@V1s)) = V1s))))))))).
thf(conj_thm_2Efinite__map_2EFLOOKUP__FUN__FMAP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27b)) => ( ! [V2k:$i] : ((mem@V2k@A_27a) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0P)) => ((ap@(ap@(c_2Efinite__map_2EFLOOKUP@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUN__FMAP@A_27a@A_27b)@V1f)@V0P))@V2k) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@A_27b))@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2k)@V0P))@(ap@(c_2Eoption_2ESOME@A_27b)@(ap@V1f@V2k)))@(c_2Eoption_2ENONE@A_27b))))))))))))).
thf(ax_thm_2Efinite__map_2Ef__o__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27b@A_27c)) => ( ! [V1g:$i] : ((mem@V1g@(arr@A_27a@A_27b)) => ((ap@(ap@(c_2Efinite__map_2Ef__o@A_27a@A_27b@A_27c)@V0f)@V1g) = (ap@(ap@(c_2Efinite__map_2Ef__o__f@A_27a@A_27b@A_27c)@V0f)@(ap@(ap@(c_2Efinite__map_2EFUN__FMAP@A_27a@A_27b)@V1g)@(ap@(c_2Epred__set_2EGSPEC@A_27a@A_27a)@(lam@A_27a@(^ [V2x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V2x)@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V1g@V2x))@(ap@(c_2Efinite__map_2EFDOM@A_27b@A_27c)@V0f))))))))))))))))).
thf(conj_thm_2Efinite__map_2EFDOM__f__o,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27b@A_27c)) => ( ! [V1g:$i] : ((mem@V1g@(arr@A_27a@A_27b)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(ap@(c_2Epred__set_2EGSPEC@A_27a@A_27a)@(lam@A_27a@(^ [V2x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V2x)@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V1g@V2x))@(ap@(c_2Efinite__map_2EFDOM@A_27b@A_27c)@V0f)))))))) => ((ap@(c_2Efinite__map_2EFDOM@A_27a@A_27c)@(ap@(ap@(c_2Efinite__map_2Ef__o@A_27a@A_27b@A_27c)@V0f)@V1g)) = (ap@(c_2Epred__set_2EGSPEC@A_27a@A_27a)@(lam@A_27a@(^ [V3x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V3x)@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V1g@V3x))@(ap@(c_2Efinite__map_2EFDOM@A_27b@A_27c)@V0f)))))))))))))))).
thf(conj_thm_2Efinite__map_2Ef__o__FEMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0g:$i] : ((mem@V0g@(arr@A_27a@A_27b)) => ((ap@(ap@(c_2Efinite__map_2Ef__o@A_27a@A_27b@A_27c)@(c_2Efinite__map_2EFEMPTY@A_27b@A_27c))@V0g) = (c_2Efinite__map_2EFEMPTY@A_27a@A_27c)))))))).
thf(conj_thm_2Efinite__map_2Ef__o__FUPDATE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0fm:$i] : ((mem@V0fm@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1k:$i] : ((mem@V1k@A_27a) => ( ! [V2v:$i] : ((mem@V2v@A_27b) => ( ! [V3g:$i] : ((mem@V3g@(arr@A_27c@A_27a)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27c)@(ap@(c_2Epred__set_2EGSPEC@A_27c@A_27c)@(lam@A_27c@(^ [V4x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27c@bool)@V4x)@(ap@(ap@(c_2Ebool_2EIN@A_27a)@(ap@V3g@V4x))@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0fm)))))))) & (p@(ap@(c_2Epred__set_2EFINITE@A_27c)@(ap@(c_2Epred__set_2EGSPEC@A_27c@A_27c)@(lam@A_27c@(^ [V5x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27c@bool)@V5x)@(ap@(ap@(c_2Emin_2E_3D@A_27a)@(ap@V3g@V5x))@V1k)))))))) => ((ap@(ap@(c_2Efinite__map_2Ef__o@A_27c@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V0fm)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1k)@V2v)))@V3g) = (ap@(ap@(ap@(c_2Efinite__map_2EFMERGE@A_27b@A_27c)@(ap@(c_2Ecombin_2EC@A_27b@A_27b@A_27b)@(c_2Ecombin_2EK@A_27b@A_27b)))@(ap@(ap@(c_2Efinite__map_2Ef__o@A_27c@A_27a@A_27b)@V0fm)@V3g))@(ap@(ap@(c_2Efinite__map_2EFUN__FMAP@A_27c@A_27b)@(ap@(c_2Ecombin_2EK@A_27b@A_27c)@V2v))@(ap@(c_2Epred__set_2EGSPEC@A_27c@A_27c)@(lam@A_27c@(^ [V6x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27c@bool)@V6x)@(ap@(ap@(c_2Emin_2E_3D@A_27a)@(ap@V3g@V6x))@V1k))))))))))))))))))))).
thf(conj_thm_2Efinite__map_2EFAPPLY__f__o,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(ty_2Efinite__map_2Efmap@A_27b@A_27c)) => ( ! [V1g:$i] : ((mem@V1g@(arr@A_27a@A_27b)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(ap@(c_2Epred__set_2EGSPEC@A_27a@A_27a)@(lam@A_27a@(^ [V2x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V2x)@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V1g@V2x))@(ap@(c_2Efinite__map_2EFDOM@A_27b@A_27c)@V0f)))))))) => ( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27c)@(ap@(ap@(c_2Efinite__map_2Ef__o@A_27a@A_27b@A_27c)@V0f)@V1g)))) => ((ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27c)@(ap@(ap@(c_2Efinite__map_2Ef__o@A_27a@A_27b@A_27c)@V0f)@V1g))@V3x) = (ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27b@A_27c)@V0f)@(ap@V1g@V3x))))))))))))))).
thf(conj_thm_2Efinite__map_2EFINITE__PRED__11,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0g:$i] : ((mem@V0g@(arr@A_27a@A_27b)) => (( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2y:$i] : ((mem@V2y@A_27a) => (((ap@V0g@V1x) = (ap@V0g@V2y)) <=> (V1x = V2y)))))) => ( ! [V3f:$i] : ((mem@V3f@(ty_2Efinite__map_2Efmap@A_27b@A_27c)) => (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(ap@(c_2Epred__set_2EGSPEC@A_27a@A_27a)@(lam@A_27a@(^ [V4x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V4x)@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V0g@V4x))@(ap@(c_2Efinite__map_2EFDOM@A_27b@A_27c)@V3f))))))))))))))))).
thf(conj_thm_2Efinite__map_2Ef__o__ASSOC,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0g:$i] : ((mem@V0g@(arr@A_27a@A_27b)) => ( ! [V1h:$i] : ((mem@V1h@(arr@A_27c@A_27a)) => ( ! [V2f:$i] : ((mem@V2f@(ty_2Efinite__map_2Efmap@A_27b@A_27d)) => ((( ! [V3x:$i] : ((mem@V3x@A_27a) => ( ! [V4y:$i] : ((mem@V4y@A_27a) => (((ap@V0g@V3x) = (ap@V0g@V4y)) <=> (V3x = V4y)))))) & ( ! [V5x:$i] : ((mem@V5x@A_27c) => ( ! [V6y:$i] : ((mem@V6y@A_27c) => (((ap@V1h@V5x) = (ap@V1h@V6y)) <=> (V5x = V6y))))))) => ((ap@(ap@(c_2Efinite__map_2Ef__o@A_27c@A_27a@A_27d)@(ap@(ap@(c_2Efinite__map_2Ef__o@A_27a@A_27b@A_27d)@V2f)@V0g))@V1h) = (ap@(ap@(c_2Efinite__map_2Ef__o@A_27c@A_27b@A_27d)@V2f)@(ap@(ap@(c_2Ecombin_2Eo@A_27c@A_27b@A_27a)@V0g)@V1h))))))))))))))).
thf(ax_thm_2Efinite__map_2Efmap__domsub,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0fm:$i] : ((mem@V0fm@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1k:$i] : ((mem@V1k@A_27a) => ((ap@(ap@(c_2Efinite__map_2Efdomsub@A_27a@A_27b)@V0fm)@V1k) = (ap@(ap@(c_2Efinite__map_2EDRESTRICT@A_27a@A_27b)@V0fm)@(ap@(c_2Epred__set_2ECOMPL@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1k)@(c_2Epred__set_2EEMPTY@A_27a)))))))))))).
thf(conj_thm_2Efinite__map_2EDOMSUB__FEMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0k:$i] : ((mem@V0k@A_27a) => ((ap@(ap@(c_2Efinite__map_2Efdomsub@A_27a@A_27b)@(c_2Efinite__map_2EFEMPTY@A_27a@A_27b))@V0k) = (c_2Efinite__map_2EFEMPTY@A_27a@A_27b))))))).
thf(conj_thm_2Efinite__map_2EDOMSUB__FUPDATE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0fm:$i] : ((mem@V0fm@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1k:$i] : ((mem@V1k@A_27a) => ( ! [V2v:$i] : ((mem@V2v@A_27b) => ((ap@(ap@(c_2Efinite__map_2Efdomsub@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V0fm)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1k)@V2v)))@V1k) = (ap@(ap@(c_2Efinite__map_2Efdomsub@A_27a@A_27b)@V0fm)@V1k))))))))))).
thf(conj_thm_2Efinite__map_2EDOMSUB__FUPDATE__NEQ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0fm:$i] : ((mem@V0fm@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1k1:$i] : ((mem@V1k1@A_27a) => ( ! [V2k2:$i] : ((mem@V2k2@A_27a) => ( ! [V3v:$i] : ((mem@V3v@A_27b) => ((~~ (V1k1 = V2k2)) => ((ap@(ap@(c_2Efinite__map_2Efdomsub@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V0fm)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1k1)@V3v)))@V2k2) = (ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2Efdomsub@A_27a@A_27b)@V0fm)@V2k2))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1k1)@V3v))))))))))))))).
thf(conj_thm_2Efinite__map_2EDOMSUB__FUPDATE__THM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0fm:$i] : ((mem@V0fm@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1k1:$i] : ((mem@V1k1@A_27a) => ( ! [V2k2:$i] : ((mem@V2k2@A_27a) => ( ! [V3v:$i] : ((mem@V3v@A_27b) => ((ap@(ap@(c_2Efinite__map_2Efdomsub@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@V0fm)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1k1)@V3v)))@V2k2) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Efinite__map_2Efmap@A_27a@A_27b))@(ap@(ap@(c_2Emin_2E_3D@A_27a)@V1k1)@V2k2))@(ap@(ap@(c_2Efinite__map_2Efdomsub@A_27a@A_27b)@V0fm)@V2k2))@(ap@(ap@(c_2Efinite__map_2EFUPDATE@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2Efdomsub@A_27a@A_27b)@V0fm)@V2k2))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1k1)@V3v))))))))))))))).
thf(conj_thm_2Efinite__map_2EFDOM__DOMSUB,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0fm:$i] : ((mem@V0fm@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1k:$i] : ((mem@V1k@A_27a) => ((ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2Efdomsub@A_27a@A_27b)@V0fm)@V1k)) = (ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V0fm))@V1k))))))))).
thf(conj_thm_2Efinite__map_2EDOMSUB__FAPPLY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0fm:$i] : ((mem@V0fm@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1k:$i] : ((mem@V1k@A_27a) => ((ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2Efdomsub@A_27a@A_27b)@V0fm)@V1k))@V1k) = (ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@(c_2Efinite__map_2EFEMPTY@A_27a@A_27b))@V1k))))))))).
thf(conj_thm_2Efinite__map_2EDOMSUB__FAPPLY__NEQ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0fm:$i] : ((mem@V0fm@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1k1:$i] : ((mem@V1k1@A_27a) => ( ! [V2k2:$i] : ((mem@V2k2@A_27a) => ((~~ (V1k1 = V2k2)) => ((ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2Efdomsub@A_27a@A_27b)@V0fm)@V1k1))@V2k2) = (ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V0fm)@V2k2)))))))))))).
thf(conj_thm_2Efinite__map_2EDOMSUB__FAPPLY__THM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0fm:$i] : ((mem@V0fm@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1k1:$i] : ((mem@V1k1@A_27a) => ( ! [V2k2:$i] : ((mem@V2k2@A_27a) => ((ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2Efdomsub@A_27a@A_27b)@V0fm)@V1k1))@V2k2) = (ap@(ap@(ap@(c_2Ebool_2ECOND@A_27b)@(ap@(ap@(c_2Emin_2E_3D@A_27a)@V1k1)@V2k2))@(ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@(c_2Efinite__map_2EFEMPTY@A_27a@A_27b))@V2k2))@(ap@(ap@(c_2Efinite__map_2EFAPPLY@A_27a@A_27b)@V0fm)@V2k2)))))))))))).
thf(conj_thm_2Efinite__map_2EDOMSUB__FLOOKUP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0fm:$i] : ((mem@V0fm@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1k:$i] : ((mem@V1k@A_27a) => ((ap@(ap@(c_2Efinite__map_2EFLOOKUP@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2Efdomsub@A_27a@A_27b)@V0fm)@V1k))@V1k) = (c_2Eoption_2ENONE@A_27b))))))))).
thf(conj_thm_2Efinite__map_2EDOMSUB__FLOOKUP__NEQ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0fm:$i] : ((mem@V0fm@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1k1:$i] : ((mem@V1k1@A_27a) => ( ! [V2k2:$i] : ((mem@V2k2@A_27a) => ((~~ (V1k1 = V2k2)) => ((ap@(ap@(c_2Efinite__map_2EFLOOKUP@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2Efdomsub@A_27a@A_27b)@V0fm)@V1k1))@V2k2) = (ap@(ap@(c_2Efinite__map_2EFLOOKUP@A_27a@A_27b)@V0fm)@V2k2)))))))))))).
thf(conj_thm_2Efinite__map_2EDOMSUB__FLOOKUP__THM,conjecture,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0fm:$i] : ((mem@V0fm@(ty_2Efinite__map_2Efmap@A_27a@A_27b)) => ( ! [V1k1:$i] : ((mem@V1k1@A_27a) => ( ! [V2k2:$i] : ((mem@V2k2@A_27a) => ((ap@(ap@(c_2Efinite__map_2EFLOOKUP@A_27a@A_27b)@(ap@(ap@(c_2Efinite__map_2Efdomsub@A_27a@A_27b)@V0fm)@V1k1))@V2k2) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@A_27b))@(ap@(ap@(c_2Emin_2E_3D@A_27a)@V1k1)@V2k2))@(c_2Eoption_2ENONE@A_27b))@(ap@(ap@(c_2Efinite__map_2EFLOOKUP@A_27a@A_27b)@V0fm)@V2k2)))))))))))).
