include('Axioms/ASCIInumbers+2.ax').
fof(ne_ty_2Efinite__map_2Efmap,axiom,( ! [A0] : ( ne(A0) => ( ! [A1] : ( ne(A1) => ne(ty_2Efinite__map_2Efmap(A0,A1)) ) ) ) )).
fof(mem_c_2Efinite__map_2EDRESTRICT,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => 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)))) ) ) )).
fof(mem_c_2Efinite__map_2EFAPPLY,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efinite__map_2EFAPPLY(A_27a,A_27b),arr(ty_2Efinite__map_2Efmap(A_27a,A_27b),arr(A_27a,A_27b))) ) ) )).
fof(mem_c_2Efinite__map_2EFCARD,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efinite__map_2EFCARD(A_27a,A_27b),arr(ty_2Efinite__map_2Efmap(A_27a,A_27b),ty_2Enum_2Enum)) ) ) )).
fof(mem_c_2Efinite__map_2EFDOM,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efinite__map_2EFDOM(A_27a,A_27b),arr(ty_2Efinite__map_2Efmap(A_27a,A_27b),arr(A_27a,bool))) ) ) )).
fof(mem_c_2Efinite__map_2EFEMPTY,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efinite__map_2EFEMPTY(A_27a,A_27b),ty_2Efinite__map_2Efmap(A_27a,A_27b)) ) ) )).
fof(mem_c_2Efinite__map_2EFEVERY,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => 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))) ) ) )).
fof(mem_c_2Efinite__map_2EFLOOKUP,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => 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)))) ) ) )).
fof(mem_c_2Efinite__map_2EFMAP__MAP2,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => 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)))) ) ) ) )).
fof(mem_c_2Efinite__map_2EFMERGE,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => 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))))) ) ) )).
fof(mem_c_2Efinite__map_2EFRANGE,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efinite__map_2EFRANGE(A_27a,A_27b),arr(ty_2Efinite__map_2Efmap(A_27a,A_27b),arr(A_27b,bool))) ) ) )).
fof(mem_c_2Efinite__map_2EFUNION,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => 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)))) ) ) )).
fof(mem_c_2Efinite__map_2EFUN__FMAP,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => 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)))) ) ) )).
fof(mem_c_2Efinite__map_2EFUPDATE,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => 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)))) ) ) )).
fof(mem_c_2Efinite__map_2EFUPDATE__LIST,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => 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)))) ) ) )).
fof(mem_c_2Efinite__map_2EMAP__KEYS,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => 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)))) ) ) ) )).
fof(mem_c_2Efinite__map_2ERRESTRICT,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => 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)))) ) ) )).
fof(mem_c_2Efinite__map_2ESUBMAP,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => 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))) ) ) )).
fof(mem_c_2Efinite__map_2Ef__o,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => 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)))) ) ) ) )).
fof(mem_c_2Efinite__map_2Ef__o__f,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => 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)))) ) ) ) )).
fof(mem_c_2Efinite__map_2Efdomsub,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => 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)))) ) ) )).
fof(mem_c_2Efinite__map_2Efmap__ABS,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => 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))) ) ) )).
fof(mem_c_2Efinite__map_2Efmap__EQ__UPTO,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => 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)))) ) ) )).
fof(mem_c_2Efinite__map_2Efmap__REP,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => 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)))) ) ) )).
fof(mem_c_2Efinite__map_2Efmap__inverse,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => 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))) ) ) )).
fof(mem_c_2Efinite__map_2Efmap__rel,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => 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)))) ) ) ) )).
fof(mem_c_2Efinite__map_2Efmap__size,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => 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)))) ) ) )).
fof(mem_c_2Efinite__map_2Eis__fmap,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efinite__map_2Eis__fmap(A_27a,A_27b),arr(arr(A_27a,ty_2Esum_2Esum(A_27b,ty_2Eone_2Eone)),bool)) ) ) )).
fof(mem_c_2Efinite__map_2Eo__f,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => 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)))) ) ) ) )).
fof(ax_thm_2Efinite__map_2Eis__fmap__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( c_2Efinite__map_2Eis__fmap(A_27a,A_27b) = f1900(A_27a,A_27b) ) ) ) )).
fof(conj_thm_2Efinite__map_2Eis__fmap__rules,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( p(ap(c_2Efinite__map_2Eis__fmap(A_27a,A_27b),k(A_27a,ap(c_2Esum_2EINR(A_27b,ty_2Eone_2Eone),c_2Eone_2Eone)))) & ! [V1f] : ( mem(V1f,arr(A_27a,ty_2Esum_2Esum(A_27b,ty_2Eone_2Eone))) => ! [V2a] : ( mem(V2a,A_27a) => ! [V3b] : ( 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),f1901(A_27b,A_27a,V3b,V2a,V1f))) ) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2Eis__fmap__ind,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0is__fmap_27] : ( mem(V0is__fmap_27,arr(arr(A_27a,ty_2Esum_2Esum(A_27b,ty_2Eone_2Eone)),bool)) => ( ( p(ap(V0is__fmap_27,k(A_27a,ap(c_2Esum_2EINR(A_27b,ty_2Eone_2Eone),c_2Eone_2Eone)))) & ! [V2f] : ( mem(V2f,arr(A_27a,ty_2Esum_2Esum(A_27b,ty_2Eone_2Eone))) => ! [V3a] : ( mem(V3a,A_27a) => ! [V4b] : ( mem(V4b,A_27b) => ( p(ap(V0is__fmap_27,V2f)) => p(ap(V0is__fmap_27,f1902(A_27b,A_27a,V4b,V3a,V2f))) ) ) ) ) ) => ! [V6a0] : ( 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)) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2Eis__fmap__strongind,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0is__fmap_27] : ( mem(V0is__fmap_27,arr(arr(A_27a,ty_2Esum_2Esum(A_27b,ty_2Eone_2Eone)),bool)) => ( ( p(ap(V0is__fmap_27,k(A_27a,ap(c_2Esum_2EINR(A_27b,ty_2Eone_2Eone),c_2Eone_2Eone)))) & ! [V2f] : ( mem(V2f,arr(A_27a,ty_2Esum_2Esum(A_27b,ty_2Eone_2Eone))) => ! [V3a] : ( mem(V3a,A_27a) => ! [V4b] : ( 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,f1902(A_27b,A_27a,V4b,V3a,V2f))) ) ) ) ) ) => ! [V6a0] : ( 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)) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2Eis__fmap__cases,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0a0] : ( 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 = k(A_27a,ap(c_2Esum_2EINR(A_27b,ty_2Eone_2Eone),c_2Eone_2Eone)) ) | ? [V2f] : ( mem(V2f,arr(A_27a,ty_2Esum_2Esum(A_27b,ty_2Eone_2Eone))) & ? [V3a] : ( mem(V3a,A_27a) & ? [V4b] : ( mem(V4b,A_27b) & ( ( V0a0 = f1902(A_27b,A_27a,V4b,V3a,V2f) ) & p(ap(c_2Efinite__map_2Eis__fmap(A_27a,A_27b),V2f)) ) ) ) ) ) ) ))))).
fof(ax_thm_2Efinite__map_2Efmap__TY__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ? [V0rep] : ( 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)) ) ) ) )).
fof(ax_thm_2Efinite__map_2Efmap__ISO__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( ( ! [V0a] : ( 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] : ( 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 ) ) ) ) ) ) )).
fof(ax_thm_2Efinite__map_2EFUPDATE__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( 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),f1903(A_27b,A_27a,V2y,V1x,V0f)) ) ) ) ) ) ) )).
fof(ax_thm_2Efinite__map_2EFEMPTY__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( c_2Efinite__map_2EFEMPTY(A_27a,A_27b) = ap(c_2Efinite__map_2Efmap__ABS(A_27a,A_27b),k(A_27a,ap(c_2Esum_2EINR(A_27b,ty_2Eone_2Eone),c_2Eone_2Eone))) ) ) ) )).
fof(ax_thm_2Efinite__map_2EFAPPLY__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1x] : ( 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)) ) ) ) ) ) )).
fof(ax_thm_2Efinite__map_2EFDOM__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1x] : ( 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))) ) ) ) ) ) )).
fof(conj_thm_2Efinite__map_2EFAPPLY__FUPDATE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( 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 ) ) ) ))))).
fof(conj_thm_2Efinite__map_2ENOT__EQ__FAPPLY,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1a] : ( mem(V1a,A_27a) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( 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) ) ) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFUPDATE__COMMUTES,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1a] : ( mem(V1a,A_27a) => ! [V2b] : ( mem(V2b,A_27b) => ! [V3c] : ( mem(V3c,A_27a) => ! [V4d] : ( 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)) ) ) ) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFUPDATE__EQ,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1a] : ( mem(V1a,A_27a) => ! [V2b] : ( mem(V2b,A_27b) => ! [V3c] : ( 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)) ) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFDOM__FEMPTY,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),c_2Efinite__map_2EFEMPTY(A_27a,A_27b)) = c_2Epred__set_2EEMPTY(A_27a) ))))).
fof(conj_thm_2Efinite__map_2EFDOM__FUPDATE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1a] : ( mem(V1a,A_27a) => ! [V2b] : ( 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)) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFAPPLY__FUPDATE__THM,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1a] : ( mem(V1a,A_27a) => ! [V2b] : ( mem(V2b,A_27b) => ! [V3x] : ( 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)) ) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2ENOT__EQ__FEMPTY__FUPDATE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1a] : ( mem(V1a,A_27a) => ! [V2b] : ( 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)) ) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFDOM__EQ__FDOM__FUPDATE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1x] : ( mem(V1x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),V0f))) => ! [V2y] : ( 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) ) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2Efmap__SIMPLE__INDUCT,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(ty_2Efinite__map_2Efmap(A_27a,A_27b),bool)) => ( ( p(ap(V0P,c_2Efinite__map_2EFEMPTY(A_27a,A_27b))) & ! [V1f] : ( mem(V1f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( p(ap(V0P,V1f)) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( 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] : ( mem(V4f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => p(ap(V0P,V4f)) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFDOM__EQ__EMPTY,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( 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) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFDOM__EQ__EMPTY__SYM,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( 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) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFDOM__F__FEMPTY1,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ( ! [V1a] : ( 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) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFDOM__FINITE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0fm] : ( 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))) ))))).
fof(ax_thm_2Efinite__map_2EFCARD__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0fm] : ( mem(V0fm,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ap(c_2Efinite__map_2EFCARD(A_27a,A_27b),V0fm) = ap(c_2Epred__set_2ECARD(A_27a),ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),V0fm)) ) ) ) ) )).
fof(conj_thm_2Efinite__map_2EFCARD__FEMPTY,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ap(c_2Efinite__map_2EFCARD(A_27a,A_27b),c_2Efinite__map_2EFEMPTY(A_27a,A_27b)) = c_2Enum_2E0 ))))).
fof(conj_thm_2Efinite__map_2EFCARD__FUPDATE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0fm] : ( mem(V0fm,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1a] : ( mem(V1a,A_27a) => ! [V2b] : ( mem(V2b,A_27b) => ( 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))) = 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,c_2Earithmetic_2EZERO))),ap(c_2Efinite__map_2EFCARD(A_27a,A_27b),V0fm))) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFCARD__0__FEMPTY,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ( ap(c_2Efinite__map_2EFCARD(A_27a,A_27b),V0f) = c_2Enum_2E0 ) <=> ( V0f = c_2Efinite__map_2EFEMPTY(A_27a,A_27b) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFCARD__SUC,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ap(c_2Efinite__map_2EFCARD(A_27a,A_27b),V0f) = ap(c_2Enum_2ESUC,V1n) ) <=> ? [V2f_27] : ( mem(V2f_27,ty_2Efinite__map_2Efmap(A_27a,A_27b)) & ? [V3x] : ( mem(V3x,A_27a) & ? [V4y] : ( mem(V4y,A_27b) & ( ( ~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V3x),ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),V2f_27))) ) & ( ( 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)) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2Efmap__INDUCT,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(ty_2Efinite__map_2Efmap(A_27a,A_27b),bool)) => ( ( p(ap(V0P,c_2Efinite__map_2EFEMPTY(A_27a,A_27b))) & ! [V1f] : ( mem(V1f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( p(ap(V0P,V1f)) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( 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] : ( mem(V4f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => p(ap(V0P,V4f)) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFM__PULL__APART,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0fm] : ( mem(V0fm,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1k] : ( mem(V1k,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V1k),ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),V0fm))) => ? [V2fm0] : ( mem(V2fm0,ty_2Efinite__map_2Efmap(A_27a,A_27b)) & ? [V3v] : ( 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))) ) ) ) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2ENOT__FDOM__FAPPLY__FEMPTY,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1x] : ( 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) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2Efmap__EQ,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1g] : ( 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 ) ) ) ))))).
fof(conj_thm_2Efinite__map_2Efmap__EQ__THM,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1g] : ( 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] : ( 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 ) ) ) ))))).
fof(conj_thm_2Efinite__map_2Efmap__EXT,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1g] : ( 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] : ( 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) ) ) ) ) ) ) ))))).
fof(ax_thm_2Efinite__map_2ESUBMAP__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1g] : ( mem(V1g,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( p(ap(ap(c_2Efinite__map_2ESUBMAP(A_27a,A_27b),V0f),V1g)) <=> ! [V2x] : ( 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) ) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Efinite__map_2ESUBMAP__FEMPTY,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( 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)) ))))).
fof(conj_thm_2Efinite__map_2ESUBMAP__REFL,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => p(ap(ap(c_2Efinite__map_2ESUBMAP(A_27a,A_27b),V0f),V0f)) ))))).
fof(conj_thm_2Efinite__map_2ESUBMAP__ANTISYM,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1g] : ( 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 ) ) ) ))))).
fof(conj_thm_2Efinite__map_2ESUBMAP__TRANS,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1g] : ( mem(V1g,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V2h] : ( 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)) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2EEQ__FDOM__SUBMAP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1g] : ( 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) ) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2ESUBMAP__FUPDATE__EQN,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( 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))) ) ) ) ) ) ))))).
fof(ax_thm_2Efinite__map_2EDRESTRICT__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1r] : ( 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] : ( 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)) ) ) ) ) ) ) ) )).
fof(conj_thm_2Efinite__map_2EDRESTRICT__FEMPTY,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0r] : ( 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) ) ))))).
fof(conj_thm_2Efinite__map_2EDRESTRICT__FUPDATE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1r] : ( mem(V1r,arr(A_27a,bool)) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( 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)) ) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2ESTRONG__DRESTRICT__FUPDATE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1r] : ( mem(V1r,arr(A_27a,bool)) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( 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)) ) ) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFDOM__DRESTRICT,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1r] : ( mem(V1r,arr(A_27a,bool)) => ! [V2x] : ( 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) ) ) ) )))))).
fof(conj_thm_2Efinite__map_2ENOT__FDOM__DRESTRICT,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1x] : ( 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 ) ) ) ))))).
fof(conj_thm_2Efinite__map_2EDRESTRICT__SUBMAP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1r] : ( 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)) ) ))))).
fof(conj_thm_2Efinite__map_2EDRESTRICT__DRESTRICT,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1P] : ( mem(V1P,arr(A_27a,bool)) => ! [V2Q] : ( 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)) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2EDRESTRICT__IS__FEMPTY,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( 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) ) ))))).
fof(conj_thm_2Efinite__map_2EFUPDATE__DRESTRICT,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( 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)) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2ESTRONG__DRESTRICT__FUPDATE__THM,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1r] : ( mem(V1r,arr(A_27a,bool)) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( 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))) ) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2EDRESTRICT__UNIV,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( 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 ) ))))).
fof(conj_thm_2Efinite__map_2ESUBMAP__DRESTRICT,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1P] : ( 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)) ) ))))).
fof(conj_thm_2Efinite__map_2EDRESTRICT__EQ__DRESTRICT,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f1] : ( mem(V0f1,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1f2] : ( mem(V1f2,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V2s1] : ( mem(V2s1,arr(A_27a,bool)) => ! [V3s2] : ( 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)) ) ) ) ) ) ) ) ))))).
fof(ax_thm_2Efinite__map_2EFUNION__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1g] : ( 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] : ( 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)) ) ) ) ) ) ) ) )).
fof(conj_thm_2Efinite__map_2EFUNION__FEMPTY__1,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0g] : ( 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 ) ))))).
fof(conj_thm_2Efinite__map_2EFUNION__FEMPTY__2,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( 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 ) ))))).
fof(conj_thm_2Efinite__map_2EFUNION__FUPDATE__1,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1g] : ( mem(V1g,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( 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)) ) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFUNION__FUPDATE__2,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1g] : ( mem(V1g,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( 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))) ) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFDOM__FUNION,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1g] : ( mem(V1g,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V2x] : ( 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)) ) ) ) )))))).
fof(conj_thm_2Efinite__map_2EFUNION__IDEMPOT,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0fm] : ( mem(V0fm,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),V0fm),V0fm) = V0fm ) ))))).
fof(ax_thm_2Efinite__map_2EFMERGE__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0m] : ( mem(V0m,arr(A_27a,arr(A_27a,A_27a))) => ! [V1f] : ( mem(V1f,ty_2Efinite__map_2Efmap(A_27b,A_27a)) => ! [V2g] : ( 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] : ( 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)))) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Efinite__map_2EFMERGE__FEMPTY,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0m] : ( mem(V0m,arr(A_27b,arr(A_27b,A_27b))) => ! [V1f] : ( 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 ) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFDOM__FMERGE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0m] : ( mem(V0m,arr(A_27a,arr(A_27a,A_27a))) => ! [V1f] : ( mem(V1f,ty_2Efinite__map_2Efmap(A_27b,A_27a)) => ! [V2g] : ( 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)) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFMERGE__FUNION,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( c_2Efinite__map_2EFUNION(A_27a,A_27b) = ap(c_2Efinite__map_2EFMERGE(A_27b,A_27a),f1904(A_27b)) ))))).
fof(conj_thm_2Efinite__map_2EFUNION__FMERGE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f1] : ( mem(V0f1,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1f2] : ( mem(V1f2,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V2m] : ( 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) ) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFMERGE__NO__CHANGE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0m] : ( mem(V0m,arr(A_27b,arr(A_27b,A_27b))) => ! [V1f1] : ( mem(V1f1,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V2f2] : ( 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] : ( 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] : ( 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) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFMERGE__COMM,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0m] : ( 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)) ) ))))).
fof(conj_thm_2Efinite__map_2EFMERGE__ASSOC,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0m] : ( 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)) ) ))))).
fof(conj_thm_2Efinite__map_2EFMERGE__DRESTRICT,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27b,arr(A_27b,A_27b))) => ! [V1st1] : ( mem(V1st1,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V2st2] : ( mem(V2st2,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V3vs] : ( 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)) ) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFMERGE__EQ__FEMPTY,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0m] : ( mem(V0m,arr(A_27b,arr(A_27b,A_27b))) => ! [V1f] : ( mem(V1f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V2g] : ( 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) ) ) ) ) ) ))))).
fof(ax_thm_2Efinite__map_2EFLOOKUP__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1x] : ( 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)) ) ) ) ) ) )).
fof(conj_thm_2Efinite__map_2EFLOOKUP__EMPTY,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0k] : ( 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) ) ))))).
fof(conj_thm_2Efinite__map_2EFLOOKUP__UPDATE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0fm] : ( mem(V0fm,ty_2Efinite__map_2Efmap(A_27b,A_27a)) => ! [V1k1] : ( mem(V1k1,A_27b) => ! [V2v] : ( mem(V2v,A_27a) => ! [V3k2] : ( 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)) ) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFLOOKUP__SUBMAP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1g] : ( mem(V1g,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V2k] : ( mem(V2k,A_27a) => ! [V3v] : ( 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) ) ) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2ESUBMAP__FUPDATE__FLOOKUP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( 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) ) ) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFLOOKUP__FUNION,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f1] : ( mem(V0f1,ty_2Efinite__map_2Efmap(A_27b,A_27a)) => ! [V1f2] : ( mem(V1f2,ty_2Efinite__map_2Efmap(A_27b,A_27a)) => ! [V2k] : ( 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)),f1905(A_27a)) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFLOOKUP__EXT,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f1] : ( mem(V0f1,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1f2] : ( 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) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2Efmap__eq__flookup,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f1] : ( mem(V0f1,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1f2] : ( mem(V1f2,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ( V0f1 = V1f2 ) <=> ! [V2x] : ( 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) ) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFLOOKUP__DRESTRICT,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0fm] : ( mem(V0fm,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ! [V2k] : ( 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)) ) ) ) ))))).
fof(ax_thm_2Efinite__map_2EFEVERY__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ! [V1f] : ( mem(V1f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( p(ap(ap(c_2Efinite__map_2EFEVERY(A_27a,A_27b),V0P),V1f)) <=> ! [V2x] : ( 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)))) ) ) ) ) ) ) ) )).
fof(conj_thm_2Efinite__map_2EFEVERY__FEMPTY,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( 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))) ))))).
fof(conj_thm_2Efinite__map_2EFEVERY__FUPDATE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ! [V1f] : ( mem(V1f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( 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)))))) ) ) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFEVERY__FLOOKUP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ! [V1f] : ( mem(V1f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V2k] : ( mem(V2k,A_27a) => ! [V3v] : ( 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))) ) ) ) ) ))))).
fof(ax_thm_2Efinite__map_2Ef__o__f__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27b,A_27c)) => ! [V1g] : ( 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),f1906(A_27c,A_27b,A_27a,V0f,V1g))) ) & ! [V3x] : ( 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)) ) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Efinite__map_2Ef__o__f__FEMPTY__1,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0f] : ( 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) ) )))))).
fof(conj_thm_2Efinite__map_2Ef__o__f__FEMPTY__2,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0f] : ( 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) ) )))))).
fof(ax_thm_2Efinite__map_2Eo__f__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => ! [V0f] : ( mem(V0f,arr(A_27b,A_27c)) => ! [V1g] : ( 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] : ( 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)) ) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Efinite__map_2Eo__f__FDOM,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0f] : ( mem(V0f,arr(A_27b,A_27c)) => ! [V1g] : ( 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)) ) ) )))))).
fof(conj_thm_2Efinite__map_2EFDOM__o__f,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0f] : ( mem(V0f,arr(A_27b,A_27c)) => ! [V1g] : ( 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) ) ) )))))).
fof(conj_thm_2Efinite__map_2Eo__f__FAPPLY,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0f] : ( mem(V0f,arr(A_27b,A_27c)) => ! [V1g] : ( mem(V1g,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V2x] : ( 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)) ) ) ) ) )))))).
fof(conj_thm_2Efinite__map_2Eo__f__FEMPTY,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0f] : ( 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) ) )))))).
fof(conj_thm_2Efinite__map_2EFEVERY__o__f,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0m] : ( mem(V0m,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1P] : ( mem(V1P,arr(ty_2Epair_2Eprod(A_27a,A_27c),bool)) => ! [V2f] : ( 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),f1907(A_27b,A_27c,A_27a,V2f,V1P)),V0m)) ) ) ) )))))).
fof(conj_thm_2Efinite__map_2Eo__f__o__f,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) =>  ! [A_27d]: ( ne(A_27d) => ! [V0f] : ( mem(V0f,arr(A_27c,A_27b)) => ! [V1g] : ( mem(V1g,arr(A_27d,A_27c)) => ! [V2h] : ( 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) ) ) ) ))))))).
fof(conj_thm_2Efinite__map_2EFLOOKUP__o__f,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0f] : ( mem(V0f,arr(A_27c,A_27a)) => ! [V1fm] : ( mem(V1fm,ty_2Efinite__map_2Efmap(A_27b,A_27c)) => ! [V2k] : ( 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)),f1908(A_27c,A_27a,V0f)) ) ) ) )))))).
fof(ax_thm_2Efinite__map_2EFRANGE__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0f] : ( 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),f1910(A_27a,A_27b,V0f)) ) ) ) ) )).
fof(conj_thm_2Efinite__map_2EFRANGE__FEMPTY,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ap(c_2Efinite__map_2EFRANGE(A_27b,A_27a),c_2Efinite__map_2EFEMPTY(A_27b,A_27a)) = c_2Epred__set_2EEMPTY(A_27a) ))))).
fof(conj_thm_2Efinite__map_2EFRANGE__FUPDATE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( 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)))))) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2ESUBMAP__FRANGE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1g] : ( 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))) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFINITE__FRANGE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0fm] : ( 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))) ))))).
fof(conj_thm_2Efinite__map_2Eo__f__FRANGE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1g] : ( mem(V1g,ty_2Efinite__map_2Efmap(A_27b,A_27a)) => ! [V2f] : ( 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)))) ) ) ) )))))).
fof(conj_thm_2Efinite__map_2EFRANGE__FLOOKUP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0v] : ( mem(V0v,A_27a) => ! [V1f] : ( 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] : ( mem(V2k,A_27b) & ( ap(ap(c_2Efinite__map_2EFLOOKUP(A_27b,A_27a),V1f),V2k) = ap(c_2Eoption_2ESOME(A_27a),V0v) ) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFRANGE__FUNION,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0fm1] : ( mem(V0fm1,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1fm2] : ( 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)) ) ) ) ))))).
fof(ax_thm_2Efinite__map_2ERRESTRICT__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1r] : ( 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),f1911(A_27b,A_27a,V0f,V1r)) ) & ! [V3x] : ( 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)) ) ) ) ) ) ) ) )).
fof(conj_thm_2Efinite__map_2ERRESTRICT__FEMPTY,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0r] : ( 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) ) ))))).
fof(conj_thm_2Efinite__map_2ERRESTRICT__FUPDATE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1r] : ( mem(V1r,arr(A_27b,bool)) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( 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)) ) ) ) ) ))))).
fof(ax_thm_2Efinite__map_2EFUN__FMAP__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,A_27b)) => ! [V1P] : ( 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] : ( 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) ) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Efinite__map_2EFUN__FMAP__EMPTY,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( 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) ) ))))).
fof(conj_thm_2Efinite__map_2EFRANGE__FMAP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1f] : ( 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) ) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFDOM__FMAP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,A_27b)) => ! [V1s] : ( 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 ) ) ) ))))).
fof(conj_thm_2Efinite__map_2EFLOOKUP__FUN__FMAP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1f] : ( mem(V1f,arr(A_27a,A_27b)) => ! [V2k] : ( 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)) ) ) ) ) ))))).
fof(ax_thm_2Efinite__map_2Ef__o__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27b,A_27c)) => ! [V1g] : ( 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),f1912(A_27c,A_27b,A_27a,V0f,V1g)))) ) ) ) ) ) ) )).
fof(conj_thm_2Efinite__map_2EFDOM__f__o,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27b,A_27c)) => ! [V1g] : ( mem(V1g,arr(A_27a,A_27b)) => ( p(ap(c_2Epred__set_2EFINITE(A_27a),ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f1912(A_27c,A_27b,A_27a,V0f,V1g)))) => ( 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),f1913(A_27c,A_27b,A_27a,V0f,V1g)) ) ) ) )))))).
fof(conj_thm_2Efinite__map_2Ef__o__FEMPTY,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0g] : ( 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) ) )))))).
fof(conj_thm_2Efinite__map_2Ef__o__FUPDATE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0fm] : ( mem(V0fm,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1k] : ( mem(V1k,A_27a) => ! [V2v] : ( mem(V2v,A_27b) => ! [V3g] : ( mem(V3g,arr(A_27c,A_27a)) => ( ( p(ap(c_2Epred__set_2EFINITE(A_27c),ap(c_2Epred__set_2EGSPEC(A_27c,A_27c),f1914(A_27b,A_27a,A_27c,V0fm,V3g)))) & p(ap(c_2Epred__set_2EFINITE(A_27c),ap(c_2Epred__set_2EGSPEC(A_27c,A_27c),f1915(A_27a,A_27c,V1k,V3g)))) ) => ( 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),f1916(A_27a,A_27c,V1k,V3g)))) ) ) ) ) ) )))))).
fof(conj_thm_2Efinite__map_2EFAPPLY__f__o,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0f] : ( mem(V0f,ty_2Efinite__map_2Efmap(A_27b,A_27c)) => ! [V1g] : ( mem(V1g,arr(A_27a,A_27b)) => ( p(ap(c_2Epred__set_2EFINITE(A_27a),ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f1912(A_27c,A_27b,A_27a,V0f,V1g)))) => ! [V3x] : ( 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)) ) ) ) ) ) )))))).
fof(conj_thm_2Efinite__map_2EFINITE__PRED__11,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0g] : ( mem(V0g,arr(A_27a,A_27b)) => ( ( ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( mem(V2y,A_27a) => ( ( ap(V0g,V1x) = ap(V0g,V2y) ) <=> ( V1x = V2y ) ) ) ) ) => ! [V3f] : ( 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),f1917(A_27c,A_27b,A_27a,V3f,V0g)))) ) ) )))))).
fof(conj_thm_2Efinite__map_2Ef__o__ASSOC,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) =>  ! [A_27d]: ( ne(A_27d) => ! [V0g] : ( mem(V0g,arr(A_27a,A_27b)) => ! [V1h] : ( mem(V1h,arr(A_27c,A_27a)) => ! [V2f] : ( mem(V2f,ty_2Efinite__map_2Efmap(A_27b,A_27d)) => ( ( ( ! [V3x] : ( mem(V3x,A_27a) => ! [V4y] : ( mem(V4y,A_27a) => ( ( ap(V0g,V3x) = ap(V0g,V4y) ) <=> ( V3x = V4y ) ) ) ) ) & ! [V5x] : ( mem(V5x,A_27c) => ! [V6y] : ( 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)) ) ) ) ) ))))))).
fof(ax_thm_2Efinite__map_2Efmap__domsub,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0fm] : ( mem(V0fm,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1k] : ( 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)))) ) ) ) ) ) )).
fof(conj_thm_2Efinite__map_2EDOMSUB__FEMPTY,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0k] : ( 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) ) ))))).
fof(conj_thm_2Efinite__map_2EDOMSUB__FUPDATE,conjecture,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0fm] : ( mem(V0fm,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V1k] : ( mem(V1k,A_27a) => ! [V2v] : ( 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) ) ) ) ))))).
