include('Axioms/ASCIInumbers_2.ax').
tff(tp_ty_2Efinite__map_2Efmap,type,( ty_2Efinite__map_2Efmap: ( del * del ) > del )).
tff(tp_c_2Efinite__map_2EDRESTRICT,type,(c_2Efinite__map_2EDRESTRICT:(del * del) > $i)).
tff(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))))))).
tff(tp_c_2Efinite__map_2EFAPPLY,type,(c_2Efinite__map_2EFAPPLY:(del * del) > $i)).
tff(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)))))).
tff(tp_c_2Efinite__map_2EFCARD,type,(c_2Efinite__map_2EFCARD:(del * del) > $i)).
tff(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))))).
tff(tp_c_2Efinite__map_2EFDOM,type,(c_2Efinite__map_2EFDOM:(del * del) > $i)).
tff(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)))))).
tff(tp_c_2Efinite__map_2EFEMPTY,type,(c_2Efinite__map_2EFEMPTY:(del * del) > $i)).
tff(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))))).
tff(tp_c_2Efinite__map_2EFEVERY,type,(c_2Efinite__map_2EFEVERY:(del * del) > $i)).
tff(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)))))).
tff(tp_c_2Efinite__map_2EFLOOKUP,type,(c_2Efinite__map_2EFLOOKUP:(del * del) > $i)).
tff(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))))))).
tff(tp_c_2Efinite__map_2EFMAP__MAP2,type,(c_2Efinite__map_2EFMAP__MAP2:(del * del * del) > $i)).
tff(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)))))))).
tff(tp_c_2Efinite__map_2EFMERGE,type,(c_2Efinite__map_2EFMERGE:(del * del) > $i)).
tff(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)))))))).
tff(tp_c_2Efinite__map_2EFRANGE,type,(c_2Efinite__map_2EFRANGE:(del * del) > $i)).
tff(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)))))).
tff(tp_c_2Efinite__map_2EFUNION,type,(c_2Efinite__map_2EFUNION:(del * del) > $i)).
tff(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))))))).
tff(tp_c_2Efinite__map_2EFUN__FMAP,type,(c_2Efinite__map_2EFUN__FMAP:(del * del) > $i)).
tff(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))))))).
tff(tp_c_2Efinite__map_2EFUPDATE,type,(c_2Efinite__map_2EFUPDATE:(del * del) > $i)).
tff(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))))))).
tff(tp_c_2Efinite__map_2EFUPDATE__LIST,type,(c_2Efinite__map_2EFUPDATE__LIST:(del * del) > $i)).
tff(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))))))).
tff(tp_c_2Efinite__map_2EMAP__KEYS,type,(c_2Efinite__map_2EMAP__KEYS:(del * del * del) > $i)).
tff(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)))))))).
tff(tp_c_2Efinite__map_2ERRESTRICT,type,(c_2Efinite__map_2ERRESTRICT:(del * del) > $i)).
tff(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))))))).
tff(tp_c_2Efinite__map_2ESUBMAP,type,(c_2Efinite__map_2ESUBMAP:(del * del) > $i)).
tff(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)))))).
tff(tp_c_2Efinite__map_2Ef__o,type,(c_2Efinite__map_2Ef__o:(del * del * del) > $i)).
tff(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)))))))).
tff(tp_c_2Efinite__map_2Ef__o__f,type,(c_2Efinite__map_2Ef__o__f:(del * del * del) > $i)).
tff(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)))))))).
tff(tp_c_2Efinite__map_2Efdomsub,type,(c_2Efinite__map_2Efdomsub:(del * del) > $i)).
tff(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))))))).
tff(tp_c_2Efinite__map_2Efmap__ABS,type,(c_2Efinite__map_2Efmap__ABS:(del * del) > $i)).
tff(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)))))).
tff(tp_c_2Efinite__map_2Efmap__EQ__UPTO,type,(c_2Efinite__map_2Efmap__EQ__UPTO:(del * del) > $i)).
tff(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))))))).
tff(tp_c_2Efinite__map_2Efmap__REP,type,(c_2Efinite__map_2Efmap__REP:(del * del) > $i)).
tff(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))))))).
tff(tp_c_2Efinite__map_2Efmap__inverse,type,(c_2Efinite__map_2Efmap__inverse:(del * del) > $i)).
tff(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)))))).
tff(tp_c_2Efinite__map_2Efmap__rel,type,(c_2Efinite__map_2Efmap__rel:(del * del * del) > $i)).
tff(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)))))))).
tff(tp_c_2Efinite__map_2Efmap__size,type,(c_2Efinite__map_2Efmap__size:(del * del) > $i)).
tff(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))))))).
tff(tp_c_2Efinite__map_2Eis__fmap,type,(c_2Efinite__map_2Eis__fmap:(del * del) > $i)).
tff(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))))).
tff(tp_c_2Efinite__map_2Eo__f,type,(c_2Efinite__map_2Eo__f:(del * del * del) > $i)).
tff(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)))))))).
tff(ax_thm_2Efinite__map_2Eis__fmap__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (c_2Efinite__map_2Eis__fmap(A_27a,A_27b) = f1900(A_27a,A_27b))))).
tff(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),k(A_27a,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),f1901(A_27b,A_27a,V3b,V2a,V1f))))))))))))))).
tff(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,k(A_27a,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,f1902(A_27b,A_27a,V4b,V3a,V2f))))))))))) => ( ! [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)))))))))))).
tff(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,k(A_27a,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,f1902(A_27b,A_27a,V4b,V3a,V2f))))))))))) => ( ! [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)))))))))))).
tff(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 = k(A_27a,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 = f1902(A_27b,A_27a,V4b,V3a,V2f)) & p(ap(c_2Efinite__map_2Eis__fmap(A_27a,A_27b),V2f))))))))))))))))).
tff(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))))))).
tff(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)))))))).
tff(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),f1903(A_27b,A_27a,V2y,V1x,V0f)))))))))))).
tff(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),k(A_27a,ap(c_2Esum_2EINR(A_27b,ty_2Eone_2Eone),inj__ty_2Eone_2Eone(fo__c_2Eone_2Eone)))))))).
tff(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)))))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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))))))))))))))).
tff(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)))))))))))))))))).
tff(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))))))))))))))).
tff(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)))))).
tff(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))))))))))))).
tff(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))))))))))))))).
tff(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)))))))))))))).
tff(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))))))))))))).
tff(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))))))))))).
tff(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))))))))).
tff(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))))))))).
tff(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))))))))).
tff(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))))))))).
tff(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))))))))).
tff(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))))).
tff(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))))))))))))))).
tff(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))))))))).
tff(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))))))))))))))))))).
tff(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))))))))))).
tff(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)))))))))))))))))).
tff(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))))))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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))))))))))))))).
tff(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)))))))))))))).
tff(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)))))))).
tff(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)))))))).
tff(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)))))))))).
tff(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))))))))))))).
tff(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)))))))))))).
tff(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)))))))))))))))).
tff(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))))))))))))).
tff(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)))))))).
tff(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))))))))))))))).
tff(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)))))))))))))))).
tff(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))))))))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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))))))))))))).
tff(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)))))))).
tff(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))))))))))))).
tff(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)))))))))))))))).
tff(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))))))).
tff(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)))))))))).
tff(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)))))))))))))))))).
tff(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))))))))))))).
tff(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))))))).
tff(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))))))).
tff(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))))))))))))))).
tff(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)))))))))))))))).
tff(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)))))))))))))).
tff(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))))))).
tff(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))))))))))))))))).
tff(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)))))))))).
tff(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))))))))))))).
tff(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),f1904(A_27b))))))).
tff(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))))))))))))).
tff(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)))))))))))))))))).
tff(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))))))))).
tff(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))))))))).
tff(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))))))))))))))).
tff(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)))))))))))))).
tff(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)))))))))).
tff(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)))))))).
tff(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))))))))))))))).
tff(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))))))))))))))).
tff(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)))))))))))))).
tff(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)),f1905(A_27a))))))))))))).
tff(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))))))))))).
tff(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))))))))))))).
tff(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))))))))))))).
tff(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))))))))))))))).
tff(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))))))))).
tff(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)))))))))))))))))))).
tff(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)))))))))))))))).
tff(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),f1906(A_27c,A_27b,A_27a,V0f,V1g)))) & ( ! [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))))))))))))))).
tff(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))))))))).
tff(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))))))))).
tff(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))))))))))))))).
tff(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)))))))))))).
tff(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))))))))))).
tff(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))))))))))))))).
tff(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))))))))).
tff(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),f1907(A_27b,A_27c,A_27a,V2f,V1P)),V0m)))))))))))))).
tff(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)))))))))))))).
tff(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)),f1908(A_27c,A_27a,V0f)))))))))))))).
tff(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),f1910(A_27a,A_27b,V0f)))))))).
tff(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)))))).
tff(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))))))))))))))))).
tff(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)))))))))))).
tff(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))))))))).
tff(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)))))))))))))))).
tff(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))))))))))))).
tff(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)))))))))))).
tff(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),f1911(A_27b,A_27a,V0f,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))))))))))))).
tff(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)))))))).
tff(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))))))))))))))).
tff(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)))))))))))))).
tff(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)))))))).
tff(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))))))))))).
tff(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)))))))))).
tff(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)))))))))))))).
tff(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),f1912(A_27c,A_27b,A_27a,V0f,V1g))))))))))))).
tff(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),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))))))))))))).
tff(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))))))))).
tff(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),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))))))))))))))))))).
tff(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),f1912(A_27c,A_27b,A_27a,V0f,V1g)))) => ( ! [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)))))))))))))))).
tff(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),f1917(A_27c,A_27b,A_27a,V3f,V0g)))))))))))))).
tff(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)))))))))))))))).
tff(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)))))))))))).
tff(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)))))))).
tff(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)))))))))))).
tff(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)))))))))))))))).
tff(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)))))))))))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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))))))))))))).
tff(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))))))))))))).
tff(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)))))))))).
tff(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))))))))))))).
tff(conj_thm_2Efinite__map_2EDOMSUB__FLOOKUP__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_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))))))))))))).
tff(conj_thm_2Efinite__map_2EFRANGE__FUPDATE__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) => ( ! [V2v:$i] : (mem(V2v,A_27b) => (ap(c_2Efinite__map_2EFRANGE(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))) = ap(ap(c_2Epred__set_2EINSERT(A_27b),V2v),ap(c_2Efinite__map_2EFRANGE(A_27a,A_27b),ap(ap(c_2Efinite__map_2Efdomsub(A_27a,A_27b),V0fm),V1k)))))))))))))).
tff(conj_thm_2Efinite__map_2Eo__f__DOMSUB,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0g:$i] : (mem(V0g,arr(A_27c,A_27b)) => ( ! [V1fm:$i] : (mem(V1fm,ty_2Efinite__map_2Efmap(A_27a,A_27c)) => ( ! [V2k:$i] : (mem(V2k,A_27a) => (ap(ap(c_2Efinite__map_2Efdomsub(A_27a,A_27b),ap(ap(c_2Efinite__map_2Eo__f(A_27a,A_27c,A_27b),V0g),V1fm)),V2k) = ap(ap(c_2Efinite__map_2Eo__f(A_27a,A_27c,A_27b),V0g),ap(ap(c_2Efinite__map_2Efdomsub(A_27a,A_27c),V1fm),V2k)))))))))))))).
tff(conj_thm_2Efinite__map_2EDOMSUB__IDEM,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_2Efdomsub(A_27a,A_27b),ap(ap(c_2Efinite__map_2Efdomsub(A_27a,A_27b),V0fm),V1k)),V1k) = ap(ap(c_2Efinite__map_2Efdomsub(A_27a,A_27b),V0fm),V1k)))))))))).
tff(conj_thm_2Efinite__map_2EDOMSUB__COMMUTES,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_2Efdomsub(A_27a,A_27b),ap(ap(c_2Efinite__map_2Efdomsub(A_27a,A_27b),V0fm),V1k1)),V2k2) = ap(ap(c_2Efinite__map_2Efdomsub(A_27a,A_27b),ap(ap(c_2Efinite__map_2Efdomsub(A_27a,A_27b),V0fm),V2k2)),V1k1)))))))))))).
tff(conj_thm_2Efinite__map_2Eo__f__FUPDATE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27c,A_27b)) => ( ! [V1fm:$i] : (mem(V1fm,ty_2Efinite__map_2Efmap(A_27a,A_27c)) => ( ! [V2k:$i] : (mem(V2k,A_27a) => ( ! [V3v:$i] : (mem(V3v,A_27c) => (ap(ap(c_2Efinite__map_2Eo__f(A_27a,A_27c,A_27b),V0f),ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27c),V1fm),ap(ap(c_2Epair_2E_2C(A_27a,A_27c),V2k),V3v))) = ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),ap(ap(c_2Efinite__map_2Eo__f(A_27a,A_27c,A_27b),V0f),V1fm)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2k),ap(V0f,V3v))))))))))))))))).
tff(conj_thm_2Efinite__map_2EDOMSUB__NOT__IN__DOM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0k:$i] : (mem(V0k,A_27a) => ( ! [V1fm:$i] : (mem(V1fm,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ((~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V0k),ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),V1fm)))) => (ap(ap(c_2Efinite__map_2Efdomsub(A_27a,A_27b),V1fm),V0k) = V1fm)))))))))).
tff(conj_thm_2Efinite__map_2Efmap__CASES,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ((V0f = c_2Efinite__map_2EFEMPTY(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) & (V0f = ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),V1g),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2x),V3y)))))))))))))))).
tff(conj_thm_2Efinite__map_2ESUBMAP__DOMSUB,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ! [V1k:$i] : (mem(V1k,A_27a) => p(ap(ap(c_2Efinite__map_2ESUBMAP(A_27a,A_27b),ap(ap(c_2Efinite__map_2Efdomsub(A_27a,A_27b),V0f),V1k)),V0f)))))))))).
tff(conj_thm_2Efinite__map_2EFMERGE__DOMSUB,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0m:$i] : (mem(V0m,arr(A_27a,arr(A_27a,A_27a))) => ( ! [V1m1:$i] : (mem(V1m1,ty_2Efinite__map_2Efmap(A_27b,A_27a)) => ( ! [V2m2:$i] : (mem(V2m2,ty_2Efinite__map_2Efmap(A_27b,A_27a)) => ( ! [V3k:$i] : (mem(V3k,A_27b) => (ap(ap(c_2Efinite__map_2Efdomsub(A_27b,A_27a),ap(ap(ap(c_2Efinite__map_2EFMERGE(A_27a,A_27b),V0m),V1m1),V2m2)),V3k) = ap(ap(ap(c_2Efinite__map_2EFMERGE(A_27a,A_27b),V0m),ap(ap(c_2Efinite__map_2Efdomsub(A_27b,A_27a),V1m1),V3k)),ap(ap(c_2Efinite__map_2Efdomsub(A_27b,A_27a),V2m2),V3k))))))))))))))).
tff(conj_thm_2Efinite__map_2ESUBMAP__FUPDATE,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) => (p(ap(ap(c_2Efinite__map_2ESUBMAP(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)) <=> (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),V1g),V2x) = V3y) & p(ap(ap(c_2Efinite__map_2ESUBMAP(A_27a,A_27b),ap(ap(c_2Efinite__map_2Efdomsub(A_27a,A_27b),V0f),V2x)),ap(ap(c_2Efinite__map_2Efdomsub(A_27a,A_27b),V1g),V2x)))))))))))))))))).
tff(ax_thm_2Efinite__map_2EFUPDATE__LIST,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (c_2Efinite__map_2EFUPDATE__LIST(A_27a,A_27b) = ap(c_2Elist_2EFOLDL(ty_2Epair_2Eprod(A_27a,A_27b),ty_2Efinite__map_2Efmap(A_27a,A_27b)),c_2Efinite__map_2EFUPDATE(A_27a,A_27b)))))).
tff(conj_thm_2Efinite__map_2EFUPDATE__LIST__THM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ((ap(ap(c_2Efinite__map_2EFUPDATE__LIST(A_27a,A_27b),V0f),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))) = V0f) & ( ! [V1h:$i] : (mem(V1h,ty_2Epair_2Eprod(A_27a,A_27b)) => ( ! [V2t:$i] : (mem(V2t,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => (ap(ap(c_2Efinite__map_2EFUPDATE__LIST(A_27a,A_27b),V0f),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),V1h),V2t)) = ap(ap(c_2Efinite__map_2EFUPDATE__LIST(A_27a,A_27b),ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),V0f),V1h)),V2t))))))))))))).
tff(conj_thm_2Efinite__map_2EFUPDATE__LIST__APPLY__NOT__MEM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0kvl:$i] : (mem(V0kvl,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V1f:$i] : (mem(V1f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ! [V2k:$i] : (mem(V2k,A_27a) => ((~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V2k),ap(c_2Elist_2ELIST__TO__SET(A_27a),ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27a),c_2Epair_2EFST(A_27a,A_27b)),V0kvl))))) => (ap(ap(c_2Efinite__map_2EFAPPLY(A_27a,A_27b),ap(ap(c_2Efinite__map_2EFUPDATE__LIST(A_27a,A_27b),V1f),V0kvl)),V2k) = ap(ap(c_2Efinite__map_2EFAPPLY(A_27a,A_27b),V1f),V2k))))))))))))).
tff(conj_thm_2Efinite__map_2EFUPDATE__LIST__APPEND,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0fm:$i] : (mem(V0fm,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ! [V1kvl1:$i] : (mem(V1kvl1,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V2kvl2:$i] : (mem(V2kvl2,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => (ap(ap(c_2Efinite__map_2EFUPDATE__LIST(A_27a,A_27b),V0fm),ap(ap(c_2Elist_2EAPPEND(ty_2Epair_2Eprod(A_27a,A_27b)),V1kvl1),V2kvl2)) = ap(ap(c_2Efinite__map_2EFUPDATE__LIST(A_27a,A_27b),ap(ap(c_2Efinite__map_2EFUPDATE__LIST(A_27a,A_27b),V0fm),V1kvl1)),V2kvl2)))))))))))).
tff(conj_thm_2Efinite__map_2EFUPDATE__FUPDATE__LIST__COMMUTES,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0k:$i] : (mem(V0k,A_27a) => ( ! [V1kvl:$i] : (mem(V1kvl,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V2fm:$i] : (mem(V2fm,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ! [V3v:$i] : (mem(V3v,A_27b) => ((~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V0k),ap(c_2Elist_2ELIST__TO__SET(A_27a),ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27a),c_2Epair_2EFST(A_27a,A_27b)),V1kvl))))) => (ap(ap(c_2Efinite__map_2EFUPDATE__LIST(A_27a,A_27b),ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),V2fm),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V0k),V3v))),V1kvl) = ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),ap(ap(c_2Efinite__map_2EFUPDATE__LIST(A_27a,A_27b),V2fm),V1kvl)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V0k),V3v)))))))))))))))).
tff(conj_thm_2Efinite__map_2EFUPDATE__FUPDATE__LIST__MEM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0k:$i] : (mem(V0k,A_27a) => ( ! [V1kvl:$i] : (mem(V1kvl,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V2fm:$i] : (mem(V2fm,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ! [V3v:$i] : (mem(V3v,A_27b) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V0k),ap(c_2Elist_2ELIST__TO__SET(A_27a),ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27a),c_2Epair_2EFST(A_27a,A_27b)),V1kvl)))) => (ap(ap(c_2Efinite__map_2EFUPDATE__LIST(A_27a,A_27b),ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),V2fm),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V0k),V3v))),V1kvl) = ap(ap(c_2Efinite__map_2EFUPDATE__LIST(A_27a,A_27b),V2fm),V1kvl))))))))))))))).
tff(conj_thm_2Efinite__map_2EFEVERY__FUPDATE__LIST,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0kvl:$i] : (mem(V0kvl,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V1P:$i] : (mem(V1P,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ! [V2fm:$i] : (mem(V2fm,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => (p(ap(c_2Elist_2EALL__DISTINCT(A_27a),ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27a),c_2Epair_2EFST(A_27a,A_27b)),V0kvl))) => (p(ap(ap(c_2Efinite__map_2EFEVERY(A_27a,A_27b),V1P),ap(ap(c_2Efinite__map_2EFUPDATE__LIST(A_27a,A_27b),V2fm),V0kvl))) <=> (p(ap(ap(c_2Elist_2EEVERY(ty_2Epair_2Eprod(A_27a,A_27b)),V1P),V0kvl)) & p(ap(ap(c_2Efinite__map_2EFEVERY(A_27a,A_27b),V1P),ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),V2fm),ap(c_2Epred__set_2ECOMPL(A_27a),ap(c_2Elist_2ELIST__TO__SET(A_27a),ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27a),c_2Epair_2EFST(A_27a,A_27b)),V0kvl))))))))))))))))))).
tff(conj_thm_2Efinite__map_2EFUPDATE__LIST__APPLY__MEM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0kvl:$i] : (mem(V0kvl,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V1f:$i] : (mem(V1f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ! [V2k:$i] : (mem(V2k,A_27a) => ( ! [V3v:$i] : (mem(V3v,A_27b) => ( ! [V4n:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V4n)),ap(c_2Elist_2ELENGTH(ty_2Epair_2Eprod(A_27a,A_27b)),V0kvl))) & ((V2k = ap(ap(c_2Elist_2EEL(A_27a),inj__ty_2Enum_2Enum(V4n)),ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27a),c_2Epair_2EFST(A_27a,A_27b)),V0kvl))) & ((V3v = ap(ap(c_2Elist_2EEL(A_27b),inj__ty_2Enum_2Enum(V4n)),ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27b),c_2Epair_2ESND(A_27a,A_27b)),V0kvl))) & ( ! [V5m:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V4n)),inj__ty_2Enum_2Enum(V5m))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V5m)),ap(c_2Elist_2ELENGTH(ty_2Epair_2Eprod(A_27a,A_27b)),V0kvl)))) => (~~ (ap(ap(c_2Elist_2EEL(A_27a),inj__ty_2Enum_2Enum(V5m)),ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27a),c_2Epair_2EFST(A_27a,A_27b)),V0kvl)) = V2k))))))) => (ap(ap(c_2Efinite__map_2EFAPPLY(A_27a,A_27b),ap(ap(c_2Efinite__map_2EFUPDATE__LIST(A_27a,A_27b),V1f),V0kvl)),V2k) = V3v))))))))))))))).
tff(conj_thm_2Efinite__map_2EFOLDL__FUPDATE__LIST,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f1:$i] : (mem(V0f1,arr(A_27a,A_27b)) => ( ! [V1f2:$i] : (mem(V1f2,arr(A_27a,A_27c)) => ( ! [V2ls:$i] : (mem(V2ls,ty_2Elist_2Elist(A_27a)) => ( ! [V3a:$i] : (mem(V3a,ty_2Efinite__map_2Efmap(A_27b,A_27c)) => (ap(ap(ap(c_2Elist_2EFOLDL(A_27a,ty_2Efinite__map_2Efmap(A_27b,A_27c)),f1919(A_27a,A_27b,A_27c,V1f2,V0f1)),V3a),V2ls) = ap(ap(c_2Efinite__map_2EFUPDATE__LIST(A_27b,A_27c),V3a),ap(ap(c_2Elist_2EMAP(A_27a,ty_2Epair_2Eprod(A_27b,A_27c)),f1920(A_27b,A_27c,A_27a,V0f1,V1f2)),V2ls)))))))))))))))).
tff(conj_thm_2Efinite__map_2EFUPDATE__LIST__SNOC,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0xs:$i] : (mem(V0xs,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V1x:$i] : (mem(V1x,ty_2Epair_2Eprod(A_27a,A_27b)) => ( ! [V2fm:$i] : (mem(V2fm,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => (ap(ap(c_2Efinite__map_2EFUPDATE__LIST(A_27a,A_27b),V2fm),ap(ap(c_2Elist_2ESNOC(ty_2Epair_2Eprod(A_27a,A_27b)),V1x),V0xs)) = ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),ap(ap(c_2Efinite__map_2EFUPDATE__LIST(A_27a,A_27b),V2fm),V0xs)),V1x)))))))))))).
tff(conj_thm_2Efinite__map_2EFUPD11__SAME__KEY__AND__BASE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ! [V1k:$i] : (mem(V1k,A_27a) => ( ! [V2v1:$i] : (mem(V2v1,A_27b) => ( ! [V3v2:$i] : (mem(V3v2,A_27b) => ((ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),V0f),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V1k),V2v1)) = ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),V0f),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V1k),V3v2))) <=> (V2v1 = V3v2)))))))))))))).
tff(conj_thm_2Efinite__map_2EFUPD11__SAME__NEW__KEY,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)) => ( ! [V2k:$i] : (mem(V2k,A_27a) => ( ! [V3v1:$i] : (mem(V3v1,A_27b) => ( ! [V4v2:$i] : (mem(V4v2,A_27b) => (((~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V2k),ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),V0f1)))) & (~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V2k),ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),V1f2))))) => ((ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),V0f1),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2k),V3v1)) = ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),V1f2),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2k),V4v2))) <=> ((V0f1 = V1f2) & (V3v1 = V4v2)))))))))))))))))).
tff(conj_thm_2Efinite__map_2ESAME__KEY__UPDATES__DIFFER,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)) => ( ! [V2k:$i] : (mem(V2k,A_27a) => ( ! [V3v1:$i] : (mem(V3v1,A_27b) => ( ! [V4v2:$i] : (mem(V4v2,A_27b) => ((~~ (V3v1 = V4v2)) => (~~ (ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),V0f1),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2k),V3v1)) = ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),V1f2),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2k),V4v2))))))))))))))))))).
tff(conj_thm_2Efinite__map_2EFUPD11__SAME__BASE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ! [V1k1:$i] : (mem(V1k1,A_27a) => ( ! [V2v1:$i] : (mem(V2v1,A_27b) => ( ! [V3k2:$i] : (mem(V3k2,A_27a) => ( ! [V4v2:$i] : (mem(V4v2,A_27b) => ((ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),V0f),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V1k1),V2v1)) = ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),V0f),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V3k2),V4v2))) <=> (((V1k1 = V3k2) & (V2v1 = V4v2)) | ((~~ (V1k1 = V3k2)) & (p(ap(ap(c_2Ebool_2EIN(A_27a),V1k1),ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),V0f))) & (p(ap(ap(c_2Ebool_2EIN(A_27a),V3k2),ap(c_2Efinite__map_2EFDOM(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),V1k1),V2v1)) = V0f) & (ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),V0f),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V3k2),V4v2)) = V0f))))))))))))))))))))).
tff(conj_thm_2Efinite__map_2EFUPD__SAME__KEY__UNWIND,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)) => ( ! [V2k:$i] : (mem(V2k,A_27a) => ( ! [V3v1:$i] : (mem(V3v1,A_27b) => ( ! [V4v2:$i] : (mem(V4v2,A_27b) => ((ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),V0f1),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2k),V3v1)) = ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),V1f2),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2k),V4v2))) => ((V3v1 = V4v2) & ( ! [V5v:$i] : (mem(V5v,A_27b) => (ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),V0f1),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2k),V5v)) = ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),V1f2),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2k),V5v))))))))))))))))))))).
tff(conj_thm_2Efinite__map_2EFUPD11__SAME__UPDATE,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)) => ( ! [V2k:$i] : (mem(V2k,A_27a) => ( ! [V3v:$i] : (mem(V3v,A_27b) => ((ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),V0f1),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2k),V3v)) = ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),V1f2),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2k),V3v))) <=> (ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),V0f1),ap(c_2Epred__set_2ECOMPL(A_27a),ap(ap(c_2Epred__set_2EINSERT(A_27a),V2k),c_2Epred__set_2EEMPTY(A_27a)))) = ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),V1f2),ap(c_2Epred__set_2ECOMPL(A_27a),ap(ap(c_2Epred__set_2EINSERT(A_27a),V2k),c_2Epred__set_2EEMPTY(A_27a)))))))))))))))))).
tff(conj_thm_2Efinite__map_2EFDOM__FUPDATE__LIST,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0kvl:$i] : (mem(V0kvl,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V1fm:$i] : (mem(V1fm,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => (ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),ap(ap(c_2Efinite__map_2EFUPDATE__LIST(A_27a,A_27b),V1fm),V0kvl)) = ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),V1fm)),ap(c_2Elist_2ELIST__TO__SET(A_27a),ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27a),c_2Epair_2EFST(A_27a,A_27b)),V0kvl)))))))))))).
tff(conj_thm_2Efinite__map_2EFUPDATE__LIST__SAME__UPDATE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0kvl:$i] : (mem(V0kvl,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,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(c_2Efinite__map_2EFUPDATE__LIST(A_27a,A_27b),V1f1),V0kvl) = ap(ap(c_2Efinite__map_2EFUPDATE__LIST(A_27a,A_27b),V2f2),V0kvl)) <=> (ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),V1f1),ap(c_2Epred__set_2ECOMPL(A_27a),ap(c_2Elist_2ELIST__TO__SET(A_27a),ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27a),c_2Epair_2EFST(A_27a,A_27b)),V0kvl)))) = ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),V2f2),ap(c_2Epred__set_2ECOMPL(A_27a),ap(c_2Elist_2ELIST__TO__SET(A_27a),ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27a),c_2Epair_2EFST(A_27a,A_27b)),V0kvl)))))))))))))))).
tff(conj_thm_2Efinite__map_2EFUPDATE__LIST__SAME__KEYS__UNWIND,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)) => ( ! [V2kvl1:$i] : (mem(V2kvl1,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V3kvl2:$i] : (mem(V3kvl2,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => (((ap(ap(c_2Efinite__map_2EFUPDATE__LIST(A_27a,A_27b),V0f1),V2kvl1) = ap(ap(c_2Efinite__map_2EFUPDATE__LIST(A_27a,A_27b),V1f2),V3kvl2)) & ((ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27a),c_2Epair_2EFST(A_27a,A_27b)),V2kvl1) = ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27a),c_2Epair_2EFST(A_27a,A_27b)),V3kvl2)) & p(ap(c_2Elist_2EALL__DISTINCT(A_27a),ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27a),c_2Epair_2EFST(A_27a,A_27b)),V2kvl1))))) => ((V2kvl1 = V3kvl2) & ( ! [V4kvl:$i] : (mem(V4kvl,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ((ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27a),c_2Epair_2EFST(A_27a,A_27b)),V4kvl) = ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27a),c_2Epair_2EFST(A_27a,A_27b)),V2kvl1)) => (ap(ap(c_2Efinite__map_2EFUPDATE__LIST(A_27a,A_27b),V0f1),V4kvl) = ap(ap(c_2Efinite__map_2EFUPDATE__LIST(A_27a,A_27b),V1f2),V4kvl))))))))))))))))))).
tff(conj_thm_2Efinite__map_2EFMEQ__ENUMERATE__CASES,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f1:$i] : (mem(V0f1,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ! [V1kvl:$i] : (mem(V1kvl,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V2p:$i] : (mem(V2p,ty_2Epair_2Eprod(A_27a,A_27b)) => ((ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),V0f1),V2p) = ap(ap(c_2Efinite__map_2EFUPDATE__LIST(A_27a,A_27b),c_2Efinite__map_2EFEMPTY(A_27a,A_27b)),V1kvl)) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27b)),V2p),ap(c_2Elist_2ELIST__TO__SET(ty_2Epair_2Eprod(A_27a,A_27b)),V1kvl)))))))))))))).
tff(conj_thm_2Efinite__map_2EFMEQ__SINGLE__SIMPLE__ELIM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Efinite__map_2Efmap(A_27a,A_27b),bool)) => ( ! [V1k:$i] : (mem(V1k,A_27a) => ( ! [V2v:$i] : (mem(V2v,A_27b) => ( ! [V3ck:$i] : (mem(V3ck,A_27a) => ( ! [V4cv:$i] : (mem(V4cv,A_27b) => ( ! [V5nv:$i] : (mem(V5nv,A_27b) => ((? [V6fm:$i] : (mem(V6fm,ty_2Efinite__map_2Efmap(A_27a,A_27b)) & ((ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),V6fm),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V1k),V2v)) = ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),c_2Efinite__map_2EFEMPTY(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V3ck),V4cv))) & p(ap(V0P,ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),V6fm),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V1k),V5nv))))))) <=> ((V1k = V3ck) & ((V2v = V4cv) & p(ap(V0P,ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),c_2Efinite__map_2EFEMPTY(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V3ck),V5nv))))))))))))))))))))))).
tff(conj_thm_2Efinite__map_2EFMEQ__SINGLE__SIMPLE__DISJ__ELIM,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) => ( ! [V3ck:$i] : (mem(V3ck,A_27a) => ( ! [V4cv:$i] : (mem(V4cv,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)) = ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),c_2Efinite__map_2EFEMPTY(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V3ck),V4cv))) <=> ((V1k = V3ck) & ((V2v = V4cv) & ((V0fm = c_2Efinite__map_2EFEMPTY(A_27a,A_27b)) | (? [V5v_27:$i] : (mem(V5v_27,A_27b) & (V0fm = ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),c_2Efinite__map_2EFEMPTY(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V1k),V5v_27))))))))))))))))))))))).
tff(conj_thm_2Efinite__map_2EFUPDATE__PURGE,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_2Efdomsub(A_27a,A_27b),V0f),V1x)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V1x),V2y))))))))))))).
tff(ax_thm_2Efinite__map_2EFMAP__MAP2__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(ty_2Epair_2Eprod(A_27a,A_27c),A_27b)) => ( ! [V1m:$i] : (mem(V1m,ty_2Efinite__map_2Efmap(A_27a,A_27c)) => (ap(ap(c_2Efinite__map_2EFMAP__MAP2(A_27a,A_27b,A_27c),V0f),V1m) = ap(ap(c_2Efinite__map_2EFUN__FMAP(A_27a,A_27b),f1921(A_27b,A_27c,A_27a,V1m,V0f)),ap(c_2Efinite__map_2EFDOM(A_27a,A_27c),V1m))))))))))).
tff(conj_thm_2Efinite__map_2EFMAP__MAP2__THM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(ty_2Epair_2Eprod(A_27a,A_27c),A_27b)) => ( ! [V1m:$i] : (mem(V1m,ty_2Efinite__map_2Efmap(A_27a,A_27c)) => ((ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),ap(ap(c_2Efinite__map_2EFMAP__MAP2(A_27a,A_27b,A_27c),V0f),V1m)) = ap(c_2Efinite__map_2EFDOM(A_27a,A_27c),V1m)) & ( ! [V2x:$i] : (mem(V2x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),ap(c_2Efinite__map_2EFDOM(A_27a,A_27c),V1m))) => (ap(ap(c_2Efinite__map_2EFAPPLY(A_27a,A_27b),ap(ap(c_2Efinite__map_2EFMAP__MAP2(A_27a,A_27b,A_27c),V0f),V1m)),V2x) = ap(V0f,ap(ap(c_2Epair_2E_2C(A_27a,A_27c),V2x),ap(ap(c_2Efinite__map_2EFAPPLY(A_27a,A_27c),V1m),V2x))))))))))))))))).
tff(conj_thm_2Efinite__map_2EFMAP__MAP2__FEMPTY,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(ty_2Epair_2Eprod(A_27a,A_27c),A_27b)) => (ap(ap(c_2Efinite__map_2EFMAP__MAP2(A_27a,A_27b,A_27c),V0f),c_2Efinite__map_2EFEMPTY(A_27a,A_27c)) = c_2Efinite__map_2EFEMPTY(A_27a,A_27b))))))))).
tff(conj_thm_2Efinite__map_2EFMAP__MAP2__FUPDATE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(ty_2Epair_2Eprod(A_27a,A_27c),A_27b)) => ( ! [V1m:$i] : (mem(V1m,ty_2Efinite__map_2Efmap(A_27a,A_27c)) => ( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3v:$i] : (mem(V3v,A_27c) => (ap(ap(c_2Efinite__map_2EFMAP__MAP2(A_27a,A_27b,A_27c),V0f),ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27c),V1m),ap(ap(c_2Epair_2E_2C(A_27a,A_27c),V2x),V3v))) = ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),ap(ap(c_2Efinite__map_2EFMAP__MAP2(A_27a,A_27b,A_27c),V0f),V1m)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2x),ap(V0f,ap(ap(c_2Epair_2E_2C(A_27a,A_27c),V2x),V3v)))))))))))))))))).
tff(conj_thm_2Efinite__map_2EFEVERY__STRENGTHEN__THM,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),c_2Efinite__map_2EFEMPTY(A_27a,A_27b))) & ((p(ap(ap(c_2Efinite__map_2EFEVERY(A_27a,A_27b),V0P),V1f)) & 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_2EFUPDATE(A_27a,A_27b),V1f),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2x),V3y)))))))))))))))))).
tff(conj_thm_2Efinite__map_2EFUPDATE__ELIM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0k:$i] : (mem(V0k,A_27a) => ( ! [V1v:$i] : (mem(V1v,A_27b) => ( ! [V2f:$i] : (mem(V2f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ((p(ap(ap(c_2Ebool_2EIN(A_27a),V0k),ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),V2f))) & (ap(ap(c_2Efinite__map_2EFAPPLY(A_27a,A_27b),V2f),V0k) = V1v)) => (ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),V2f),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V0k),V1v)) = V2f)))))))))))).
tff(conj_thm_2Efinite__map_2EFEVERY__DRESTRICT__COMPL,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) => ( ! [V4s:$i] : (mem(V4s,arr(A_27a,bool)) => (p(ap(ap(c_2Efinite__map_2EFEVERY(A_27a,A_27b),V0P),ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27b),V1f),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2k),V3v))),ap(c_2Epred__set_2ECOMPL(A_27a),V4s)))) <=> (((~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V2k),V4s))) => p(ap(V0P,ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2k),V3v)))) & 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),V2k),V4s))))))))))))))))))))).
tff(conj_thm_2Efinite__map_2EFUNION__EQ__FEMPTY,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0h1:$i] : (mem(V0h1,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ! [V1h2:$i] : (mem(V1h2,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ((ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),V0h1),V1h2) = c_2Efinite__map_2EFEMPTY(A_27a,A_27b)) <=> ((V0h1 = c_2Efinite__map_2EFEMPTY(A_27a,A_27b)) & (V1h2 = c_2Efinite__map_2EFEMPTY(A_27a,A_27b)))))))))))).
tff(conj_thm_2Efinite__map_2ESUBMAP__FUNION__EQ,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d: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)) => ( ! [V2f3:$i] : (mem(V2f3,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),V0f1)),ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),V1f2))) => (p(ap(ap(c_2Efinite__map_2ESUBMAP(A_27a,A_27b),V0f1),ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),V1f2),V2f3))) <=> p(ap(ap(c_2Efinite__map_2ESUBMAP(A_27a,A_27b),V0f1),V2f3)))))))))) & ( ! [V3f1:$i] : (mem(V3f1,ty_2Efinite__map_2Efmap(A_27c,A_27d)) => ( ! [V4f2:$i] : (mem(V4f2,ty_2Efinite__map_2Efmap(A_27c,A_27d)) => ( ! [V5f3:$i] : (mem(V5f3,ty_2Efinite__map_2Efmap(A_27c,A_27d)) => (p(ap(ap(c_2Epred__set_2EDISJOINT(A_27c),ap(c_2Efinite__map_2EFDOM(A_27c,A_27d),V3f1)),ap(ap(c_2Epred__set_2EDIFF(A_27c),ap(c_2Efinite__map_2EFDOM(A_27c,A_27d),V5f3)),ap(c_2Efinite__map_2EFDOM(A_27c,A_27d),V4f2)))) => (p(ap(ap(c_2Efinite__map_2ESUBMAP(A_27c,A_27d),V3f1),ap(ap(c_2Efinite__map_2EFUNION(A_27c,A_27d),V4f2),V5f3))) <=> p(ap(ap(c_2Efinite__map_2ESUBMAP(A_27c,A_27d),V3f1),V4f2))))))))))))))))).
tff(conj_thm_2Efinite__map_2ESUBMAP__FUNION,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)) => ( ! [V2f3:$i] : (mem(V2f3,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ((p(ap(ap(c_2Efinite__map_2ESUBMAP(A_27a,A_27b),V0f1),V1f2)) | (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))) & p(ap(ap(c_2Efinite__map_2ESUBMAP(A_27a,A_27b),V0f1),V2f3)))) => p(ap(ap(c_2Efinite__map_2ESUBMAP(A_27a,A_27b),V0f1),ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),V1f2),V2f3)))))))))))))).
tff(conj_thm_2Efinite__map_2ESUBMAP__FUNION__ID,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d: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)) => p(ap(ap(c_2Efinite__map_2ESUBMAP(A_27a,A_27b),V0f1),ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),V0f1),V1f2))))))) & ( ! [V2f1:$i] : (mem(V2f1,ty_2Efinite__map_2Efmap(A_27c,A_27d)) => ( ! [V3f2:$i] : (mem(V3f2,ty_2Efinite__map_2Efmap(A_27c,A_27d)) => (p(ap(ap(c_2Epred__set_2EDISJOINT(A_27c),ap(c_2Efinite__map_2EFDOM(A_27c,A_27d),V2f1)),ap(c_2Efinite__map_2EFDOM(A_27c,A_27d),V3f2))) => p(ap(ap(c_2Efinite__map_2ESUBMAP(A_27c,A_27d),V3f2),ap(ap(c_2Efinite__map_2EFUNION(A_27c,A_27d),V2f1),V3f2))))))))))))))).
tff(conj_thm_2Efinite__map_2EFEMPTY__SUBMAP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0h:$i] : (mem(V0h,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => (p(ap(ap(c_2Efinite__map_2ESUBMAP(A_27a,A_27b),V0h),c_2Efinite__map_2EFEMPTY(A_27a,A_27b))) <=> (V0h = c_2Efinite__map_2EFEMPTY(A_27a,A_27b))))))))).
tff(conj_thm_2Efinite__map_2EFUNION__EQ,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)) => ( ! [V2f3:$i] : (mem(V2f3,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),V0f1)),ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),V1f2))) & 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),V2f3)))) => ((ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),V0f1),V1f2) = ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),V0f1),V2f3)) <=> (V1f2 = V2f3))))))))))))).
tff(conj_thm_2Efinite__map_2EFUNION__EQ__IMPL,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)) => ( ! [V2f3:$i] : (mem(V2f3,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),V0f1)),ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),V1f2))) & (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),V2f3))) & (V1f2 = V2f3))) => (ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),V0f1),V1f2) = ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),V0f1),V2f3))))))))))))).
tff(conj_thm_2Efinite__map_2EDOMSUB__FUNION,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) => (ap(ap(c_2Efinite__map_2Efdomsub(A_27a,A_27b),ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),V0f),V1g)),V2k) = ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),ap(ap(c_2Efinite__map_2Efdomsub(A_27a,A_27b),V0f),V2k)),ap(ap(c_2Efinite__map_2Efdomsub(A_27a,A_27b),V1g),V2k))))))))))))).
tff(conj_thm_2Efinite__map_2EFUNION__COMM,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_2Epred__set_2EDISJOINT(A_27a),ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),V0f)),ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),V1g))) => (ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),V0f),V1g) = ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),V1g),V0f))))))))))).
tff(conj_thm_2Efinite__map_2EFUNION__ASSOC,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)) => (ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),V0f),ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),V1g),V2h)) = ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),V0f),V1g)),V2h)))))))))))).
tff(conj_thm_2Efinite__map_2EDRESTRICT__FUNION,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0h:$i] : (mem(V0h,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ! [V1s1:$i] : (mem(V1s1,arr(A_27a,bool)) => ( ! [V2s2:$i] : (mem(V2s2,arr(A_27a,bool)) => (ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),V0h),V1s1)),ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),V0h),V2s2)) = ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),V0h),ap(ap(c_2Epred__set_2EUNION(A_27a),V1s1),V2s2))))))))))))).
tff(conj_thm_2Efinite__map_2EDRESTRICT__EQ__FUNION,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0h:$i] : (mem(V0h,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ! [V1h1:$i] : (mem(V1h1,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ! [V2h2:$i] : (mem(V2h2,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),V1h1)),ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),V2h2))) & (ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),V1h1),V2h2) = V0h)) => (V2h2 = ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),V0h),ap(c_2Epred__set_2ECOMPL(A_27a),ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),V1h1))))))))))))))).
tff(conj_thm_2Efinite__map_2EIN__FDOM__FOLDR__UNION,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1hL:$i] : (mem(V1hL,ty_2Elist_2Elist(ty_2Efinite__map_2Efmap(A_27a,A_27b))) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),ap(ap(ap(c_2Elist_2EFOLDR(ty_2Efinite__map_2Efmap(A_27a,A_27b),ty_2Efinite__map_2Efmap(A_27a,A_27b)),c_2Efinite__map_2EFUNION(A_27a,A_27b)),c_2Efinite__map_2EFEMPTY(A_27a,A_27b)),V1hL)))) <=> (? [V2h:$i] : (mem(V2h,ty_2Efinite__map_2Efmap(A_27a,A_27b)) & (p(ap(ap(c_2Ebool_2EIN(ty_2Efinite__map_2Efmap(A_27a,A_27b)),V2h),ap(c_2Elist_2ELIST__TO__SET(ty_2Efinite__map_2Efmap(A_27a,A_27b)),V1hL))) & p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),V2h))))))))))))))).
tff(conj_thm_2Efinite__map_2EDRESTRICT__FUNION__DRESTRICT__COMPL,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),V0f),V1s)),ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),V0f),ap(c_2Epred__set_2ECOMPL(A_27a),V1s))) = V0f))))))))).
tff(conj_thm_2Efinite__map_2EDRESTRICT__IDEMPOT,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : (mem(V0s,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ! [V1vs:$i] : (mem(V1vs,arr(A_27a,bool)) => (ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),V0s),V1vs)),V1vs) = ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),V0s),V1vs)))))))))).
tff(conj_thm_2Efinite__map_2ESUBMAP__FUNION__ABSORPTION,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)) <=> (ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),V0f),V1g) = V1g)))))))))).
tff(conj_thm_2Efinite__map_2EMAP__KEYS__witness,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: p(ap(ap(c_2Ebool_2ELET(arr(arr(A_27a,A_27b),arr(ty_2Efinite__map_2Efmap(A_27a,A_27c),ty_2Efinite__map_2Efmap(A_27b,A_27c))),bool),f1925(A_27c,A_27b,A_27a)),f1927(A_27a,A_27c,A_27b)))))))).
tff(ax_thm_2Efinite__map_2EMAP__KEYS__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1fm:$i] : (mem(V1fm,ty_2Efinite__map_2Efmap(A_27a,A_27c)) => ((ap(c_2Efinite__map_2EFDOM(A_27b,A_27c),ap(ap(c_2Efinite__map_2EMAP__KEYS(A_27a,A_27b,A_27c),V0f),V1fm)) = ap(ap(c_2Epred__set_2EIMAGE(A_27a,A_27b),V0f),ap(c_2Efinite__map_2EFDOM(A_27a,A_27c),V1fm))) & (p(ap(ap(ap(c_2Epred__set_2EINJ(A_27a,A_27b),V0f),ap(c_2Efinite__map_2EFDOM(A_27a,A_27c),V1fm)),c_2Epred__set_2EUNIV(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_27c),V1fm))) => (ap(ap(c_2Efinite__map_2EFAPPLY(A_27b,A_27c),ap(ap(c_2Efinite__map_2EMAP__KEYS(A_27a,A_27b,A_27c),V0f),V1fm)),ap(V0f,V2x)) = ap(ap(c_2Efinite__map_2EFAPPLY(A_27a,A_27c),V1fm),V2x))))))))))))))).
tff(conj_thm_2Efinite__map_2EMAP__KEYS__FEMPTY,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => (ap(ap(c_2Efinite__map_2EMAP__KEYS(A_27a,A_27b,A_27c),V0f),c_2Efinite__map_2EFEMPTY(A_27a,A_27c)) = c_2Efinite__map_2EFEMPTY(A_27b,A_27c))))))))).
tff(conj_thm_2Efinite__map_2EMAP__KEYS__FUPDATE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1fm:$i] : (mem(V1fm,ty_2Efinite__map_2Efmap(A_27a,A_27c)) => ( ! [V2k:$i] : (mem(V2k,A_27a) => ( ! [V3v:$i] : (mem(V3v,A_27c) => (p(ap(ap(ap(c_2Epred__set_2EINJ(A_27a,A_27b),V0f),ap(ap(c_2Epred__set_2EINSERT(A_27a),V2k),ap(c_2Efinite__map_2EFDOM(A_27a,A_27c),V1fm))),c_2Epred__set_2EUNIV(A_27b))) => (ap(ap(c_2Efinite__map_2EMAP__KEYS(A_27a,A_27b,A_27c),V0f),ap(ap(c_2Efinite__map_2EFUPDATE(A_27a,A_27c),V1fm),ap(ap(c_2Epair_2E_2C(A_27a,A_27c),V2k),V3v))) = ap(ap(c_2Efinite__map_2EFUPDATE(A_27b,A_27c),ap(ap(c_2Efinite__map_2EMAP__KEYS(A_27a,A_27b,A_27c),V0f),V1fm)),ap(ap(c_2Epair_2E_2C(A_27b,A_27c),ap(V0f,V2k)),V3v))))))))))))))))).
tff(conj_thm_2Efinite__map_2EMAP__KEYS__using__LINV,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1fm:$i] : (mem(V1fm,ty_2Efinite__map_2Efmap(A_27a,A_27c)) => (p(ap(ap(ap(c_2Epred__set_2EINJ(A_27a,A_27b),V0f),ap(c_2Efinite__map_2EFDOM(A_27a,A_27c),V1fm)),c_2Epred__set_2EUNIV(A_27b))) => (ap(ap(c_2Efinite__map_2EMAP__KEYS(A_27a,A_27b,A_27c),V0f),V1fm) = ap(ap(c_2Efinite__map_2Ef__o__f(A_27b,A_27a,A_27c),V1fm),ap(ap(c_2Efinite__map_2EFUN__FMAP(A_27b,A_27a),ap(ap(c_2Epred__set_2ELINV(A_27a,A_27b),V0f),ap(c_2Efinite__map_2EFDOM(A_27a,A_27c),V1fm))),ap(ap(c_2Epred__set_2EIMAGE(A_27a,A_27b),V0f),ap(c_2Efinite__map_2EFDOM(A_27a,A_27c),V1fm))))))))))))))).
tff(conj_thm_2Efinite__map_2EMAP__KEYS__BIJ__LINV,lemma,(( ! [A_27a:del]: ( ! [V0f:$i] : (mem(V0f,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ( ! [V1t:$i] : (mem(V1t,ty_2Efinite__map_2Efmap(ty_2Enum_2Enum,A_27a)) => (p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Enum_2Enum,ty_2Enum_2Enum),V0f),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))) => (ap(ap(c_2Efinite__map_2EMAP__KEYS(ty_2Enum_2Enum,ty_2Enum_2Enum,A_27a),V0f),ap(ap(c_2Efinite__map_2EMAP__KEYS(ty_2Enum_2Enum,ty_2Enum_2Enum,A_27a),ap(ap(c_2Epred__set_2ELINV(ty_2Enum_2Enum,ty_2Enum_2Enum),V0f),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))),V1t)) = V1t))))))))).
tff(conj_thm_2Efinite__map_2EFLOOKUP__MAP__KEYS,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1m:$i] : (mem(V1m,ty_2Efinite__map_2Efmap(A_27a,A_27c)) => ( ! [V2k:$i] : (mem(V2k,A_27b) => (p(ap(ap(ap(c_2Epred__set_2EINJ(A_27a,A_27b),V0f),ap(c_2Efinite__map_2EFDOM(A_27a,A_27c),V1m)),c_2Epred__set_2EUNIV(A_27b))) => (ap(ap(c_2Efinite__map_2EFLOOKUP(A_27b,A_27c),ap(ap(c_2Efinite__map_2EMAP__KEYS(A_27a,A_27b,A_27c),V0f),V1m)),V2k) = ap(ap(c_2Eoption_2EOPTION__BIND(A_27c,A_27a),ap(c_2Eoption_2Esome(A_27a),f1928(A_27b,A_27c,A_27a,V0f,V2k,V1m))),ap(c_2Efinite__map_2EFLOOKUP(A_27a,A_27c),V1m))))))))))))))).
tff(conj_thm_2Efinite__map_2EFLOOKUP__MAP__KEYS__MAPPED,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1m:$i] : (mem(V1m,ty_2Efinite__map_2Efmap(A_27a,A_27c)) => ( ! [V2k:$i] : (mem(V2k,A_27a) => (p(ap(ap(ap(c_2Epred__set_2EINJ(A_27a,A_27b),V0f),c_2Epred__set_2EUNIV(A_27a)),c_2Epred__set_2EUNIV(A_27b))) => (ap(ap(c_2Efinite__map_2EFLOOKUP(A_27b,A_27c),ap(ap(c_2Efinite__map_2EMAP__KEYS(A_27a,A_27b,A_27c),V0f),V1m)),ap(V0f,V2k)) = ap(ap(c_2Efinite__map_2EFLOOKUP(A_27a,A_27c),V1m),V2k)))))))))))))).
tff(conj_thm_2Efinite__map_2EDRESTRICT__MAP__KEYS__IMAGE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1fm:$i] : (mem(V1fm,ty_2Efinite__map_2Efmap(A_27a,A_27c)) => ( ! [V2s:$i] : (mem(V2s,arr(A_27a,bool)) => (p(ap(ap(ap(c_2Epred__set_2EINJ(A_27a,A_27b),V0f),c_2Epred__set_2EUNIV(A_27a)),c_2Epred__set_2EUNIV(A_27b))) => (ap(ap(c_2Efinite__map_2EDRESTRICT(A_27b,A_27c),ap(ap(c_2Efinite__map_2EMAP__KEYS(A_27a,A_27b,A_27c),V0f),V1fm)),ap(ap(c_2Epred__set_2EIMAGE(A_27a,A_27b),V0f),V2s)) = ap(ap(c_2Efinite__map_2EMAP__KEYS(A_27a,A_27b,A_27c),V0f),ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27c),V1fm),V2s))))))))))))))).
tff(conj_thm_2Efinite__map_2EDOMSUB__MAP__KEYS,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1fm:$i] : (mem(V1fm,ty_2Efinite__map_2Efmap(A_27a,A_27c)) => ( ! [V2s:$i] : (mem(V2s,A_27a) => (p(ap(ap(ap(c_2Epred__set_2EBIJ(A_27a,A_27b),V0f),c_2Epred__set_2EUNIV(A_27a)),c_2Epred__set_2EUNIV(A_27b))) => (ap(ap(c_2Efinite__map_2Efdomsub(A_27b,A_27c),ap(ap(c_2Efinite__map_2EMAP__KEYS(A_27a,A_27b,A_27c),V0f),V1fm)),ap(V0f,V2s)) = ap(ap(c_2Efinite__map_2EMAP__KEYS(A_27a,A_27b,A_27c),V0f),ap(ap(c_2Efinite__map_2Efdomsub(A_27a,A_27c),V1fm),V2s))))))))))))))).
tff(ax_thm_2Efinite__map_2Efmap__rel__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27b,bool))) => ( ! [V1f1:$i] : (mem(V1f1,ty_2Efinite__map_2Efmap(A_27c,A_27a)) => ( ! [V2f2:$i] : (mem(V2f2,ty_2Efinite__map_2Efmap(A_27c,A_27b)) => (p(ap(ap(ap(c_2Efinite__map_2Efmap__rel(A_27a,A_27b,A_27c),V0R),V1f1),V2f2)) <=> ((ap(c_2Efinite__map_2EFDOM(A_27c,A_27b),V2f2) = ap(c_2Efinite__map_2EFDOM(A_27c,A_27a),V1f1)) & ( ! [V3x:$i] : (mem(V3x,A_27c) => (p(ap(ap(c_2Ebool_2EIN(A_27c),V3x),ap(c_2Efinite__map_2EFDOM(A_27c,A_27a),V1f1))) => p(ap(ap(V0R,ap(ap(c_2Efinite__map_2EFAPPLY(A_27c,A_27a),V1f1),V3x)),ap(ap(c_2Efinite__map_2EFAPPLY(A_27c,A_27b),V2f2),V3x)))))))))))))))))).
tff(conj_thm_2Efinite__map_2Efmap__rel__FUPDATE__same,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27b,bool))) => ( ! [V1f1:$i] : (mem(V1f1,ty_2Efinite__map_2Efmap(A_27c,A_27a)) => ( ! [V2f2:$i] : (mem(V2f2,ty_2Efinite__map_2Efmap(A_27c,A_27b)) => ( ! [V3v1:$i] : (mem(V3v1,A_27a) => ( ! [V4v2:$i] : (mem(V4v2,A_27b) => ( ! [V5k:$i] : (mem(V5k,A_27c) => ((p(ap(ap(ap(c_2Efinite__map_2Efmap__rel(A_27a,A_27b,A_27c),V0R),V1f1),V2f2)) & p(ap(ap(V0R,V3v1),V4v2))) => p(ap(ap(ap(c_2Efinite__map_2Efmap__rel(A_27a,A_27b,A_27c),V0R),ap(ap(c_2Efinite__map_2EFUPDATE(A_27c,A_27a),V1f1),ap(ap(c_2Epair_2E_2C(A_27c,A_27a),V5k),V3v1))),ap(ap(c_2Efinite__map_2EFUPDATE(A_27c,A_27b),V2f2),ap(ap(c_2Epair_2E_2C(A_27c,A_27b),V5k),V4v2)))))))))))))))))))))).
tff(conj_thm_2Efinite__map_2Efmap__rel__FUPDATE__LIST__same,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27b,bool))) => ( ! [V1ls1:$i] : (mem(V1ls1,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27c,A_27a))) => ( ! [V2ls2:$i] : (mem(V2ls2,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27c,A_27b))) => ( ! [V3f1:$i] : (mem(V3f1,ty_2Efinite__map_2Efmap(A_27c,A_27a)) => ( ! [V4f2:$i] : (mem(V4f2,ty_2Efinite__map_2Efmap(A_27c,A_27b)) => ((p(ap(ap(ap(c_2Efinite__map_2Efmap__rel(A_27a,A_27b,A_27c),V0R),V3f1),V4f2)) & ((ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27c,A_27a),A_27c),c_2Epair_2EFST(A_27c,A_27a)),V1ls1) = ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27c,A_27b),A_27c),c_2Epair_2EFST(A_27c,A_27b)),V2ls2)) & p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27c,A_27a),A_27a),c_2Epair_2ESND(A_27c,A_27a)),V1ls1)),ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27c,A_27b),A_27b),c_2Epair_2ESND(A_27c,A_27b)),V2ls2))))) => p(ap(ap(ap(c_2Efinite__map_2Efmap__rel(A_27a,A_27b,A_27c),V0R),ap(ap(c_2Efinite__map_2EFUPDATE__LIST(A_27c,A_27a),V3f1),V1ls1)),ap(ap(c_2Efinite__map_2EFUPDATE__LIST(A_27c,A_27b),V4f2),V2ls2))))))))))))))))))).
tff(conj_thm_2Efinite__map_2Efmap__rel__FEMPTY,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27b,bool))) => p(ap(ap(ap(c_2Efinite__map_2Efmap__rel(A_27a,A_27b,A_27c),V0R),c_2Efinite__map_2EFEMPTY(A_27c,A_27a)),c_2Efinite__map_2EFEMPTY(A_27c,A_27b)))))))))).
tff(conj_thm_2Efinite__map_2Efmap__rel__FEMPTY2,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27a,bool))) => ( ! [V1f:$i] : (mem(V1f,ty_2Efinite__map_2Efmap(A_27b,A_27a)) => ((p(ap(ap(ap(c_2Efinite__map_2Efmap__rel(A_27a,A_27a,A_27b),V0R),c_2Efinite__map_2EFEMPTY(A_27b,A_27a)),V1f)) <=> (V1f = c_2Efinite__map_2EFEMPTY(A_27b,A_27a))) & (p(ap(ap(ap(c_2Efinite__map_2Efmap__rel(A_27a,A_27a,A_27b),V0R),V1f),c_2Efinite__map_2EFEMPTY(A_27b,A_27a))) <=> (V1f = c_2Efinite__map_2EFEMPTY(A_27b,A_27a)))))))))))).
tff(conj_thm_2Efinite__map_2Efmap__rel__refl,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27a,bool))) => ( ! [V1x:$i] : (mem(V1x,ty_2Efinite__map_2Efmap(A_27b,A_27a)) => (( ! [V2x:$i] : (mem(V2x,A_27a) => p(ap(ap(V0R,V2x),V2x)))) => p(ap(ap(ap(c_2Efinite__map_2Efmap__rel(A_27a,A_27a,A_27b),V0R),V1x),V1x))))))))))).
tff(conj_thm_2Efinite__map_2Efmap__rel__FUNION__rels,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27b,bool))) => ( ! [V1f1:$i] : (mem(V1f1,ty_2Efinite__map_2Efmap(A_27c,A_27a)) => ( ! [V2f2:$i] : (mem(V2f2,ty_2Efinite__map_2Efmap(A_27c,A_27b)) => ( ! [V3f3:$i] : (mem(V3f3,ty_2Efinite__map_2Efmap(A_27c,A_27a)) => ( ! [V4f4:$i] : (mem(V4f4,ty_2Efinite__map_2Efmap(A_27c,A_27b)) => ((p(ap(ap(ap(c_2Efinite__map_2Efmap__rel(A_27a,A_27b,A_27c),V0R),V1f1),V2f2)) & p(ap(ap(ap(c_2Efinite__map_2Efmap__rel(A_27a,A_27b,A_27c),V0R),V3f3),V4f4))) => p(ap(ap(ap(c_2Efinite__map_2Efmap__rel(A_27a,A_27b,A_27c),V0R),ap(ap(c_2Efinite__map_2EFUNION(A_27c,A_27a),V1f1),V3f3)),ap(ap(c_2Efinite__map_2EFUNION(A_27c,A_27b),V2f2),V4f4))))))))))))))))))).
tff(conj_thm_2Efinite__map_2Efmap__rel__FUPDATE__I,conjecture,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27b,bool))) => ( ! [V1f1:$i] : (mem(V1f1,ty_2Efinite__map_2Efmap(A_27c,A_27a)) => ( ! [V2k:$i] : (mem(V2k,A_27c) => ( ! [V3f2:$i] : (mem(V3f2,ty_2Efinite__map_2Efmap(A_27c,A_27b)) => ( ! [V4v1:$i] : (mem(V4v1,A_27a) => ( ! [V5v2:$i] : (mem(V5v2,A_27b) => ((p(ap(ap(ap(c_2Efinite__map_2Efmap__rel(A_27a,A_27b,A_27c),V0R),ap(ap(c_2Efinite__map_2Efdomsub(A_27c,A_27a),V1f1),V2k)),ap(ap(c_2Efinite__map_2Efdomsub(A_27c,A_27b),V3f2),V2k))) & p(ap(ap(V0R,V4v1),V5v2))) => p(ap(ap(ap(c_2Efinite__map_2Efmap__rel(A_27a,A_27b,A_27c),V0R),ap(ap(c_2Efinite__map_2EFUPDATE(A_27c,A_27a),V1f1),ap(ap(c_2Epair_2E_2C(A_27c,A_27a),V2k),V4v1))),ap(ap(c_2Efinite__map_2EFUPDATE(A_27c,A_27b),V3f2),ap(ap(c_2Epair_2E_2C(A_27c,A_27b),V2k),V5v2)))))))))))))))))))))).
