include('Axioms/DeepSyntax+2.ax').
fof(mem_c_2Efmapal_2EAP__SND,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => mem(c_2Efmapal_2EAP__SND(A_27a,A_27b,A_27c),arr(arr(A_27b,A_27c),arr(ty_2Epair_2Eprod(A_27a,A_27b),ty_2Epair_2Eprod(A_27a,A_27c)))) ) ) ) )).
fof(mem_c_2Efmapal_2EFMAPAL,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2EFMAPAL(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Efinite__map_2Efmap(A_27a,A_27b)))) ) ) )).
fof(mem_c_2Efmapal_2EOFU,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2EOFU(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Efinite__map_2Efmap(A_27a,A_27b),arr(ty_2Efinite__map_2Efmap(A_27a,A_27b),ty_2Efinite__map_2Efmap(A_27a,A_27b))))) ) ) )).
fof(mem_c_2Efmapal_2EOPTION__FLAT,axiom,( ! [A_27z] : ( ne(A_27z) => mem(c_2Efmapal_2EOPTION__FLAT(A_27z),arr(ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27z))),ty_2Elist_2Elist(A_27z))) ) )).
fof(mem_c_2Efmapal_2EOPTION__UPDATE,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2EOPTION__UPDATE(A_27a,A_27b),arr(arr(A_27a,ty_2Eoption_2Eoption(A_27b)),arr(arr(A_27a,ty_2Eoption_2Eoption(A_27b)),arr(A_27a,ty_2Eoption_2Eoption(A_27b))))) ) ) )).
fof(mem_c_2Efmapal_2EORL,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2EORL(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),bool))) ) ) )).
fof(mem_c_2Efmapal_2EORL__bt,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2EORL__bt(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),bool))) ) ) )).
fof(mem_c_2Efmapal_2EORL__bt__lb,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2EORL__bt__lb(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),bool)))) ) ) )).
fof(mem_c_2Efmapal_2EORL__bt__lb__ub,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2EORL__bt__lb__ub(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),arr(A_27a,bool))))) ) ) )).
fof(mem_c_2Efmapal_2EORL__bt__ub,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2EORL__bt__ub(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),arr(A_27a,bool)))) ) ) )).
fof(mem_c_2Efmapal_2EORL__sublists,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2EORL__sublists(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),bool))) ) ) )).
fof(mem_c_2Efmapal_2EORWL,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2EORWL(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Efinite__map_2Efmap(A_27a,A_27b),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),bool)))) ) ) )).
fof(mem_c_2Efmapal_2EUFO,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2EUFO(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Efinite__map_2Efmap(A_27a,A_27b),arr(ty_2Efinite__map_2Efmap(A_27a,A_27b),ty_2Efinite__map_2Efmap(A_27a,A_27b))))) ) ) )).
fof(mem_c_2Efmapal_2Eassocv,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Eassocv(A_27a,A_27b),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) ) ) )).
fof(mem_c_2Efmapal_2Ebl__to__fmap,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Ebl__to__fmap(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebl(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Efinite__map_2Efmap(A_27a,A_27b)))) ) ) )).
fof(mem_c_2Efmapal_2Ebt__map,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Ebt__map(A_27a,A_27b),arr(arr(A_27a,A_27b),arr(ty_2Eenumeral_2Ebt(A_27a),ty_2Eenumeral_2Ebt(A_27b)))) ) ) )).
fof(mem_c_2Efmapal_2Ebt__rplacv__cn,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Ebt__rplacv__cn(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Epair_2Eprod(A_27a,A_27b),arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),arr(arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))),ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))))))) ) ) )).
fof(mem_c_2Efmapal_2Ebt__to__fmap__lb,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Ebt__to__fmap__lb(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Efinite__map_2Efmap(A_27a,A_27b))))) ) ) )).
fof(mem_c_2Efmapal_2Ebt__to__fmap__lb__ub,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Ebt__to__fmap__lb__ub(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),arr(A_27a,ty_2Efinite__map_2Efmap(A_27a,A_27b)))))) ) ) )).
fof(mem_c_2Efmapal_2Ebt__to__fmap__ub,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Ebt__to__fmap__ub(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),arr(A_27a,ty_2Efinite__map_2Efmap(A_27a,A_27b))))) ) ) )).
fof(mem_c_2Efmapal_2Ebt__to__orl,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Ebt__to__orl(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) ) ) )).
fof(mem_c_2Efmapal_2Ebt__to__orl__ac,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Ebt__to__orl__ac(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))))) ) ) )).
fof(mem_c_2Efmapal_2Ebt__to__orl__lb,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Ebt__to__orl__lb(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))))) ) ) )).
fof(mem_c_2Efmapal_2Ebt__to__orl__lb__ac,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Ebt__to__orl__lb__ac(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))))) ) ) )).
fof(mem_c_2Efmapal_2Ebt__to__orl__lb__ub,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Ebt__to__orl__lb__ub(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),arr(A_27a,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))))) ) ) )).
fof(mem_c_2Efmapal_2Ebt__to__orl__lb__ub__ac,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Ebt__to__orl__lb__ub__ac(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),arr(A_27a,arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))))))) ) ) )).
fof(mem_c_2Efmapal_2Ebt__to__orl__lb__ub__ac__tupled__aux,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Ebt__to__orl__lb__ub__ac__tupled__aux(A_27a,A_27b),arr(arr(ty_2Epair_2Eprod(ty_2Etoto_2Etoto(A_27a),ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))))),arr(ty_2Epair_2Eprod(ty_2Etoto_2Etoto(A_27a),ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))))),bool)),arr(ty_2Epair_2Eprod(ty_2Etoto_2Etoto(A_27a),ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))))),ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) ) ) )).
fof(mem_c_2Efmapal_2Ebt__to__orl__ub,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Ebt__to__orl__ub(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),arr(A_27a,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))))) ) ) )).
fof(mem_c_2Efmapal_2Ebt__to__orl__ub__ac,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Ebt__to__orl__ub__ac(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),arr(A_27a,arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))))) ) ) )).
fof(mem_c_2Efmapal_2Ediff__merge,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Ediff__merge(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))))) ) ) )).
fof(mem_c_2Efmapal_2Efmap,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Efmap(A_27a,A_27b),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Efinite__map_2Efmap(A_27a,A_27b))) ) ) )).
fof(mem_c_2Efmapal_2Eincr__build,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Eincr__build(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))))) ) ) )).
fof(mem_c_2Efmapal_2Eincr__flat,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Eincr__flat(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) ) ) )).
fof(mem_c_2Efmapal_2Eincr__merge,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Eincr__merge(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),arr(ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))))))) ) ) )).
fof(mem_c_2Efmapal_2Eincr__sort,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Eincr__sort(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) ) ) )).
fof(mem_c_2Efmapal_2Einter__merge,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Einter__merge(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))))) ) ) )).
fof(mem_c_2Efmapal_2Elist__rplacv__cn,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Elist__rplacv__cn(A_27a,A_27b),arr(ty_2Epair_2Eprod(A_27a,A_27b),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),arr(arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))),ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))))) ) ) )).
fof(mem_c_2Efmapal_2Emerge,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Emerge(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))))) ) ) )).
fof(mem_c_2Efmapal_2Emerge__out,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Emerge__out(A_27a,A_27b),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),arr(ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))))) ) ) )).
fof(mem_c_2Efmapal_2Eoptry,axiom,( ! [A_27z] : ( ne(A_27z) => mem(c_2Efmapal_2Eoptry(A_27z),arr(ty_2Eoption_2Eoption(A_27z),arr(ty_2Eoption_2Eoption(A_27z),ty_2Eoption_2Eoption(A_27z)))) ) )).
fof(mem_c_2Efmapal_2Eoptry__list,axiom,( ! [A_27g] : ( ne(A_27g) => ! [A_27z] : ( ne(A_27z) => mem(c_2Efmapal_2Eoptry__list(A_27g,A_27z),arr(arr(A_27z,ty_2Eoption_2Eoption(A_27g)),arr(ty_2Elist_2Elist(ty_2Eoption_2Eoption(A_27z)),ty_2Eoption_2Eoption(A_27g)))) ) ) )).
fof(mem_c_2Efmapal_2Eunlookup,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Eunlookup(A_27a,A_27b),arr(arr(A_27a,ty_2Eoption_2Eoption(A_27b)),ty_2Efinite__map_2Efmap(A_27a,A_27b))) ) ) )).
fof(mem_c_2Efmapal_2Evcossa,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Efmapal_2Evcossa(A_27a,A_27b),arr(A_27a,arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Eoption_2Eoption(A_27b)))) ) ) )).
fof(conj_thm_2Efmapal_2EORL__ind,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),bool))) => ( ( ( ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => p(ap(ap(V0P,V1cmp),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b)))) ) ) & ! [V2cmp] : ( mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V3a] : ( mem(V3a,A_27a) => ! [V4b] : ( mem(V4b,A_27b) => ! [V5l] : ( mem(V5l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( p(ap(ap(V0P,V2cmp),V5l)) => p(ap(ap(V0P,V2cmp),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V3a),V4b)),V5l))) ) ) ) ) ) ) => ! [V6v] : ( mem(V6v,ty_2Etoto_2Etoto(A_27a)) => ! [V7v1] : ( mem(V7v1,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(V0P,V6v),V7v1)) ) ) ) ))))).
fof(conj_thm_2Efmapal_2EORL,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( p(ap(ap(c_2Efmapal_2EORL(A_27a,A_27b),V0cmp),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b)))) <=> $true ) ) ) & ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V2cmp] : ( mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V3b] : ( mem(V3b,A_27b) => ! [V4a] : ( mem(V4a,A_27a) => ( p(ap(ap(c_2Efmapal_2EORL(A_27a,A_27b),V2cmp),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V4a),V3b)),V1l))) <=> ( p(ap(ap(c_2Efmapal_2EORL(A_27a,A_27b),V2cmp),V1l)) & ! [V5p] : ( mem(V5p,A_27a) => ! [V6q] : ( mem(V6q,A_27b) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V5p),V6q)),ap(c_2Elist_2ELIST__TO__SET(ty_2Epair_2Eprod(A_27a,A_27b)),V1l))) => ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V2cmp),V4a),V5p) = c_2EternaryComparisons_2ELESS ) ) ) ) ) ) ) ) ) ) ))))).
fof(ax_thm_2Efmapal_2Eoptry,axiom,( ! [A_27z] : ( ne(A_27z) => ( ( ! [V0p] : ( mem(V0p,A_27z) => ! [V1q] : ( mem(V1q,ty_2Eoption_2Eoption(A_27z)) => ( ap(ap(c_2Efmapal_2Eoptry(A_27z),ap(c_2Eoption_2ESOME(A_27z),V0p)),V1q) = ap(c_2Eoption_2ESOME(A_27z),V0p) ) ) ) ) & ! [V2q] : ( mem(V2q,ty_2Eoption_2Eoption(A_27z)) => ( ap(ap(c_2Efmapal_2Eoptry(A_27z),c_2Eoption_2ENONE(A_27z)),V2q) = V2q ) ) ) ) )).
fof(conj_thm_2Efmapal_2Eoptry__list__ind,lemma,( ! [A_27g]: ( ne(A_27g) =>  ! [A_27z]: ( ne(A_27z) => ! [V0P] : ( mem(V0P,arr(arr(A_27z,ty_2Eoption_2Eoption(A_27g)),arr(ty_2Elist_2Elist(ty_2Eoption_2Eoption(A_27z)),bool))) => ( ( ( ! [V1f] : ( mem(V1f,arr(A_27z,ty_2Eoption_2Eoption(A_27g))) => p(ap(ap(V0P,V1f),c_2Elist_2ENIL(ty_2Eoption_2Eoption(A_27z)))) ) ) & ( ( ! [V2f] : ( mem(V2f,arr(A_27z,ty_2Eoption_2Eoption(A_27g))) => ! [V3l] : ( mem(V3l,ty_2Elist_2Elist(ty_2Eoption_2Eoption(A_27z))) => ( p(ap(ap(V0P,V2f),V3l)) => p(ap(ap(V0P,V2f),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(A_27z)),c_2Eoption_2ENONE(A_27z)),V3l))) ) ) ) ) & ! [V4f] : ( mem(V4f,arr(A_27z,ty_2Eoption_2Eoption(A_27g))) => ! [V5z] : ( mem(V5z,A_27z) => ! [V6l] : ( mem(V6l,ty_2Elist_2Elist(ty_2Eoption_2Eoption(A_27z))) => ( p(ap(ap(V0P,V4f),V6l)) => p(ap(ap(V0P,V4f),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(A_27z)),ap(c_2Eoption_2ESOME(A_27z),V5z)),V6l))) ) ) ) ) ) ) => ! [V7v] : ( mem(V7v,arr(A_27z,ty_2Eoption_2Eoption(A_27g))) => ! [V8v1] : ( mem(V8v1,ty_2Elist_2Elist(ty_2Eoption_2Eoption(A_27z))) => p(ap(ap(V0P,V7v),V8v1)) ) ) ) ))))).
fof(conj_thm_2Efmapal_2Eoptry__list,lemma,( ! [A_27g]: ( ne(A_27g) =>  ! [A_27z]: ( ne(A_27z) => ( ( ! [V0f] : ( mem(V0f,arr(A_27z,ty_2Eoption_2Eoption(A_27g))) => ( ap(ap(c_2Efmapal_2Eoptry__list(A_27g,A_27z),V0f),c_2Elist_2ENIL(ty_2Eoption_2Eoption(A_27z))) = c_2Eoption_2ENONE(A_27g) ) ) ) & ( ( ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(ty_2Eoption_2Eoption(A_27z))) => ! [V2f] : ( mem(V2f,arr(A_27z,ty_2Eoption_2Eoption(A_27g))) => ( ap(ap(c_2Efmapal_2Eoptry__list(A_27g,A_27z),V2f),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(A_27z)),c_2Eoption_2ENONE(A_27z)),V1l)) = ap(ap(c_2Efmapal_2Eoptry__list(A_27g,A_27z),V2f),V1l) ) ) ) ) & ! [V3z] : ( mem(V3z,A_27z) => ! [V4l] : ( mem(V4l,ty_2Elist_2Elist(ty_2Eoption_2Eoption(A_27z))) => ! [V5f] : ( mem(V5f,arr(A_27z,ty_2Eoption_2Eoption(A_27g))) => ( ap(ap(c_2Efmapal_2Eoptry__list(A_27g,A_27z),V5f),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(A_27z)),ap(c_2Eoption_2ESOME(A_27z),V3z)),V4l)) = ap(ap(c_2Efmapal_2Eoptry(A_27g),ap(V5f,V3z)),ap(ap(c_2Efmapal_2Eoptry__list(A_27g,A_27z),V5f),V4l)) ) ) ) ) ) ))))).
fof(conj_thm_2Efmapal_2Eassocv__ind,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),arr(A_27a,bool))) => ( ( ( ! [V1a] : ( mem(V1a,A_27a) => p(ap(ap(V0P,c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))),V1a)) ) ) & ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( mem(V3y,A_27b) => ! [V4l] : ( mem(V4l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V5a] : ( mem(V5a,A_27a) => ( ( ( ~~ ( V5a = V2x ) ) => p(ap(ap(V0P,V4l),V5a)) ) => p(ap(ap(V0P,ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2x),V3y)),V4l)),V5a)) ) ) ) ) ) ) => ! [V6v] : ( mem(V6v,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V7v1] : ( mem(V7v1,A_27a) => p(ap(ap(V0P,V6v),V7v1)) ) ) ) ))))).
fof(conj_thm_2Efmapal_2Eassocv,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0a] : ( mem(V0a,A_27a) => ( ap(ap(c_2Efmapal_2Eassocv(A_27a,A_27b),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))),V0a) = c_2Eoption_2ENONE(A_27b) ) ) ) & ! [V1y] : ( mem(V1y,A_27b) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3l] : ( mem(V3l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V4a] : ( mem(V4a,A_27a) => ( ap(ap(c_2Efmapal_2Eassocv(A_27a,A_27b),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2x),V1y)),V3l)),V4a) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(A_27b)),ap(ap(c_2Emin_2E_3D(A_27a),V4a),V2x)),ap(c_2Eoption_2ESOME(A_27b),V1y)),ap(ap(c_2Efmapal_2Eassocv(A_27a,A_27b),V3l),V4a)) ) ) ) ) ) ))))).
fof(ax_thm_2Efmapal_2Evcossa,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0a] : ( mem(V0a,A_27a) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ap(ap(c_2Efmapal_2Evcossa(A_27a,A_27b),V0a),V1l) = ap(ap(c_2Efmapal_2Eassocv(A_27a,A_27b),V1l),V0a) ) ) ) ) ) )).
fof(ax_thm_2Efmapal_2EOPTION__UPDATE,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,ty_2Eoption_2Eoption(A_27b))) => ! [V1g] : ( mem(V1g,arr(A_27a,ty_2Eoption_2Eoption(A_27b))) => ! [V2x] : ( mem(V2x,A_27a) => ( ap(ap(ap(c_2Efmapal_2EOPTION__UPDATE(A_27a,A_27b),V0f),V1g),V2x) = ap(ap(c_2Efmapal_2Eoptry(A_27b),ap(V0f,V2x)),ap(V1g,V2x)) ) ) ) ) ) ) )).
fof(conj_thm_2Efmapal_2Emerge__ind,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),bool)))) => ( ( ( ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(ap(V0P,V1cmp),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))),V2l)) ) ) ) & ( ( ! [V3cmp] : ( mem(V3cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V4v4] : ( mem(V4v4,ty_2Epair_2Eprod(A_27a,A_27b)) => ! [V5v5] : ( mem(V5v5,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(ap(V0P,V3cmp),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),V4v4),V5v5)),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b)))) ) ) ) ) & ! [V6cmp] : ( mem(V6cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V7a1] : ( mem(V7a1,A_27a) => ! [V8b1] : ( mem(V8b1,A_27b) => ! [V9l1] : ( mem(V9l1,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V10a2] : ( mem(V10a2,A_27a) => ! [V11b2] : ( mem(V11b2,A_27b) => ! [V12l2] : ( mem(V12l2,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ( ( ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V6cmp),V7a1),V10a2) = c_2EternaryComparisons_2EEQUAL ) => p(ap(ap(ap(V0P,V6cmp),V9l1),V12l2)) ) & ( ( ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V6cmp),V7a1),V10a2) = c_2EternaryComparisons_2EGREATER ) => p(ap(ap(ap(V0P,V6cmp),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V7a1),V8b1)),V9l1)),V12l2)) ) & ( ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V6cmp),V7a1),V10a2) = c_2EternaryComparisons_2ELESS ) => p(ap(ap(ap(V0P,V6cmp),V9l1),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V10a2),V11b2)),V12l2))) ) ) ) => p(ap(ap(ap(V0P,V6cmp),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V7a1),V8b1)),V9l1)),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V10a2),V11b2)),V12l2))) ) ) ) ) ) ) ) ) ) ) => ! [V13v] : ( mem(V13v,ty_2Etoto_2Etoto(A_27a)) => ! [V14v1] : ( mem(V14v1,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V15v2] : ( mem(V15v2,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(ap(V0P,V13v),V14v1),V15v2)) ) ) ) ) ))))).
fof(conj_thm_2Efmapal_2Emerge,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Efmapal_2Emerge(A_27a,A_27b),V1cmp),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))),V0l) = V0l ) ) ) ) & ( ( ! [V2v5] : ( mem(V2v5,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V3v4] : ( mem(V3v4,ty_2Epair_2Eprod(A_27a,A_27b)) => ! [V4cmp] : ( mem(V4cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Efmapal_2Emerge(A_27a,A_27b),V4cmp),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),V3v4),V2v5)),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))) = ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),V3v4),V2v5) ) ) ) ) ) & ! [V5l2] : ( mem(V5l2,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V6l1] : ( mem(V6l1,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V7cmp] : ( mem(V7cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V8b2] : ( mem(V8b2,A_27b) => ! [V9b1] : ( mem(V9b1,A_27b) => ! [V10a2] : ( mem(V10a2,A_27a) => ! [V11a1] : ( mem(V11a1,A_27a) => ( ap(ap(ap(c_2Efmapal_2Emerge(A_27a,A_27b),V7cmp),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V11a1),V9b1)),V6l1)),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V10a2),V8b2)),V5l2)) = ap(ap(ap(ap(c_2EternaryComparisons_2Eordering__CASE(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V7cmp),V11a1),V10a2)),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V11a1),V9b1)),ap(ap(ap(c_2Efmapal_2Emerge(A_27a,A_27b),V7cmp),V6l1),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V10a2),V8b2)),V5l2)))),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V11a1),V9b1)),ap(ap(ap(c_2Efmapal_2Emerge(A_27a,A_27b),V7cmp),V6l1),V5l2))),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V10a2),V8b2)),ap(ap(ap(c_2Efmapal_2Emerge(A_27a,A_27b),V7cmp),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V11a1),V9b1)),V6l1)),V5l2))) ) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Efmapal_2Eincr__merge__ind,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),arr(ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),bool)))) => ( ( ( ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(ap(V0P,V1cmp),V2l),c_2Elist_2ENIL(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))))) ) ) ) & ( ( ! [V3cmp] : ( mem(V3cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V4l] : ( mem(V4l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V5lol] : ( mem(V5lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) => p(ap(ap(ap(V0P,V3cmp),V4l),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),c_2Eoption_2ENONE(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),V5lol))) ) ) ) ) & ! [V6cmp] : ( mem(V6cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V7l] : ( mem(V7l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V8m] : ( mem(V8m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V9lol] : ( mem(V9lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) => ( p(ap(ap(ap(V0P,V6cmp),ap(ap(ap(c_2Efmapal_2Emerge(A_27a,A_27b),V6cmp),V7l),V8m)),V9lol)) => p(ap(ap(ap(V0P,V6cmp),V7l),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),ap(c_2Eoption_2ESOME(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))),V8m)),V9lol))) ) ) ) ) ) ) ) => ! [V10v] : ( mem(V10v,ty_2Etoto_2Etoto(A_27a)) => ! [V11v1] : ( mem(V11v1,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V12v2] : ( mem(V12v2,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) => p(ap(ap(ap(V0P,V10v),V11v1),V12v2)) ) ) ) ) ))))).
fof(conj_thm_2Efmapal_2Eincr__merge,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Efmapal_2Eincr__merge(A_27a,A_27b),V1cmp),V0l),c_2Elist_2ENIL(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) = ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),ap(c_2Eoption_2ESOME(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))),V0l)),c_2Elist_2ENIL(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) ) ) ) ) & ( ( ! [V2lol] : ( mem(V2lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) => ! [V3l] : ( mem(V3l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V4cmp] : ( mem(V4cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Efmapal_2Eincr__merge(A_27a,A_27b),V4cmp),V3l),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),c_2Eoption_2ENONE(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),V2lol)) = ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),ap(c_2Eoption_2ESOME(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))),V3l)),V2lol) ) ) ) ) ) & ! [V5m] : ( mem(V5m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V6lol] : ( mem(V6lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) => ! [V7l] : ( mem(V7l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V8cmp] : ( mem(V8cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Efmapal_2Eincr__merge(A_27a,A_27b),V8cmp),V7l),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),ap(c_2Eoption_2ESOME(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))),V5m)),V6lol)) = ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),c_2Eoption_2ENONE(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),ap(ap(ap(c_2Efmapal_2Eincr__merge(A_27a,A_27b),V8cmp),ap(ap(ap(c_2Efmapal_2Emerge(A_27a,A_27b),V8cmp),V7l),V5m)),V6lol)) ) ) ) ) ) ) ))))).
fof(conj_thm_2Efmapal_2EORL__sublists__ind,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),bool))) => ( ( ( ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => p(ap(ap(V0P,V1cmp),c_2Elist_2ENIL(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))))) ) ) & ( ( ! [V2cmp] : ( mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V3lol] : ( mem(V3lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) => ( p(ap(ap(V0P,V2cmp),V3lol)) => p(ap(ap(V0P,V2cmp),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),c_2Eoption_2ENONE(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),V3lol))) ) ) ) ) & ! [V4cmp] : ( mem(V4cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V5m] : ( mem(V5m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V6lol] : ( mem(V6lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) => ( p(ap(ap(V0P,V4cmp),V6lol)) => p(ap(ap(V0P,V4cmp),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),ap(c_2Eoption_2ESOME(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))),V5m)),V6lol))) ) ) ) ) ) ) => ! [V7v] : ( mem(V7v,ty_2Etoto_2Etoto(A_27a)) => ! [V8v1] : ( mem(V8v1,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) => p(ap(ap(V0P,V7v),V8v1)) ) ) ) ))))).
fof(conj_thm_2Efmapal_2EORL__sublists,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( p(ap(ap(c_2Efmapal_2EORL__sublists(A_27a,A_27b),V0cmp),c_2Elist_2ENIL(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))))) <=> $true ) ) ) & ( ( ! [V1lol] : ( mem(V1lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) => ! [V2cmp] : ( mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ( p(ap(ap(c_2Efmapal_2EORL__sublists(A_27a,A_27b),V2cmp),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),c_2Eoption_2ENONE(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),V1lol))) <=> p(ap(ap(c_2Efmapal_2EORL__sublists(A_27a,A_27b),V2cmp),V1lol)) ) ) ) ) & ! [V3m] : ( mem(V3m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V4lol] : ( mem(V4lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) => ! [V5cmp] : ( mem(V5cmp,ty_2Etoto_2Etoto(A_27a)) => ( p(ap(ap(c_2Efmapal_2EORL__sublists(A_27a,A_27b),V5cmp),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),ap(c_2Eoption_2ESOME(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))),V3m)),V4lol))) <=> ( p(ap(ap(c_2Efmapal_2EORL(A_27a,A_27b),V5cmp),V3m)) & p(ap(ap(c_2Efmapal_2EORL__sublists(A_27a,A_27b),V5cmp),V4lol)) ) ) ) ) ) ) ))))).
fof(ax_thm_2Efmapal_2Eincr__build,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( ( ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(c_2Efmapal_2Eincr__build(A_27a,A_27b),V0cmp),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))) = c_2Elist_2ENIL(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))) ) ) ) & ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V2ab] : ( mem(V2ab,ty_2Epair_2Eprod(A_27a,A_27b)) => ! [V3l] : ( mem(V3l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ap(ap(c_2Efmapal_2Eincr__build(A_27a,A_27b),V1cmp),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),V2ab),V3l)) = ap(ap(ap(c_2Efmapal_2Eincr__merge(A_27a,A_27b),V1cmp),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),V2ab),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b)))),ap(ap(c_2Efmapal_2Eincr__build(A_27a,A_27b),V1cmp),V3l)) ) ) ) ) ) ) ) )).
fof(conj_thm_2Efmapal_2Emerge__out__ind,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),arr(ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),bool)))) => ( ( ( ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(ap(V0P,V1cmp),V2l),c_2Elist_2ENIL(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))))) ) ) ) & ( ( ! [V3cmp] : ( mem(V3cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V4l] : ( mem(V4l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V5lol] : ( mem(V5lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) => ( p(ap(ap(ap(V0P,V3cmp),V4l),V5lol)) => p(ap(ap(ap(V0P,V3cmp),V4l),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),c_2Eoption_2ENONE(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),V5lol))) ) ) ) ) ) & ! [V6cmp] : ( mem(V6cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V7l] : ( mem(V7l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V8m] : ( mem(V8m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V9lol] : ( mem(V9lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) => ( p(ap(ap(ap(V0P,V6cmp),ap(ap(ap(c_2Efmapal_2Emerge(A_27a,A_27b),V6cmp),V7l),V8m)),V9lol)) => p(ap(ap(ap(V0P,V6cmp),V7l),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),ap(c_2Eoption_2ESOME(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))),V8m)),V9lol))) ) ) ) ) ) ) ) => ! [V10v] : ( mem(V10v,ty_2Etoto_2Etoto(A_27a)) => ! [V11v1] : ( mem(V11v1,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V12v2] : ( mem(V12v2,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) => p(ap(ap(ap(V0P,V10v),V11v1),V12v2)) ) ) ) ) ))))).
fof(conj_thm_2Efmapal_2Emerge__out,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Efmapal_2Emerge__out(A_27a,A_27b),V1cmp),V0l),c_2Elist_2ENIL(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) = V0l ) ) ) ) & ( ( ! [V2lol] : ( mem(V2lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) => ! [V3l] : ( mem(V3l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V4cmp] : ( mem(V4cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Efmapal_2Emerge__out(A_27a,A_27b),V4cmp),V3l),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),c_2Eoption_2ENONE(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),V2lol)) = ap(ap(ap(c_2Efmapal_2Emerge__out(A_27a,A_27b),V4cmp),V3l),V2lol) ) ) ) ) ) & ! [V5m] : ( mem(V5m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V6lol] : ( mem(V6lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) => ! [V7l] : ( mem(V7l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V8cmp] : ( mem(V8cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Efmapal_2Emerge__out(A_27a,A_27b),V8cmp),V7l),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))),ap(c_2Eoption_2ESOME(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))),V5m)),V6lol)) = ap(ap(ap(c_2Efmapal_2Emerge__out(A_27a,A_27b),V8cmp),ap(ap(ap(c_2Efmapal_2Emerge(A_27a,A_27b),V8cmp),V7l),V5m)),V6lol) ) ) ) ) ) ) ))))).
fof(ax_thm_2Efmapal_2Eincr__flat,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1lol] : ( mem(V1lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) => ( ap(ap(c_2Efmapal_2Eincr__flat(A_27a,A_27b),V0cmp),V1lol) = ap(ap(ap(c_2Efmapal_2Emerge__out(A_27a,A_27b),V0cmp),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))),V1lol) ) ) ) ) ) )).
fof(ax_thm_2Efmapal_2Eincr__sort,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ap(ap(c_2Efmapal_2Eincr__sort(A_27a,A_27b),V0cmp),V1l) = ap(ap(ap(c_2Efmapal_2Emerge__out(A_27a,A_27b),V0cmp),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))),ap(ap(c_2Efmapal_2Eincr__build(A_27a,A_27b),V0cmp),V1l)) ) ) ) ) ) )).
fof(ax_thm_2Efmapal_2EOPTION__FLAT__primitive,axiom,( ! [A_27z] : ( ne(A_27z) => ( c_2Efmapal_2EOPTION__FLAT(A_27z) = ap(ap(c_2Erelation_2EWFREC(ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27z))),ty_2Elist_2Elist(A_27z)),ap(c_2Emin_2E_40(arr(ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27z))),arr(ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27z))),bool))),f2620(A_27z))),f2625(A_27z)) ) ) )).
fof(conj_thm_2Efmapal_2EOPTION__FLAT__ind,lemma,( ! [A_27z]: ( ne(A_27z) => ! [V0P] : ( mem(V0P,arr(ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27z))),bool)) => ( ( p(ap(V0P,c_2Elist_2ENIL(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27z))))) & ( ( ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27z)))) => ( p(ap(V0P,V1l)) => p(ap(V0P,ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27z))),c_2Eoption_2ENONE(ty_2Elist_2Elist(A_27z))),V1l))) ) ) ) & ! [V2a] : ( mem(V2a,ty_2Elist_2Elist(A_27z)) => ! [V3l] : ( mem(V3l,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27z)))) => ( p(ap(V0P,V3l)) => p(ap(V0P,ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27z))),ap(c_2Eoption_2ESOME(ty_2Elist_2Elist(A_27z)),V2a)),V3l))) ) ) ) ) ) => ! [V4v] : ( mem(V4v,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27z)))) => p(ap(V0P,V4v)) ) ) )))).
fof(conj_thm_2Efmapal_2EOPTION__FLAT,lemma,( ! [A_27z]: ( ne(A_27z) => ( ( ap(c_2Efmapal_2EOPTION__FLAT(A_27z),c_2Elist_2ENIL(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27z)))) = c_2Elist_2ENIL(A_27z) ) & ( ( ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27z)))) => ( ap(c_2Efmapal_2EOPTION__FLAT(A_27z),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27z))),c_2Eoption_2ENONE(ty_2Elist_2Elist(A_27z))),V0l)) = ap(c_2Efmapal_2EOPTION__FLAT(A_27z),V0l) ) ) ) & ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27z)))) => ! [V2a] : ( mem(V2a,ty_2Elist_2Elist(A_27z)) => ( ap(c_2Efmapal_2EOPTION__FLAT(A_27z),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27z))),ap(c_2Eoption_2ESOME(ty_2Elist_2Elist(A_27z)),V2a)),V1l)) = ap(ap(c_2Elist_2EAPPEND(A_27z),V2a),ap(c_2Efmapal_2EOPTION__FLAT(A_27z),V1l)) ) ) ) ) )))).
fof(ax_thm_2Efmapal_2Eunlookup,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,ty_2Eoption_2Eoption(A_27b))) => ( ap(c_2Efmapal_2Eunlookup(A_27a,A_27b),V0f) = ap(ap(c_2Efinite__map_2EFUN__FMAP(A_27a,A_27b),ap(ap(c_2Ecombin_2Eo(A_27a,A_27b,ty_2Eoption_2Eoption(A_27b)),c_2Eoption_2ETHE(A_27b)),V0f)),ap(ap(c_2Ecombin_2Eo(A_27a,bool,ty_2Eoption_2Eoption(A_27b)),c_2Eoption_2EIS__SOME(A_27b)),V0f)) ) ) ) ) )).
fof(conj_thm_2Efmapal_2Ebt__to__fmap__ind,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),bool))) => ( ( ( ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => p(ap(ap(V0P,V1cmp),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b)))) ) ) & ! [V2cmp] : ( mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V3l] : ( mem(V3l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V4x] : ( mem(V4x,A_27a) => ! [V5v] : ( mem(V5v,A_27b) => ! [V6r] : ( mem(V6r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ( p(ap(ap(V0P,V2cmp),V3l)) & p(ap(ap(V0P,V2cmp),V6r)) ) => p(ap(ap(V0P,V2cmp),ap(ap(ap(c_2Eenumeral_2Enode(ty_2Epair_2Eprod(A_27a,A_27b)),V3l),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V4x),V5v)),V6r))) ) ) ) ) ) ) ) => ! [V7v] : ( mem(V7v,ty_2Etoto_2Etoto(A_27a)) => ! [V8v1] : ( mem(V8v1,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(V0P,V7v),V8v1)) ) ) ) ))))).
fof(conj_thm_2Efmapal_2Ebt__to__fmap,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(c_2Efmapal_2EFMAPAL(A_27a,A_27b),V0cmp),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b))) = c_2Efinite__map_2EFEMPTY(A_27a,A_27b) ) ) ) & ! [V1x] : ( mem(V1x,A_27a) => ! [V2v] : ( mem(V2v,A_27b) => ! [V3r] : ( mem(V3r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V4l] : ( mem(V4l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V5cmp] : ( mem(V5cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(c_2Efmapal_2EFMAPAL(A_27a,A_27b),V5cmp),ap(ap(ap(c_2Eenumeral_2Enode(ty_2Epair_2Eprod(A_27a,A_27b)),V4l),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V1x),V2v)),V3r)) = ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),ap(ap(c_2Efmapal_2EFMAPAL(A_27a,A_27b),V5cmp),V4l)),ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f2626(A_27a,V1x,V5cmp)))),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),V1x),V2v)))),ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),ap(ap(c_2Efmapal_2EFMAPAL(A_27a,A_27b),V5cmp),V3r)),ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f2627(A_27a,V5cmp,V1x)))) ) ) ) ) ) ) ))))).
fof(conj_thm_2Efmapal_2EFAPPLY__nt,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1x] : ( mem(V1x,A_27a) => ( ap(ap(c_2Efinite__map_2EFAPPLY(A_27a,A_27b),ap(ap(c_2Efmapal_2EFMAPAL(A_27a,A_27b),V0cmp),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b)))),V1x) = ap(ap(c_2Efinite__map_2EFAPPLY(A_27a,A_27b),c_2Efinite__map_2EFEMPTY(A_27a,A_27b)),V1x) ) ) ))))).
fof(conj_thm_2Efmapal_2EFAPPLY__node,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2l] : ( mem(V2l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V3a] : ( mem(V3a,A_27a) => ! [V4b] : ( mem(V4b,A_27b) => ! [V5r] : ( mem(V5r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ap(ap(c_2Efinite__map_2EFAPPLY(A_27a,A_27b),ap(ap(c_2Efmapal_2EFMAPAL(A_27a,A_27b),V0cmp),ap(ap(ap(c_2Eenumeral_2Enode(ty_2Epair_2Eprod(A_27a,A_27b)),V2l),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V3a),V4b)),V5r))),V1x) = ap(ap(ap(ap(c_2EternaryComparisons_2Eordering__CASE(A_27b),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0cmp),V1x),V3a)),ap(ap(c_2Efinite__map_2EFAPPLY(A_27a,A_27b),ap(ap(c_2Efmapal_2EFMAPAL(A_27a,A_27b),V0cmp),V2l)),V1x)),V4b),ap(ap(c_2Efinite__map_2EFAPPLY(A_27a,A_27b),ap(ap(c_2Efmapal_2EFMAPAL(A_27a,A_27b),V0cmp),V5r)),V1x)) ) ) ) ) ) ) ))))).
fof(ax_thm_2Efmapal_2Ebt__to__fmap__lb,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1lb] : ( mem(V1lb,A_27a) => ! [V2t] : ( mem(V2t,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ap(ap(ap(c_2Efmapal_2Ebt__to__fmap__lb(A_27a,A_27b),V0cmp),V1lb),V2t) = ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),ap(ap(c_2Efmapal_2EFMAPAL(A_27a,A_27b),V0cmp),V2t)),ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f2628(A_27a,V0cmp,V1lb))) ) ) ) ) ) ) )).
fof(ax_thm_2Efmapal_2Ebt__to__fmap__ub,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1t] : ( mem(V1t,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V2ub] : ( mem(V2ub,A_27a) => ( ap(ap(ap(c_2Efmapal_2Ebt__to__fmap__ub(A_27a,A_27b),V0cmp),V1t),V2ub) = ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),ap(ap(c_2Efmapal_2EFMAPAL(A_27a,A_27b),V0cmp),V1t)),ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f2629(A_27a,V2ub,V0cmp))) ) ) ) ) ) ) )).
fof(ax_thm_2Efmapal_2Ebt__to__fmap__lb__ub,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1lb] : ( mem(V1lb,A_27a) => ! [V2t] : ( mem(V2t,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V3ub] : ( mem(V3ub,A_27a) => ( ap(ap(ap(ap(c_2Efmapal_2Ebt__to__fmap__lb__ub(A_27a,A_27b),V0cmp),V1lb),V2t),V3ub) = ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),ap(ap(c_2Efmapal_2EFMAPAL(A_27a,A_27b),V0cmp),V2t)),ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f2630(A_27a,V3ub,V0cmp,V1lb))) ) ) ) ) ) ) ) )).
fof(ax_thm_2Efmapal_2Ebt__map,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( ( ! [V0f] : ( mem(V0f,arr(A_27a,A_27b)) => ( ap(ap(c_2Efmapal_2Ebt__map(A_27a,A_27b),V0f),c_2Eenumeral_2Ent(A_27a)) = c_2Eenumeral_2Ent(A_27b) ) ) ) & ! [V1f] : ( mem(V1f,arr(A_27a,A_27b)) => ! [V2l] : ( mem(V2l,ty_2Eenumeral_2Ebt(A_27a)) => ! [V3x] : ( mem(V3x,A_27a) => ! [V4r] : ( mem(V4r,ty_2Eenumeral_2Ebt(A_27a)) => ( ap(ap(c_2Efmapal_2Ebt__map(A_27a,A_27b),V1f),ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V2l),V3x),V4r)) = ap(ap(ap(c_2Eenumeral_2Enode(A_27b),ap(ap(c_2Efmapal_2Ebt__map(A_27a,A_27b),V1f),V2l)),ap(V1f,V3x)),ap(ap(c_2Efmapal_2Ebt__map(A_27a,A_27b),V1f),V4r)) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Efmapal_2Ebt__FST__FDOM,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1t] : ( mem(V1t,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),ap(ap(c_2Efmapal_2EFMAPAL(A_27a,A_27b),V0cmp),V1t)) = ap(ap(c_2Eenumeral_2EENUMERAL(A_27a),V0cmp),ap(ap(c_2Efmapal_2Ebt__map(ty_2Epair_2Eprod(A_27a,A_27b),A_27a),c_2Epair_2EFST(A_27a,A_27b)),V1t)) ) ) ))))).
fof(conj_thm_2Efmapal_2Ebt__to__orl__lb__ub__ind,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),arr(A_27a,bool))))) => ( ( ( ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V2lb] : ( mem(V2lb,A_27a) => ! [V3ub] : ( mem(V3ub,A_27a) => p(ap(ap(ap(ap(V0P,V1cmp),V2lb),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b))),V3ub)) ) ) ) ) & ! [V4cmp] : ( mem(V4cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V5lb] : ( mem(V5lb,A_27a) => ! [V6l] : ( mem(V6l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V7x] : ( mem(V7x,A_27a) => ! [V8y] : ( mem(V8y,A_27b) => ! [V9r] : ( mem(V9r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V10ub] : ( mem(V10ub,A_27a) => ( ( ( ( ~~ ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4cmp),V5lb),V7x) = c_2EternaryComparisons_2ELESS ) ) => p(ap(ap(ap(ap(V0P,V4cmp),V5lb),V9r),V10ub)) ) & ( ( ( ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4cmp),V5lb),V7x) = c_2EternaryComparisons_2ELESS ) & ( ~~ ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4cmp),V7x),V10ub) = c_2EternaryComparisons_2ELESS ) ) ) => p(ap(ap(ap(ap(V0P,V4cmp),V5lb),V6l),V10ub)) ) & ( ( ( ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4cmp),V5lb),V7x) = c_2EternaryComparisons_2ELESS ) & ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4cmp),V7x),V10ub) = c_2EternaryComparisons_2ELESS ) ) => p(ap(ap(ap(ap(V0P,V4cmp),V5lb),V6l),V7x)) ) & ( ( ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4cmp),V5lb),V7x) = c_2EternaryComparisons_2ELESS ) & ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4cmp),V7x),V10ub) = c_2EternaryComparisons_2ELESS ) ) => p(ap(ap(ap(ap(V0P,V4cmp),V7x),V9r),V10ub)) ) ) ) ) => p(ap(ap(ap(ap(V0P,V4cmp),V5lb),ap(ap(ap(c_2Eenumeral_2Enode(ty_2Epair_2Eprod(A_27a,A_27b)),V6l),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V7x),V8y)),V9r)),V10ub)) ) ) ) ) ) ) ) ) ) => ! [V11v] : ( mem(V11v,ty_2Etoto_2Etoto(A_27a)) => ! [V12v1] : ( mem(V12v1,A_27a) => ! [V13v2] : ( mem(V13v2,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V14v3] : ( mem(V14v3,A_27a) => p(ap(ap(ap(ap(V0P,V11v),V12v1),V13v2),V14v3)) ) ) ) ) ) ))))).
fof(conj_thm_2Efmapal_2Ebt__to__orl__lb__ub,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0ub] : ( mem(V0ub,A_27a) => ! [V1lb] : ( mem(V1lb,A_27a) => ! [V2cmp] : ( mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb__ub(A_27a,A_27b),V2cmp),V1lb),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b))),V0ub) = c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b)) ) ) ) ) ) & ! [V3y] : ( mem(V3y,A_27b) => ! [V4x] : ( mem(V4x,A_27a) => ! [V5ub] : ( mem(V5ub,A_27a) => ! [V6r] : ( mem(V6r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V7lb] : ( mem(V7lb,A_27a) => ! [V8l] : ( mem(V8l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V9cmp] : ( mem(V9cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb__ub(A_27a,A_27b),V9cmp),V7lb),ap(ap(ap(c_2Eenumeral_2Enode(ty_2Epair_2Eprod(A_27a,A_27b)),V8l),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V4x),V3y)),V6r)),V5ub) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))),ap(ap(c_2Emin_2E_3D(ty_2EternaryComparisons_2Eordering),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V9cmp),V7lb),V4x)),c_2EternaryComparisons_2ELESS)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))),ap(ap(c_2Emin_2E_3D(ty_2EternaryComparisons_2Eordering),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V9cmp),V4x),V5ub)),c_2EternaryComparisons_2ELESS)),ap(ap(c_2Elist_2EAPPEND(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Elist_2EAPPEND(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb__ub(A_27a,A_27b),V9cmp),V7lb),V8l),V4x)),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V4x),V3y)),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))))),ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb__ub(A_27a,A_27b),V9cmp),V4x),V6r),V5ub))),ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb__ub(A_27a,A_27b),V9cmp),V7lb),V8l),V5ub))),ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb__ub(A_27a,A_27b),V9cmp),V7lb),V6r),V5ub)) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Efmapal_2Ebt__to__orl__lb__ind,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),bool)))) => ( ( ( ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V2lb] : ( mem(V2lb,A_27a) => p(ap(ap(ap(V0P,V1cmp),V2lb),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b)))) ) ) ) & ! [V3cmp] : ( mem(V3cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V4lb] : ( mem(V4lb,A_27a) => ! [V5l] : ( mem(V5l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V6x] : ( mem(V6x,A_27a) => ! [V7y] : ( mem(V7y,A_27b) => ! [V8r] : ( mem(V8r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ( ( ( ~~ ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V3cmp),V4lb),V6x) = c_2EternaryComparisons_2ELESS ) ) => p(ap(ap(ap(V0P,V3cmp),V4lb),V8r)) ) & ( ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V3cmp),V4lb),V6x) = c_2EternaryComparisons_2ELESS ) => p(ap(ap(ap(V0P,V3cmp),V6x),V8r)) ) ) => p(ap(ap(ap(V0P,V3cmp),V4lb),ap(ap(ap(c_2Eenumeral_2Enode(ty_2Epair_2Eprod(A_27a,A_27b)),V5l),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V6x),V7y)),V8r))) ) ) ) ) ) ) ) ) => ! [V9v] : ( mem(V9v,ty_2Etoto_2Etoto(A_27a)) => ! [V10v1] : ( mem(V10v1,A_27a) => ! [V11v2] : ( mem(V11v2,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(ap(V0P,V9v),V10v1),V11v2)) ) ) ) ) ))))).
fof(conj_thm_2Efmapal_2Ebt__to__orl__lb,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0lb] : ( mem(V0lb,A_27a) => ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb(A_27a,A_27b),V1cmp),V0lb),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b))) = c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b)) ) ) ) ) & ! [V2y] : ( mem(V2y,A_27b) => ! [V3x] : ( mem(V3x,A_27a) => ! [V4r] : ( mem(V4r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V5lb] : ( mem(V5lb,A_27a) => ! [V6l] : ( mem(V6l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V7cmp] : ( mem(V7cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb(A_27a,A_27b),V7cmp),V5lb),ap(ap(ap(c_2Eenumeral_2Enode(ty_2Epair_2Eprod(A_27a,A_27b)),V6l),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V3x),V2y)),V4r)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))),ap(ap(c_2Emin_2E_3D(ty_2EternaryComparisons_2Eordering),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V7cmp),V5lb),V3x)),c_2EternaryComparisons_2ELESS)),ap(ap(c_2Elist_2EAPPEND(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Elist_2EAPPEND(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb__ub(A_27a,A_27b),V7cmp),V5lb),V6l),V3x)),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V3x),V2y)),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))))),ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb(A_27a,A_27b),V7cmp),V3x),V4r))),ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb(A_27a,A_27b),V7cmp),V5lb),V4r)) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Efmapal_2Ebt__to__orl__ub__ind,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),arr(A_27a,bool)))) => ( ( ( ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V2ub] : ( mem(V2ub,A_27a) => p(ap(ap(ap(V0P,V1cmp),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b))),V2ub)) ) ) ) & ! [V3cmp] : ( mem(V3cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V4l] : ( mem(V4l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V5x] : ( mem(V5x,A_27a) => ! [V6y] : ( mem(V6y,A_27b) => ! [V7r] : ( mem(V7r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V8ub] : ( mem(V8ub,A_27a) => ( ( ( ( ~~ ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V3cmp),V5x),V8ub) = c_2EternaryComparisons_2ELESS ) ) => p(ap(ap(ap(V0P,V3cmp),V4l),V8ub)) ) & ( ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V3cmp),V5x),V8ub) = c_2EternaryComparisons_2ELESS ) => p(ap(ap(ap(V0P,V3cmp),V4l),V5x)) ) ) => p(ap(ap(ap(V0P,V3cmp),ap(ap(ap(c_2Eenumeral_2Enode(ty_2Epair_2Eprod(A_27a,A_27b)),V4l),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V5x),V6y)),V7r)),V8ub)) ) ) ) ) ) ) ) ) => ! [V9v] : ( mem(V9v,ty_2Etoto_2Etoto(A_27a)) => ! [V10v1] : ( mem(V10v1,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V11v2] : ( mem(V11v2,A_27a) => p(ap(ap(ap(V0P,V9v),V10v1),V11v2)) ) ) ) ) ))))).
fof(conj_thm_2Efmapal_2Ebt__to__orl__ub,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0ub] : ( mem(V0ub,A_27a) => ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Efmapal_2Ebt__to__orl__ub(A_27a,A_27b),V1cmp),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b))),V0ub) = c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b)) ) ) ) ) & ! [V2y] : ( mem(V2y,A_27b) => ! [V3x] : ( mem(V3x,A_27a) => ! [V4ub] : ( mem(V4ub,A_27a) => ! [V5r] : ( mem(V5r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V6l] : ( mem(V6l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V7cmp] : ( mem(V7cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Efmapal_2Ebt__to__orl__ub(A_27a,A_27b),V7cmp),ap(ap(ap(c_2Eenumeral_2Enode(ty_2Epair_2Eprod(A_27a,A_27b)),V6l),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V3x),V2y)),V5r)),V4ub) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))),ap(ap(c_2Emin_2E_3D(ty_2EternaryComparisons_2Eordering),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V7cmp),V3x),V4ub)),c_2EternaryComparisons_2ELESS)),ap(ap(c_2Elist_2EAPPEND(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Elist_2EAPPEND(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(ap(c_2Efmapal_2Ebt__to__orl__ub(A_27a,A_27b),V7cmp),V6l),V3x)),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V3x),V2y)),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))))),ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb__ub(A_27a,A_27b),V7cmp),V3x),V5r),V4ub))),ap(ap(ap(c_2Efmapal_2Ebt__to__orl__ub(A_27a,A_27b),V7cmp),V6l),V4ub)) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Efmapal_2Ebt__to__orl__ind,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),bool))) => ( ( ( ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => p(ap(ap(V0P,V1cmp),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b)))) ) ) & ! [V2cmp] : ( mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V3l] : ( mem(V3l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V4x] : ( mem(V4x,A_27a) => ! [V5y] : ( mem(V5y,A_27b) => ! [V6r] : ( mem(V6r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(V0P,V2cmp),ap(ap(ap(c_2Eenumeral_2Enode(ty_2Epair_2Eprod(A_27a,A_27b)),V3l),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V4x),V5y)),V6r))) ) ) ) ) ) ) => ! [V7v] : ( mem(V7v,ty_2Etoto_2Etoto(A_27a)) => ! [V8v1] : ( mem(V8v1,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(V0P,V7v),V8v1)) ) ) ) ))))).
fof(conj_thm_2Efmapal_2Ebt__to__orl,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1l] : ( mem(V1l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( mem(V3y,A_27b) => ! [V4r] : ( mem(V4r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ( ap(ap(c_2Efmapal_2Ebt__to__orl(A_27a,A_27b),V0cmp),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b))) = c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b)) ) & ( ap(ap(c_2Efmapal_2Ebt__to__orl(A_27a,A_27b),V0cmp),ap(ap(ap(c_2Eenumeral_2Enode(ty_2Epair_2Eprod(A_27a,A_27b)),V1l),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2x),V3y)),V4r)) = ap(ap(c_2Elist_2EAPPEND(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Elist_2EAPPEND(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(ap(c_2Efmapal_2Ebt__to__orl__ub(A_27a,A_27b),V0cmp),V1l),V2x)),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2x),V3y)),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))))),ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb(A_27a,A_27b),V0cmp),V2x),V4r)) ) ) ) ) ) ) ))))).
fof(ax_thm_2Efmapal_2Efmap,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ap(c_2Efmapal_2Efmap(A_27a,A_27b),V0l) = ap(ap(c_2Efinite__map_2EFUPDATE__LIST(A_27a,A_27b),c_2Efinite__map_2EFEMPTY(A_27a,A_27b)),ap(c_2Elist_2EREVERSE(ty_2Epair_2Eprod(A_27a,A_27b)),V0l)) ) ) ) ) )).
fof(ax_thm_2Efmapal_2Ebt__to__orl__lb__ub__ac__tupled__AUX,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0R] : ( mem(V0R,arr(ty_2Epair_2Eprod(ty_2Etoto_2Etoto(A_27a),ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))))),arr(ty_2Epair_2Eprod(ty_2Etoto_2Etoto(A_27a),ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))))),bool))) => ( ap(c_2Efmapal_2Ebt__to__orl__lb__ub__ac__tupled__aux(A_27a,A_27b),V0R) = ap(ap(c_2Erelation_2EWFREC(ty_2Epair_2Eprod(ty_2Etoto_2Etoto(A_27a),ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))))),ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))),V0R),f2645(A_27b,A_27a)) ) ) ) ) )).
fof(conj_thm_2Efmapal_2Ebt__to__orl__lb__ub__ac__ind,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),arr(A_27a,arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),bool)))))) => ( ( ( ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V2lb] : ( mem(V2lb,A_27a) => ! [V3ub] : ( mem(V3ub,A_27a) => ! [V4m] : ( mem(V4m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(ap(ap(ap(V0P,V1cmp),V2lb),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b))),V3ub),V4m)) ) ) ) ) ) & ! [V5cmp] : ( mem(V5cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V6lb] : ( mem(V6lb,A_27a) => ! [V7l] : ( mem(V7l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V8x] : ( mem(V8x,A_27a) => ! [V9y] : ( mem(V9y,A_27b) => ! [V10r] : ( mem(V10r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V11ub] : ( mem(V11ub,A_27a) => ! [V12m] : ( mem(V12m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ( ( ( ~~ ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V5cmp),V6lb),V8x) = c_2EternaryComparisons_2ELESS ) ) => p(ap(ap(ap(ap(ap(V0P,V5cmp),V6lb),V10r),V11ub),V12m)) ) & ( ( ( ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V5cmp),V6lb),V8x) = c_2EternaryComparisons_2ELESS ) & ( ~~ ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V5cmp),V8x),V11ub) = c_2EternaryComparisons_2ELESS ) ) ) => p(ap(ap(ap(ap(ap(V0P,V5cmp),V6lb),V7l),V11ub),V12m)) ) & ( ( ( ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V5cmp),V6lb),V8x) = c_2EternaryComparisons_2ELESS ) & ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V5cmp),V8x),V11ub) = c_2EternaryComparisons_2ELESS ) ) => p(ap(ap(ap(ap(ap(V0P,V5cmp),V6lb),V7l),V8x),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V8x),V9y)),ap(ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb__ub__ac(A_27a,A_27b),V5cmp),V8x),V10r),V11ub),V12m)))) ) & ( ( ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V5cmp),V6lb),V8x) = c_2EternaryComparisons_2ELESS ) & ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V5cmp),V8x),V11ub) = c_2EternaryComparisons_2ELESS ) ) => p(ap(ap(ap(ap(ap(V0P,V5cmp),V8x),V10r),V11ub),V12m)) ) ) ) ) => p(ap(ap(ap(ap(ap(V0P,V5cmp),V6lb),ap(ap(ap(c_2Eenumeral_2Enode(ty_2Epair_2Eprod(A_27a,A_27b)),V7l),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V8x),V9y)),V10r)),V11ub),V12m)) ) ) ) ) ) ) ) ) ) ) => ! [V13v] : ( mem(V13v,ty_2Etoto_2Etoto(A_27a)) => ! [V14v1] : ( mem(V14v1,A_27a) => ! [V15v2] : ( mem(V15v2,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V16v3] : ( mem(V16v3,A_27a) => ! [V17v4] : ( mem(V17v4,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(ap(ap(ap(V0P,V13v),V14v1),V15v2),V16v3),V17v4)) ) ) ) ) ) ) ))))).
fof(conj_thm_2Efmapal_2Ebt__to__orl__lb__ub__ac,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0ub] : ( mem(V0ub,A_27a) => ! [V1m] : ( mem(V1m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V2lb] : ( mem(V2lb,A_27a) => ! [V3cmp] : ( mem(V3cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb__ub__ac(A_27a,A_27b),V3cmp),V2lb),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b))),V0ub),V1m) = V1m ) ) ) ) ) ) & ! [V4y] : ( mem(V4y,A_27b) => ! [V5x] : ( mem(V5x,A_27a) => ! [V6ub] : ( mem(V6ub,A_27a) => ! [V7r] : ( mem(V7r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V8m] : ( mem(V8m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V9lb] : ( mem(V9lb,A_27a) => ! [V10l] : ( mem(V10l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V11cmp] : ( mem(V11cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb__ub__ac(A_27a,A_27b),V11cmp),V9lb),ap(ap(ap(c_2Eenumeral_2Enode(ty_2Epair_2Eprod(A_27a,A_27b)),V10l),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V5x),V4y)),V7r)),V6ub),V8m) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))),ap(ap(c_2Emin_2E_3D(ty_2EternaryComparisons_2Eordering),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V11cmp),V9lb),V5x)),c_2EternaryComparisons_2ELESS)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))),ap(ap(c_2Emin_2E_3D(ty_2EternaryComparisons_2Eordering),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V11cmp),V5x),V6ub)),c_2EternaryComparisons_2ELESS)),ap(ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb__ub__ac(A_27a,A_27b),V11cmp),V9lb),V10l),V5x),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V5x),V4y)),ap(ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb__ub__ac(A_27a,A_27b),V11cmp),V5x),V7r),V6ub),V8m)))),ap(ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb__ub__ac(A_27a,A_27b),V11cmp),V9lb),V10l),V6ub),V8m))),ap(ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb__ub__ac(A_27a,A_27b),V11cmp),V9lb),V7r),V6ub),V8m)) ) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Efmapal_2Ebt__to__orl__lb__ac__ind,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),bool))))) => ( ( ( ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V2lb] : ( mem(V2lb,A_27a) => ! [V3m] : ( mem(V3m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(ap(ap(V0P,V1cmp),V2lb),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b))),V3m)) ) ) ) ) & ! [V4cmp] : ( mem(V4cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V5lb] : ( mem(V5lb,A_27a) => ! [V6l] : ( mem(V6l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V7x] : ( mem(V7x,A_27a) => ! [V8y] : ( mem(V8y,A_27b) => ! [V9r] : ( mem(V9r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V10m] : ( mem(V10m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ( ( ( ~~ ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4cmp),V5lb),V7x) = c_2EternaryComparisons_2ELESS ) ) => p(ap(ap(ap(ap(V0P,V4cmp),V5lb),V9r),V10m)) ) & ( ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4cmp),V5lb),V7x) = c_2EternaryComparisons_2ELESS ) => p(ap(ap(ap(ap(V0P,V4cmp),V7x),V9r),V10m)) ) ) => p(ap(ap(ap(ap(V0P,V4cmp),V5lb),ap(ap(ap(c_2Eenumeral_2Enode(ty_2Epair_2Eprod(A_27a,A_27b)),V6l),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V7x),V8y)),V9r)),V10m)) ) ) ) ) ) ) ) ) ) => ! [V11v] : ( mem(V11v,ty_2Etoto_2Etoto(A_27a)) => ! [V12v1] : ( mem(V12v1,A_27a) => ! [V13v2] : ( mem(V13v2,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V14v3] : ( mem(V14v3,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(ap(ap(V0P,V11v),V12v1),V13v2),V14v3)) ) ) ) ) ) ))))).
fof(conj_thm_2Efmapal_2Ebt__to__orl__lb__ac,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0m] : ( mem(V0m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V1lb] : ( mem(V1lb,A_27a) => ! [V2cmp] : ( mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb__ac(A_27a,A_27b),V2cmp),V1lb),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b))),V0m) = V0m ) ) ) ) ) & ! [V3y] : ( mem(V3y,A_27b) => ! [V4x] : ( mem(V4x,A_27a) => ! [V5r] : ( mem(V5r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V6m] : ( mem(V6m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V7lb] : ( mem(V7lb,A_27a) => ! [V8l] : ( mem(V8l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V9cmp] : ( mem(V9cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb__ac(A_27a,A_27b),V9cmp),V7lb),ap(ap(ap(c_2Eenumeral_2Enode(ty_2Epair_2Eprod(A_27a,A_27b)),V8l),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V4x),V3y)),V5r)),V6m) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))),ap(ap(c_2Emin_2E_3D(ty_2EternaryComparisons_2Eordering),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V9cmp),V7lb),V4x)),c_2EternaryComparisons_2ELESS)),ap(ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb__ub__ac(A_27a,A_27b),V9cmp),V7lb),V8l),V4x),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V4x),V3y)),ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb__ac(A_27a,A_27b),V9cmp),V4x),V5r),V6m)))),ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb__ac(A_27a,A_27b),V9cmp),V7lb),V5r),V6m)) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Efmapal_2Ebt__to__orl__ub__ac__ind,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),arr(A_27a,arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),bool))))) => ( ( ( ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V2ub] : ( mem(V2ub,A_27a) => ! [V3m] : ( mem(V3m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(ap(ap(V0P,V1cmp),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b))),V2ub),V3m)) ) ) ) ) & ! [V4cmp] : ( mem(V4cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V5l] : ( mem(V5l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V6x] : ( mem(V6x,A_27a) => ! [V7y] : ( mem(V7y,A_27b) => ! [V8r] : ( mem(V8r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V9ub] : ( mem(V9ub,A_27a) => ! [V10m] : ( mem(V10m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ( ( ( ~~ ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4cmp),V6x),V9ub) = c_2EternaryComparisons_2ELESS ) ) => p(ap(ap(ap(ap(V0P,V4cmp),V5l),V9ub),V10m)) ) & ( ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4cmp),V6x),V9ub) = c_2EternaryComparisons_2ELESS ) => p(ap(ap(ap(ap(V0P,V4cmp),V5l),V6x),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V6x),V7y)),ap(ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb__ub__ac(A_27a,A_27b),V4cmp),V6x),V8r),V9ub),V10m)))) ) ) => p(ap(ap(ap(ap(V0P,V4cmp),ap(ap(ap(c_2Eenumeral_2Enode(ty_2Epair_2Eprod(A_27a,A_27b)),V5l),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V6x),V7y)),V8r)),V9ub),V10m)) ) ) ) ) ) ) ) ) ) => ! [V11v] : ( mem(V11v,ty_2Etoto_2Etoto(A_27a)) => ! [V12v1] : ( mem(V12v1,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V13v2] : ( mem(V13v2,A_27a) => ! [V14v3] : ( mem(V14v3,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(ap(ap(V0P,V11v),V12v1),V13v2),V14v3)) ) ) ) ) ) ))))).
fof(conj_thm_2Efmapal_2Ebt__to__orl__ub__ac,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0ub] : ( mem(V0ub,A_27a) => ! [V1m] : ( mem(V1m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V2cmp] : ( mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__ub__ac(A_27a,A_27b),V2cmp),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b))),V0ub),V1m) = V1m ) ) ) ) ) & ! [V3y] : ( mem(V3y,A_27b) => ! [V4x] : ( mem(V4x,A_27a) => ! [V5ub] : ( mem(V5ub,A_27a) => ! [V6r] : ( mem(V6r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V7m] : ( mem(V7m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V8l] : ( mem(V8l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V9cmp] : ( mem(V9cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__ub__ac(A_27a,A_27b),V9cmp),ap(ap(ap(c_2Eenumeral_2Enode(ty_2Epair_2Eprod(A_27a,A_27b)),V8l),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V4x),V3y)),V6r)),V5ub),V7m) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))),ap(ap(c_2Emin_2E_3D(ty_2EternaryComparisons_2Eordering),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V9cmp),V4x),V5ub)),c_2EternaryComparisons_2ELESS)),ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__ub__ac(A_27a,A_27b),V9cmp),V8l),V4x),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V4x),V3y)),ap(ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb__ub__ac(A_27a,A_27b),V9cmp),V4x),V6r),V5ub),V7m)))),ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__ub__ac(A_27a,A_27b),V9cmp),V8l),V5ub),V7m)) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Efmapal_2Ebt__to__orl__ac__ind,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),bool)))) => ( ( ( ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V2m] : ( mem(V2m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(ap(V0P,V1cmp),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b))),V2m)) ) ) ) & ! [V3cmp] : ( mem(V3cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V4l] : ( mem(V4l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V5x] : ( mem(V5x,A_27a) => ! [V6y] : ( mem(V6y,A_27b) => ! [V7r] : ( mem(V7r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V8m] : ( mem(V8m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(ap(V0P,V3cmp),ap(ap(ap(c_2Eenumeral_2Enode(ty_2Epair_2Eprod(A_27a,A_27b)),V4l),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V5x),V6y)),V7r)),V8m)) ) ) ) ) ) ) ) => ! [V9v] : ( mem(V9v,ty_2Etoto_2Etoto(A_27a)) => ! [V10v1] : ( mem(V10v1,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V11v2] : ( mem(V11v2,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(ap(V0P,V9v),V10v1),V11v2)) ) ) ) ) ))))).
fof(conj_thm_2Efmapal_2Ebt__to__orl__ac,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1m] : ( mem(V1m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V2l] : ( mem(V2l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V3x] : ( mem(V3x,A_27a) => ! [V4y] : ( mem(V4y,A_27b) => ! [V5r] : ( mem(V5r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ( ap(ap(ap(c_2Efmapal_2Ebt__to__orl__ac(A_27a,A_27b),V0cmp),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b))),V1m) = V1m ) & ( ap(ap(ap(c_2Efmapal_2Ebt__to__orl__ac(A_27a,A_27b),V0cmp),ap(ap(ap(c_2Eenumeral_2Enode(ty_2Epair_2Eprod(A_27a,A_27b)),V2l),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V3x),V4y)),V5r)),V1m) = ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__ub__ac(A_27a,A_27b),V0cmp),V2l),V3x),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V3x),V4y)),ap(ap(ap(ap(c_2Efmapal_2Ebt__to__orl__lb__ac(A_27a,A_27b),V0cmp),V3x),V5r),V1m))) ) ) ) ) ) ) ) ))))).
fof(ax_thm_2Efmapal_2EORWL,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1f] : ( mem(V1f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( p(ap(ap(ap(c_2Efmapal_2EORWL(A_27a,A_27b),V0cmp),V1f),V2l)) <=> ( ( V1f = ap(c_2Efmapal_2Efmap(A_27a,A_27b),V2l) ) & p(ap(ap(c_2Efmapal_2EORL(A_27a,A_27b),V0cmp),V2l)) ) ) ) ) ) ) ) )).
fof(conj_thm_2Efmapal_2EORWL__bt__to__orl,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1t] : ( mem(V1t,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(ap(c_2Efmapal_2EORWL(A_27a,A_27b),V0cmp),ap(ap(c_2Efmapal_2EFMAPAL(A_27a,A_27b),V0cmp),V1t)),ap(ap(c_2Efmapal_2Ebt__to__orl(A_27a,A_27b),V0cmp),V1t))) ) ))))).
fof(ax_thm_2Efmapal_2EOFU,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1f] : ( mem(V1f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V2g] : ( mem(V2g,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ap(ap(ap(c_2Efmapal_2EOFU(A_27a,A_27b),V0cmp),V1f),V2g) = ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),V1f),ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f2646(A_27b,A_27a,V2g,V0cmp)))),V2g) ) ) ) ) ) ) )).
fof(ax_thm_2Efmapal_2EUFO,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1f] : ( mem(V1f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ! [V2g] : ( mem(V2g,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ap(ap(ap(c_2Efmapal_2EUFO(A_27a,A_27b),V0cmp),V1f),V2g) = ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),V1f),ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),V2g),ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f2648(A_27b,A_27a,V0cmp,V1f)))) ) ) ) ) ) ) )).
fof(conj_thm_2Efmapal_2Ebl__to__fmap__ind,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebl(ty_2Epair_2Eprod(A_27a,A_27b)),bool))) => ( ( ( ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => p(ap(ap(V0P,V1cmp),c_2Eenumeral_2Enbl(ty_2Epair_2Eprod(A_27a,A_27b)))) ) ) & ( ( ! [V2cmp] : ( mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V3b] : ( mem(V3b,ty_2Eenumeral_2Ebl(ty_2Epair_2Eprod(A_27a,A_27b))) => ( p(ap(ap(V0P,V2cmp),V3b)) => p(ap(ap(V0P,V2cmp),ap(c_2Eenumeral_2Ezerbl(ty_2Epair_2Eprod(A_27a,A_27b)),V3b))) ) ) ) ) & ! [V4cmp] : ( mem(V4cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V5x] : ( mem(V5x,A_27a) => ! [V6y] : ( mem(V6y,A_27b) => ! [V7t] : ( mem(V7t,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V8b] : ( mem(V8b,ty_2Eenumeral_2Ebl(ty_2Epair_2Eprod(A_27a,A_27b))) => ( p(ap(ap(V0P,V4cmp),V8b)) => p(ap(ap(V0P,V4cmp),ap(ap(ap(c_2Eenumeral_2Eonebl(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V5x),V6y)),V7t),V8b))) ) ) ) ) ) ) ) ) => ! [V9v] : ( mem(V9v,ty_2Etoto_2Etoto(A_27a)) => ! [V10v1] : ( mem(V10v1,ty_2Eenumeral_2Ebl(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(V0P,V9v),V10v1)) ) ) ) ))))).
fof(conj_thm_2Efmapal_2Ebl__to__fmap,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(c_2Efmapal_2Ebl__to__fmap(A_27a,A_27b),V0cmp),c_2Eenumeral_2Enbl(ty_2Epair_2Eprod(A_27a,A_27b))) = c_2Efinite__map_2EFEMPTY(A_27a,A_27b) ) ) ) & ( ( ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V2b] : ( mem(V2b,ty_2Eenumeral_2Ebl(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ap(ap(c_2Efmapal_2Ebl__to__fmap(A_27a,A_27b),V1cmp),ap(c_2Eenumeral_2Ezerbl(ty_2Epair_2Eprod(A_27a,A_27b)),V2b)) = ap(ap(c_2Efmapal_2Ebl__to__fmap(A_27a,A_27b),V1cmp),V2b) ) ) ) ) & ! [V3y] : ( mem(V3y,A_27b) => ! [V4x] : ( mem(V4x,A_27a) => ! [V5t] : ( mem(V5t,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V6cmp] : ( mem(V6cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V7b] : ( mem(V7b,ty_2Eenumeral_2Ebl(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ap(ap(c_2Efmapal_2Ebl__to__fmap(A_27a,A_27b),V6cmp),ap(ap(ap(c_2Eenumeral_2Eonebl(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V4x),V3y)),V5t),V7b)) = ap(ap(ap(c_2Efmapal_2EOFU(A_27a,A_27b),V6cmp),ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),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),V4x),V3y))),ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),ap(ap(c_2Efmapal_2EFMAPAL(A_27a,A_27b),V6cmp),V5t)),ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f2649(A_27a,V6cmp,V4x))))),ap(ap(c_2Efmapal_2Ebl__to__fmap(A_27a,A_27b),V6cmp),V7b)) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Efmapal_2Ebt__to__orl__ID__IMP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( p(ap(ap(c_2Efmapal_2EORL(A_27a,A_27b),V0cmp),V1l)) => ( ap(ap(c_2Efmapal_2Ebt__to__orl(A_27a,A_27b),V0cmp),ap(c_2Eenumeral_2Elist__to__bt(ty_2Epair_2Eprod(A_27a,A_27b)),V1l)) = V1l ) ) ) ))))).
fof(conj_thm_2Efmapal_2Efmap__FDOM,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),ap(c_2Efmapal_2Efmap(A_27a,A_27b),V0l)) = 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)),V0l)) ) ))))).
fof(conj_thm_2Efmapal_2EORL__FUNION__IMP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( p(ap(ap(c_2Efmapal_2EORL(A_27a,A_27b),V0cmp),V1l)) => ! [V2m] : ( mem(V2m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( p(ap(ap(c_2Efmapal_2EORL(A_27a,A_27b),V0cmp),V2m)) => ( p(ap(ap(c_2Efmapal_2EORL(A_27a,A_27b),V0cmp),ap(ap(ap(c_2Efmapal_2Emerge(A_27a,A_27b),V0cmp),V1l),V2m))) & ( ap(c_2Efmapal_2Efmap(A_27a,A_27b),ap(ap(ap(c_2Efmapal_2Emerge(A_27a,A_27b),V0cmp),V1l),V2m)) = ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),ap(c_2Efmapal_2Efmap(A_27a,A_27b),V1l)),ap(c_2Efmapal_2Efmap(A_27a,A_27b),V2m)) ) ) ) ) ) ) ))))).
fof(conj_thm_2Efmapal_2EFMAPAL__FDOM__THM,conjecture,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1x] : ( mem(V1x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),ap(ap(c_2Efmapal_2EFMAPAL(A_27a,A_27b),V0cmp),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b)))))) <=> $false ) ) ) ) & ! [V2cmp] : ( mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V3x] : ( mem(V3x,A_27a) => ! [V4a] : ( mem(V4a,A_27a) => ! [V5b] : ( mem(V5b,A_27b) => ! [V6l] : ( mem(V6l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ! [V7r] : ( mem(V7r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V3x),ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),ap(ap(c_2Efmapal_2EFMAPAL(A_27a,A_27b),V2cmp),ap(ap(ap(c_2Eenumeral_2Enode(ty_2Epair_2Eprod(A_27a,A_27b)),V6l),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V4a),V5b)),V7r))))) <=> p(ap(ap(ap(ap(c_2EternaryComparisons_2Eordering__CASE(bool),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V2cmp),V3x),V4a)),ap(ap(c_2Ebool_2EIN(A_27a),V3x),ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),ap(ap(c_2Efmapal_2EFMAPAL(A_27a,A_27b),V2cmp),V6l)))),c_2Ebool_2ET),ap(ap(c_2Ebool_2EIN(A_27a),V3x),ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),ap(ap(c_2Efmapal_2EFMAPAL(A_27a,A_27b),V2cmp),V7r))))) ) ) ) ) ) ) ) ))))).
