include('Axioms/DeepSyntax_2.ax').
tff(tp_c_2Efmapal_2EAP__SND,type,(c_2Efmapal_2EAP__SND:(del * del * del) > $i)).
tff(mem_c_2Efmapal_2EAP__SND,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : 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)))))))).
tff(tp_c_2Efmapal_2EFMAPAL,type,(c_2Efmapal_2EFMAPAL:(del * del) > $i)).
tff(mem_c_2Efmapal_2EFMAPAL,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))).
tff(tp_c_2Efmapal_2EOFU,type,(c_2Efmapal_2EOFU:(del * del) > $i)).
tff(mem_c_2Efmapal_2EOFU,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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)))))))).
tff(tp_c_2Efmapal_2EOPTION__FLAT,type,(c_2Efmapal_2EOPTION__FLAT:del > $i)).
tff(mem_c_2Efmapal_2EOPTION__FLAT,axiom,( ! [A_27z:del] : mem(c_2Efmapal_2EOPTION__FLAT(A_27z),arr(ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27z))),ty_2Elist_2Elist(A_27z))))).
tff(tp_c_2Efmapal_2EOPTION__UPDATE,type,(c_2Efmapal_2EOPTION__UPDATE:(del * del) > $i)).
tff(mem_c_2Efmapal_2EOPTION__UPDATE,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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)))))))).
tff(tp_c_2Efmapal_2EORL,type,(c_2Efmapal_2EORL:(del * del) > $i)).
tff(mem_c_2Efmapal_2EORL,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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)))))).
tff(tp_c_2Efmapal_2EORL__bt,type,(c_2Efmapal_2EORL__bt:(del * del) > $i)).
tff(mem_c_2Efmapal_2EORL__bt,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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)))))).
tff(tp_c_2Efmapal_2EORL__bt__lb,type,(c_2Efmapal_2EORL__bt__lb:(del * del) > $i)).
tff(mem_c_2Efmapal_2EORL__bt__lb,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))).
tff(tp_c_2Efmapal_2EORL__bt__lb__ub,type,(c_2Efmapal_2EORL__bt__lb__ub:(del * del) > $i)).
tff(mem_c_2Efmapal_2EORL__bt__lb__ub,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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)))))))).
tff(tp_c_2Efmapal_2EORL__bt__ub,type,(c_2Efmapal_2EORL__bt__ub:(del * del) > $i)).
tff(mem_c_2Efmapal_2EORL__bt__ub,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))).
tff(tp_c_2Efmapal_2EORL__sublists,type,(c_2Efmapal_2EORL__sublists:(del * del) > $i)).
tff(mem_c_2Efmapal_2EORL__sublists,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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)))))).
tff(tp_c_2Efmapal_2EORWL,type,(c_2Efmapal_2EORWL:(del * del) > $i)).
tff(mem_c_2Efmapal_2EORWL,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))).
tff(tp_c_2Efmapal_2EUFO,type,(c_2Efmapal_2EUFO:(del * del) > $i)).
tff(mem_c_2Efmapal_2EUFO,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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)))))))).
tff(tp_c_2Efmapal_2Eassocv,type,(c_2Efmapal_2Eassocv:(del * del) > $i)).
tff(mem_c_2Efmapal_2Eassocv,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))).
tff(tp_c_2Efmapal_2Ebl__to__fmap,type,(c_2Efmapal_2Ebl__to__fmap:(del * del) > $i)).
tff(mem_c_2Efmapal_2Ebl__to__fmap,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))).
tff(tp_c_2Efmapal_2Ebt__map,type,(c_2Efmapal_2Ebt__map:(del * del) > $i)).
tff(mem_c_2Efmapal_2Ebt__map,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))).
tff(tp_c_2Efmapal_2Ebt__rplacv__cn,type,(c_2Efmapal_2Ebt__rplacv__cn:(del * del) > $i)).
tff(mem_c_2Efmapal_2Ebt__rplacv__cn,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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)))))))))).
tff(tp_c_2Efmapal_2Ebt__to__fmap__lb,type,(c_2Efmapal_2Ebt__to__fmap__lb:(del * del) > $i)).
tff(mem_c_2Efmapal_2Ebt__to__fmap__lb,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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)))))))).
tff(tp_c_2Efmapal_2Ebt__to__fmap__lb__ub,type,(c_2Efmapal_2Ebt__to__fmap__lb__ub:(del * del) > $i)).
tff(mem_c_2Efmapal_2Ebt__to__fmap__lb__ub,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))))).
tff(tp_c_2Efmapal_2Ebt__to__fmap__ub,type,(c_2Efmapal_2Ebt__to__fmap__ub:(del * del) > $i)).
tff(mem_c_2Efmapal_2Ebt__to__fmap__ub,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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)))))))).
tff(tp_c_2Efmapal_2Ebt__to__orl,type,(c_2Efmapal_2Ebt__to__orl:(del * del) > $i)).
tff(mem_c_2Efmapal_2Ebt__to__orl,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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)))))))).
tff(tp_c_2Efmapal_2Ebt__to__orl__ac,type,(c_2Efmapal_2Ebt__to__orl__ac:(del * del) > $i)).
tff(mem_c_2Efmapal_2Ebt__to__orl__ac,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))))).
tff(tp_c_2Efmapal_2Ebt__to__orl__lb,type,(c_2Efmapal_2Ebt__to__orl__lb:(del * del) > $i)).
tff(mem_c_2Efmapal_2Ebt__to__orl__lb,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))))).
tff(tp_c_2Efmapal_2Ebt__to__orl__lb__ac,type,(c_2Efmapal_2Ebt__to__orl__lb__ac:(del * del) > $i)).
tff(mem_c_2Efmapal_2Ebt__to__orl__lb__ac,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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)))))))))).
tff(tp_c_2Efmapal_2Ebt__to__orl__lb__ub,type,(c_2Efmapal_2Ebt__to__orl__lb__ub:(del * del) > $i)).
tff(mem_c_2Efmapal_2Ebt__to__orl__lb__ub,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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)))))))))).
tff(tp_c_2Efmapal_2Ebt__to__orl__lb__ub__ac,type,(c_2Efmapal_2Ebt__to__orl__lb__ub__ac:(del * del) > $i)).
tff(mem_c_2Efmapal_2Ebt__to__orl__lb__ub__ac,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))))))).
tff(tp_c_2Efmapal_2Ebt__to__orl__lb__ub__ac__tupled__aux,type,(c_2Efmapal_2Ebt__to__orl__lb__ub__ac__tupled__aux:(del * del) > $i)).
tff(mem_c_2Efmapal_2Ebt__to__orl__lb__ub__ac__tupled__aux,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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)))))))).
tff(tp_c_2Efmapal_2Ebt__to__orl__ub,type,(c_2Efmapal_2Ebt__to__orl__ub:(del * del) > $i)).
tff(mem_c_2Efmapal_2Ebt__to__orl__ub,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))))).
tff(tp_c_2Efmapal_2Ebt__to__orl__ub__ac,type,(c_2Efmapal_2Ebt__to__orl__ub__ac:(del * del) > $i)).
tff(mem_c_2Efmapal_2Ebt__to__orl__ub__ac,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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)))))))))).
tff(tp_c_2Efmapal_2Ediff__merge,type,(c_2Efmapal_2Ediff__merge:(del * del) > $i)).
tff(mem_c_2Efmapal_2Ediff__merge,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))))).
tff(tp_c_2Efmapal_2Efmap,type,(c_2Efmapal_2Efmap:(del * del) > $i)).
tff(mem_c_2Efmapal_2Efmap,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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)))))).
tff(tp_c_2Efmapal_2Eincr__build,type,(c_2Efmapal_2Eincr__build:(del * del) > $i)).
tff(mem_c_2Efmapal_2Eincr__build,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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)))))))))).
tff(tp_c_2Efmapal_2Eincr__flat,type,(c_2Efmapal_2Eincr__flat:(del * del) > $i)).
tff(mem_c_2Efmapal_2Eincr__flat,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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)))))))).
tff(tp_c_2Efmapal_2Eincr__merge,type,(c_2Efmapal_2Eincr__merge:(del * del) > $i)).
tff(mem_c_2Efmapal_2Eincr__merge,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))))))).
tff(tp_c_2Efmapal_2Eincr__sort,type,(c_2Efmapal_2Eincr__sort:(del * del) > $i)).
tff(mem_c_2Efmapal_2Eincr__sort,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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)))))))).
tff(tp_c_2Efmapal_2Einter__merge,type,(c_2Efmapal_2Einter__merge:(del * del) > $i)).
tff(mem_c_2Efmapal_2Einter__merge,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))))).
tff(tp_c_2Efmapal_2Elist__rplacv__cn,type,(c_2Efmapal_2Elist__rplacv__cn:(del * del) > $i)).
tff(mem_c_2Efmapal_2Elist__rplacv__cn,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))))).
tff(tp_c_2Efmapal_2Emerge,type,(c_2Efmapal_2Emerge:(del * del) > $i)).
tff(mem_c_2Efmapal_2Emerge,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))))).
tff(tp_c_2Efmapal_2Emerge__out,type,(c_2Efmapal_2Emerge__out:(del * del) > $i)).
tff(mem_c_2Efmapal_2Emerge__out,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))))).
tff(tp_c_2Efmapal_2Eoptry,type,(c_2Efmapal_2Eoptry:del > $i)).
tff(mem_c_2Efmapal_2Eoptry,axiom,( ! [A_27z:del] : mem(c_2Efmapal_2Eoptry(A_27z),arr(ty_2Eoption_2Eoption(A_27z),arr(ty_2Eoption_2Eoption(A_27z),ty_2Eoption_2Eoption(A_27z)))))).
tff(tp_c_2Efmapal_2Eoptry__list,type,(c_2Efmapal_2Eoptry__list:(del * del) > $i)).
tff(mem_c_2Efmapal_2Eoptry__list,axiom,( ! [A_27g:del] : ( ! [A_27z:del] : 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))))))).
tff(tp_c_2Efmapal_2Eunlookup,type,(c_2Efmapal_2Eunlookup:(del * del) > $i)).
tff(mem_c_2Efmapal_2Eunlookup,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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)))))).
tff(tp_c_2Efmapal_2Evcossa,type,(c_2Efmapal_2Evcossa:(del * del) > $i)).
tff(mem_c_2Efmapal_2Evcossa,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))).
tff(conj_thm_2Efmapal_2EORL__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),bool))) => ((( ! [V1cmp:$i] : (mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => p(ap(ap(V0P,V1cmp),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b)))))) & ( ! [V2cmp:$i] : (mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V3a:$i] : (mem(V3a,A_27a) => ( ! [V4b:$i] : (mem(V4b,A_27b) => ( ! [V5l:$i] : (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:$i] : (mem(V6v,ty_2Etoto_2Etoto(A_27a)) => ( ! [V7v1:$i] : (mem(V7v1,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(V0P,V6v),V7v1))))))))))))).
tff(conj_thm_2Efmapal_2EORL,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0cmp:$i] : (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:$i] : (mem(V1l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V2cmp:$i] : (mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V3b:$i] : (mem(V3b,A_27b) => ( ! [V4a:$i] : (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:$i] : (mem(V5p,A_27a) => ( ! [V6q:$i] : (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))) => (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V2cmp),V4a),V5p)) = fo__c_2EternaryComparisons_2ELESS))))))))))))))))))))).
tff(ax_thm_2Efmapal_2Eoptry,axiom,( ! [A_27z:del]: (( ! [V0p:$i] : (mem(V0p,A_27z) => ( ! [V1q:$i] : (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:$i] : (mem(V2q,ty_2Eoption_2Eoption(A_27z)) => (ap(ap(c_2Efmapal_2Eoptry(A_27z),c_2Eoption_2ENONE(A_27z)),V2q) = V2q)))))).
tff(conj_thm_2Efmapal_2Eoptry__list__ind,lemma,(( ! [A_27g:del]: ( ! [A_27z:del]: ( ! [V0P:$i] : (mem(V0P,arr(arr(A_27z,ty_2Eoption_2Eoption(A_27g)),arr(ty_2Elist_2Elist(ty_2Eoption_2Eoption(A_27z)),bool))) => ((( ! [V1f:$i] : (mem(V1f,arr(A_27z,ty_2Eoption_2Eoption(A_27g))) => p(ap(ap(V0P,V1f),c_2Elist_2ENIL(ty_2Eoption_2Eoption(A_27z)))))) & (( ! [V2f:$i] : (mem(V2f,arr(A_27z,ty_2Eoption_2Eoption(A_27g))) => ( ! [V3l:$i] : (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:$i] : (mem(V4f,arr(A_27z,ty_2Eoption_2Eoption(A_27g))) => ( ! [V5z:$i] : (mem(V5z,A_27z) => ( ! [V6l:$i] : (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:$i] : (mem(V7v,arr(A_27z,ty_2Eoption_2Eoption(A_27g))) => ( ! [V8v1:$i] : (mem(V8v1,ty_2Elist_2Elist(ty_2Eoption_2Eoption(A_27z))) => p(ap(ap(V0P,V7v),V8v1))))))))))))).
tff(conj_thm_2Efmapal_2Eoptry__list,lemma,(( ! [A_27g:del]: ( ! [A_27z:del]: (( ! [V0f:$i] : (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:$i] : (mem(V1l,ty_2Elist_2Elist(ty_2Eoption_2Eoption(A_27z))) => ( ! [V2f:$i] : (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:$i] : (mem(V3z,A_27z) => ( ! [V4l:$i] : (mem(V4l,ty_2Elist_2Elist(ty_2Eoption_2Eoption(A_27z))) => ( ! [V5f:$i] : (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))))))))))))))).
tff(conj_thm_2Efmapal_2Eassocv__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),arr(A_27a,bool))) => ((( ! [V1a:$i] : (mem(V1a,A_27a) => p(ap(ap(V0P,c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))),V1a)))) & ( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27b) => ( ! [V4l:$i] : (mem(V4l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V5a:$i] : (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:$i] : (mem(V6v,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V7v1:$i] : (mem(V7v1,A_27a) => p(ap(ap(V0P,V6v),V7v1))))))))))))).
tff(conj_thm_2Efmapal_2Eassocv,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0a:$i] : (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:$i] : (mem(V1y,A_27b) => ( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3l:$i] : (mem(V3l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V4a:$i] : (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)))))))))))))))).
tff(ax_thm_2Efmapal_2Evcossa,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0a:$i] : (mem(V0a,A_27a) => ( ! [V1l:$i] : (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))))))))).
tff(ax_thm_2Efmapal_2EOPTION__UPDATE,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,ty_2Eoption_2Eoption(A_27b))) => ( ! [V1g:$i] : (mem(V1g,arr(A_27a,ty_2Eoption_2Eoption(A_27b))) => ( ! [V2x:$i] : (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)))))))))))).
tff(conj_thm_2Efmapal_2Emerge__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (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:$i] : (mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V2l:$i] : (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:$i] : (mem(V3cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V4v4:$i] : (mem(V4v4,ty_2Epair_2Eprod(A_27a,A_27b)) => ( ! [V5v5:$i] : (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:$i] : (mem(V6cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V7a1:$i] : (mem(V7a1,A_27a) => ( ! [V8b1:$i] : (mem(V8b1,A_27b) => ( ! [V9l1:$i] : (mem(V9l1,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V10a2:$i] : (mem(V10a2,A_27a) => ( ! [V11b2:$i] : (mem(V11b2,A_27b) => ( ! [V12l2:$i] : (mem(V12l2,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ((((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V6cmp),V7a1),V10a2)) = fo__c_2EternaryComparisons_2EEQUAL) => p(ap(ap(ap(V0P,V6cmp),V9l1),V12l2))) & (((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V6cmp),V7a1),V10a2)) = fo__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))) & ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V6cmp),V7a1),V10a2)) = fo__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:$i] : (mem(V13v,ty_2Etoto_2Etoto(A_27a)) => ( ! [V14v1:$i] : (mem(V14v1,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V15v2:$i] : (mem(V15v2,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(ap(V0P,V13v),V14v1),V15v2))))))))))))))).
tff(conj_thm_2Efmapal_2Emerge,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V1cmp:$i] : (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:$i] : (mem(V2v5,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V3v4:$i] : (mem(V3v4,ty_2Epair_2Eprod(A_27a,A_27b)) => ( ! [V4cmp:$i] : (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:$i] : (mem(V5l2,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V6l1:$i] : (mem(V6l1,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V7cmp:$i] : (mem(V7cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V8b2:$i] : (mem(V8b2,A_27b) => ( ! [V9b1:$i] : (mem(V9b1,A_27b) => ( ! [V10a2:$i] : (mem(V10a2,A_27a) => ( ! [V11a1:$i] : (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)))))))))))))))))))))))).
tff(conj_thm_2Efmapal_2Eincr__merge__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (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:$i] : (mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V2l:$i] : (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:$i] : (mem(V3cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V4l:$i] : (mem(V4l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V5lol:$i] : (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:$i] : (mem(V6cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V7l:$i] : (mem(V7l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V8m:$i] : (mem(V8m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V9lol:$i] : (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:$i] : (mem(V10v,ty_2Etoto_2Etoto(A_27a)) => ( ! [V11v1:$i] : (mem(V11v1,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V12v2:$i] : (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))))))))))))))).
tff(conj_thm_2Efmapal_2Eincr__merge,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V1cmp:$i] : (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:$i] : (mem(V2lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) => ( ! [V3l:$i] : (mem(V3l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V4cmp:$i] : (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:$i] : (mem(V5m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V6lol:$i] : (mem(V6lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) => ( ! [V7l:$i] : (mem(V7l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V8cmp:$i] : (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))))))))))))))))).
tff(conj_thm_2Efmapal_2EORL__sublists__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (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:$i] : (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:$i] : (mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V3lol:$i] : (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:$i] : (mem(V4cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V5m:$i] : (mem(V5m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V6lol:$i] : (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:$i] : (mem(V7v,ty_2Etoto_2Etoto(A_27a)) => ( ! [V8v1:$i] : (mem(V8v1,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) => p(ap(ap(V0P,V7v),V8v1))))))))))))).
tff(conj_thm_2Efmapal_2EORL__sublists,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0cmp:$i] : (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:$i] : (mem(V1lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) => ( ! [V2cmp:$i] : (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:$i] : (mem(V3m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V4lol:$i] : (mem(V4lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) => ( ! [V5cmp:$i] : (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)))))))))))))))).
tff(ax_thm_2Efmapal_2Eincr__build,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0cmp:$i] : (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:$i] : (mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V2ab:$i] : (mem(V2ab,ty_2Epair_2Eprod(A_27a,A_27b)) => ( ! [V3l:$i] : (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))))))))))))).
tff(conj_thm_2Efmapal_2Emerge__out__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (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:$i] : (mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V2l:$i] : (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:$i] : (mem(V3cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V4l:$i] : (mem(V4l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V5lol:$i] : (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:$i] : (mem(V6cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V7l:$i] : (mem(V7l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V8m:$i] : (mem(V8m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V9lol:$i] : (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:$i] : (mem(V10v,ty_2Etoto_2Etoto(A_27a)) => ( ! [V11v1:$i] : (mem(V11v1,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V12v2:$i] : (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))))))))))))))).
tff(conj_thm_2Efmapal_2Emerge__out,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V1cmp:$i] : (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:$i] : (mem(V2lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) => ( ! [V3l:$i] : (mem(V3l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V4cmp:$i] : (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:$i] : (mem(V5m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V6lol:$i] : (mem(V6lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))))) => ( ! [V7l:$i] : (mem(V7l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V8cmp:$i] : (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)))))))))))))))).
tff(ax_thm_2Efmapal_2Eincr__flat,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1lol:$i] : (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))))))))).
tff(ax_thm_2Efmapal_2Eincr__sort,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1l:$i] : (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)))))))))).
tff(ax_thm_2Efmapal_2EOPTION__FLAT__primitive,axiom,( ! [A_27z:del]: (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))))).
tff(conj_thm_2Efmapal_2EOPTION__FLAT__ind,lemma,(( ! [A_27z:del]: ( ! [V0P:$i] : (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:$i] : (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:$i] : (mem(V2a,ty_2Elist_2Elist(A_27z)) => ( ! [V3l:$i] : (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:$i] : (mem(V4v,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27z)))) => p(ap(V0P,V4v)))))))))).
tff(conj_thm_2Efmapal_2EOPTION__FLAT,lemma,(( ! [A_27z:del]: ((ap(c_2Efmapal_2EOPTION__FLAT(A_27z),c_2Elist_2ENIL(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27z)))) = c_2Elist_2ENIL(A_27z)) & (( ! [V0l:$i] : (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:$i] : (mem(V1l,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27z)))) => ( ! [V2a:$i] : (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)))))))))))).
tff(ax_thm_2Efmapal_2Eunlookup,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (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)))))))).
tff(conj_thm_2Efmapal_2Ebt__to__fmap__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),bool))) => ((( ! [V1cmp:$i] : (mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => p(ap(ap(V0P,V1cmp),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b)))))) & ( ! [V2cmp:$i] : (mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V3l:$i] : (mem(V3l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V4x:$i] : (mem(V4x,A_27a) => ( ! [V5v:$i] : (mem(V5v,A_27b) => ( ! [V6r:$i] : (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:$i] : (mem(V7v,ty_2Etoto_2Etoto(A_27a)) => ( ! [V8v1:$i] : (mem(V8v1,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(V0P,V7v),V8v1))))))))))))).
tff(conj_thm_2Efmapal_2Ebt__to__fmap,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0cmp:$i] : (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:$i] : (mem(V1x,A_27a) => ( ! [V2v:$i] : (mem(V2v,A_27b) => ( ! [V3r:$i] : (mem(V3r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V4l:$i] : (mem(V4l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V5cmp:$i] : (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)))))))))))))))))))).
tff(conj_thm_2Efmapal_2EFAPPLY__nt,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1x:$i] : (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)))))))))).
tff(conj_thm_2Efmapal_2EFAPPLY__node,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2l:$i] : (mem(V2l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V3a:$i] : (mem(V3a,A_27a) => ( ! [V4b:$i] : (mem(V4b,A_27b) => ( ! [V5r:$i] : (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))))))))))))))))))).
tff(ax_thm_2Efmapal_2Ebt__to__fmap__lb,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1lb:$i] : (mem(V1lb,A_27a) => ( ! [V2t:$i] : (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))))))))))))).
tff(ax_thm_2Efmapal_2Ebt__to__fmap__ub,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1t:$i] : (mem(V1t,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V2ub:$i] : (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))))))))))))).
tff(ax_thm_2Efmapal_2Ebt__to__fmap__lb__ub,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1lb:$i] : (mem(V1lb,A_27a) => ( ! [V2t:$i] : (mem(V2t,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V3ub:$i] : (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))))))))))))))).
tff(ax_thm_2Efmapal_2Ebt__map,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0f:$i] : (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:$i] : (mem(V1f,arr(A_27a,A_27b)) => ( ! [V2l:$i] : (mem(V2l,ty_2Eenumeral_2Ebt(A_27a)) => ( ! [V3x:$i] : (mem(V3x,A_27a) => ( ! [V4r:$i] : (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))))))))))))))).
tff(conj_thm_2Efmapal_2Ebt__FST__FDOM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1t:$i] : (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))))))))))).
tff(conj_thm_2Efmapal_2Ebt__to__orl__lb__ub__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (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:$i] : (mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V2lb:$i] : (mem(V2lb,A_27a) => ( ! [V3ub:$i] : (mem(V3ub,A_27a) => p(ap(ap(ap(ap(V0P,V1cmp),V2lb),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b))),V3ub)))))))) & ( ! [V4cmp:$i] : (mem(V4cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V5lb:$i] : (mem(V5lb,A_27a) => ( ! [V6l:$i] : (mem(V6l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V7x:$i] : (mem(V7x,A_27a) => ( ! [V8y:$i] : (mem(V8y,A_27b) => ( ! [V9r:$i] : (mem(V9r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V10ub:$i] : (mem(V10ub,A_27a) => ((((~~ (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4cmp),V5lb),V7x)) = fo__c_2EternaryComparisons_2ELESS)) => p(ap(ap(ap(ap(V0P,V4cmp),V5lb),V9r),V10ub))) & ((((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4cmp),V5lb),V7x)) = fo__c_2EternaryComparisons_2ELESS) & (~~ (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4cmp),V7x),V10ub)) = fo__c_2EternaryComparisons_2ELESS))) => p(ap(ap(ap(ap(V0P,V4cmp),V5lb),V6l),V10ub))) & ((((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4cmp),V5lb),V7x)) = fo__c_2EternaryComparisons_2ELESS) & (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4cmp),V7x),V10ub)) = fo__c_2EternaryComparisons_2ELESS)) => p(ap(ap(ap(ap(V0P,V4cmp),V5lb),V6l),V7x))) & (((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4cmp),V5lb),V7x)) = fo__c_2EternaryComparisons_2ELESS) & (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4cmp),V7x),V10ub)) = fo__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:$i] : (mem(V11v,ty_2Etoto_2Etoto(A_27a)) => ( ! [V12v1:$i] : (mem(V12v1,A_27a) => ( ! [V13v2:$i] : (mem(V13v2,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V14v3:$i] : (mem(V14v3,A_27a) => p(ap(ap(ap(ap(V0P,V11v),V12v1),V13v2),V14v3))))))))))))))))).
tff(conj_thm_2Efmapal_2Ebt__to__orl__lb__ub,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0ub:$i] : (mem(V0ub,A_27a) => ( ! [V1lb:$i] : (mem(V1lb,A_27a) => ( ! [V2cmp:$i] : (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:$i] : (mem(V3y,A_27b) => ( ! [V4x:$i] : (mem(V4x,A_27a) => ( ! [V5ub:$i] : (mem(V5ub,A_27a) => ( ! [V6r:$i] : (mem(V6r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V7lb:$i] : (mem(V7lb,A_27a) => ( ! [V8l:$i] : (mem(V8l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V9cmp:$i] : (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)),inj__ty_2EternaryComparisons_2Eordering(fo__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)),inj__ty_2EternaryComparisons_2Eordering(fo__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)))))))))))))))))))))).
tff(conj_thm_2Efmapal_2Ebt__to__orl__lb__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),bool)))) => ((( ! [V1cmp:$i] : (mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V2lb:$i] : (mem(V2lb,A_27a) => p(ap(ap(ap(V0P,V1cmp),V2lb),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b)))))))) & ( ! [V3cmp:$i] : (mem(V3cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V4lb:$i] : (mem(V4lb,A_27a) => ( ! [V5l:$i] : (mem(V5l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V6x:$i] : (mem(V6x,A_27a) => ( ! [V7y:$i] : (mem(V7y,A_27b) => ( ! [V8r:$i] : (mem(V8r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ((((~~ (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V3cmp),V4lb),V6x)) = fo__c_2EternaryComparisons_2ELESS)) => p(ap(ap(ap(V0P,V3cmp),V4lb),V8r))) & ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V3cmp),V4lb),V6x)) = fo__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:$i] : (mem(V9v,ty_2Etoto_2Etoto(A_27a)) => ( ! [V10v1:$i] : (mem(V10v1,A_27a) => ( ! [V11v2:$i] : (mem(V11v2,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(ap(V0P,V9v),V10v1),V11v2))))))))))))))).
tff(conj_thm_2Efmapal_2Ebt__to__orl__lb,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0lb:$i] : (mem(V0lb,A_27a) => ( ! [V1cmp:$i] : (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:$i] : (mem(V2y,A_27b) => ( ! [V3x:$i] : (mem(V3x,A_27a) => ( ! [V4r:$i] : (mem(V4r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V5lb:$i] : (mem(V5lb,A_27a) => ( ! [V6l:$i] : (mem(V6l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V7cmp:$i] : (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)),inj__ty_2EternaryComparisons_2Eordering(fo__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)))))))))))))))))))).
tff(conj_thm_2Efmapal_2Ebt__to__orl__ub__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),arr(A_27a,bool)))) => ((( ! [V1cmp:$i] : (mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V2ub:$i] : (mem(V2ub,A_27a) => p(ap(ap(ap(V0P,V1cmp),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b))),V2ub)))))) & ( ! [V3cmp:$i] : (mem(V3cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V4l:$i] : (mem(V4l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V5x:$i] : (mem(V5x,A_27a) => ( ! [V6y:$i] : (mem(V6y,A_27b) => ( ! [V7r:$i] : (mem(V7r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V8ub:$i] : (mem(V8ub,A_27a) => ((((~~ (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V3cmp),V5x),V8ub)) = fo__c_2EternaryComparisons_2ELESS)) => p(ap(ap(ap(V0P,V3cmp),V4l),V8ub))) & ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V3cmp),V5x),V8ub)) = fo__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:$i] : (mem(V9v,ty_2Etoto_2Etoto(A_27a)) => ( ! [V10v1:$i] : (mem(V10v1,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V11v2:$i] : (mem(V11v2,A_27a) => p(ap(ap(ap(V0P,V9v),V10v1),V11v2))))))))))))))).
tff(conj_thm_2Efmapal_2Ebt__to__orl__ub,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0ub:$i] : (mem(V0ub,A_27a) => ( ! [V1cmp:$i] : (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:$i] : (mem(V2y,A_27b) => ( ! [V3x:$i] : (mem(V3x,A_27a) => ( ! [V4ub:$i] : (mem(V4ub,A_27a) => ( ! [V5r:$i] : (mem(V5r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V6l:$i] : (mem(V6l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V7cmp:$i] : (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)),inj__ty_2EternaryComparisons_2Eordering(fo__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)))))))))))))))))))).
tff(conj_thm_2Efmapal_2Ebt__to__orl__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),bool))) => ((( ! [V1cmp:$i] : (mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => p(ap(ap(V0P,V1cmp),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b)))))) & ( ! [V2cmp:$i] : (mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V3l:$i] : (mem(V3l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V4x:$i] : (mem(V4x,A_27a) => ( ! [V5y:$i] : (mem(V5y,A_27b) => ( ! [V6r:$i] : (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:$i] : (mem(V7v,ty_2Etoto_2Etoto(A_27a)) => ( ! [V8v1:$i] : (mem(V8v1,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(V0P,V7v),V8v1))))))))))))).
tff(conj_thm_2Efmapal_2Ebt__to__orl,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1l:$i] : (mem(V1l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27b) => ( ! [V4r:$i] : (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)))))))))))))))))).
tff(ax_thm_2Efmapal_2Efmap,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0l:$i] : (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)))))))).
tff(ax_thm_2Efmapal_2Ebt__to__orl__lb__ub__ac__tupled__AUX,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : (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)))))))).
tff(conj_thm_2Efmapal_2Ebt__to__orl__lb__ub__ac__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (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:$i] : (mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V2lb:$i] : (mem(V2lb,A_27a) => ( ! [V3ub:$i] : (mem(V3ub,A_27a) => ( ! [V4m:$i] : (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:$i] : (mem(V5cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V6lb:$i] : (mem(V6lb,A_27a) => ( ! [V7l:$i] : (mem(V7l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V8x:$i] : (mem(V8x,A_27a) => ( ! [V9y:$i] : (mem(V9y,A_27b) => ( ! [V10r:$i] : (mem(V10r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V11ub:$i] : (mem(V11ub,A_27a) => ( ! [V12m:$i] : (mem(V12m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ((((~~ (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V5cmp),V6lb),V8x)) = fo__c_2EternaryComparisons_2ELESS)) => p(ap(ap(ap(ap(ap(V0P,V5cmp),V6lb),V10r),V11ub),V12m))) & ((((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V5cmp),V6lb),V8x)) = fo__c_2EternaryComparisons_2ELESS) & (~~ (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V5cmp),V8x),V11ub)) = fo__c_2EternaryComparisons_2ELESS))) => p(ap(ap(ap(ap(ap(V0P,V5cmp),V6lb),V7l),V11ub),V12m))) & ((((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V5cmp),V6lb),V8x)) = fo__c_2EternaryComparisons_2ELESS) & (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V5cmp),V8x),V11ub)) = fo__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))))) & (((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V5cmp),V6lb),V8x)) = fo__c_2EternaryComparisons_2ELESS) & (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V5cmp),V8x),V11ub)) = fo__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:$i] : (mem(V13v,ty_2Etoto_2Etoto(A_27a)) => ( ! [V14v1:$i] : (mem(V14v1,A_27a) => ( ! [V15v2:$i] : (mem(V15v2,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V16v3:$i] : (mem(V16v3,A_27a) => ( ! [V17v4:$i] : (mem(V17v4,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(ap(ap(ap(V0P,V13v),V14v1),V15v2),V16v3),V17v4))))))))))))))))))).
tff(conj_thm_2Efmapal_2Ebt__to__orl__lb__ub__ac,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0ub:$i] : (mem(V0ub,A_27a) => ( ! [V1m:$i] : (mem(V1m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V2lb:$i] : (mem(V2lb,A_27a) => ( ! [V3cmp:$i] : (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:$i] : (mem(V4y,A_27b) => ( ! [V5x:$i] : (mem(V5x,A_27a) => ( ! [V6ub:$i] : (mem(V6ub,A_27a) => ( ! [V7r:$i] : (mem(V7r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V8m:$i] : (mem(V8m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V9lb:$i] : (mem(V9lb,A_27a) => ( ! [V10l:$i] : (mem(V10l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V11cmp:$i] : (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)),inj__ty_2EternaryComparisons_2Eordering(fo__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)),inj__ty_2EternaryComparisons_2Eordering(fo__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)))))))))))))))))))))))).
tff(conj_thm_2Efmapal_2Ebt__to__orl__lb__ac__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (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:$i] : (mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V2lb:$i] : (mem(V2lb,A_27a) => ( ! [V3m:$i] : (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:$i] : (mem(V4cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V5lb:$i] : (mem(V5lb,A_27a) => ( ! [V6l:$i] : (mem(V6l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V7x:$i] : (mem(V7x,A_27a) => ( ! [V8y:$i] : (mem(V8y,A_27b) => ( ! [V9r:$i] : (mem(V9r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V10m:$i] : (mem(V10m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ((((~~ (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4cmp),V5lb),V7x)) = fo__c_2EternaryComparisons_2ELESS)) => p(ap(ap(ap(ap(V0P,V4cmp),V5lb),V9r),V10m))) & ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4cmp),V5lb),V7x)) = fo__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:$i] : (mem(V11v,ty_2Etoto_2Etoto(A_27a)) => ( ! [V12v1:$i] : (mem(V12v1,A_27a) => ( ! [V13v2:$i] : (mem(V13v2,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V14v3:$i] : (mem(V14v3,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(ap(ap(V0P,V11v),V12v1),V13v2),V14v3))))))))))))))))).
tff(conj_thm_2Efmapal_2Ebt__to__orl__lb__ac,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0m:$i] : (mem(V0m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V1lb:$i] : (mem(V1lb,A_27a) => ( ! [V2cmp:$i] : (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:$i] : (mem(V3y,A_27b) => ( ! [V4x:$i] : (mem(V4x,A_27a) => ( ! [V5r:$i] : (mem(V5r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V6m:$i] : (mem(V6m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V7lb:$i] : (mem(V7lb,A_27a) => ( ! [V8l:$i] : (mem(V8l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V9cmp:$i] : (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)),inj__ty_2EternaryComparisons_2Eordering(fo__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)))))))))))))))))))))).
tff(conj_thm_2Efmapal_2Ebt__to__orl__ub__ac__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (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:$i] : (mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V2ub:$i] : (mem(V2ub,A_27a) => ( ! [V3m:$i] : (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:$i] : (mem(V4cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V5l:$i] : (mem(V5l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V6x:$i] : (mem(V6x,A_27a) => ( ! [V7y:$i] : (mem(V7y,A_27b) => ( ! [V8r:$i] : (mem(V8r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V9ub:$i] : (mem(V9ub,A_27a) => ( ! [V10m:$i] : (mem(V10m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ((((~~ (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4cmp),V6x),V9ub)) = fo__c_2EternaryComparisons_2ELESS)) => p(ap(ap(ap(ap(V0P,V4cmp),V5l),V9ub),V10m))) & ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4cmp),V6x),V9ub)) = fo__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:$i] : (mem(V11v,ty_2Etoto_2Etoto(A_27a)) => ( ! [V12v1:$i] : (mem(V12v1,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V13v2:$i] : (mem(V13v2,A_27a) => ( ! [V14v3:$i] : (mem(V14v3,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(ap(ap(V0P,V11v),V12v1),V13v2),V14v3))))))))))))))))).
tff(conj_thm_2Efmapal_2Ebt__to__orl__ub__ac,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0ub:$i] : (mem(V0ub,A_27a) => ( ! [V1m:$i] : (mem(V1m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V2cmp:$i] : (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:$i] : (mem(V3y,A_27b) => ( ! [V4x:$i] : (mem(V4x,A_27a) => ( ! [V5ub:$i] : (mem(V5ub,A_27a) => ( ! [V6r:$i] : (mem(V6r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V7m:$i] : (mem(V7m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V8l:$i] : (mem(V8l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V9cmp:$i] : (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)),inj__ty_2EternaryComparisons_2Eordering(fo__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)))))))))))))))))))))).
tff(conj_thm_2Efmapal_2Ebt__to__orl__ac__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (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:$i] : (mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V2m:$i] : (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:$i] : (mem(V3cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V4l:$i] : (mem(V4l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V5x:$i] : (mem(V5x,A_27a) => ( ! [V6y:$i] : (mem(V6y,A_27b) => ( ! [V7r:$i] : (mem(V7r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V8m:$i] : (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:$i] : (mem(V9v,ty_2Etoto_2Etoto(A_27a)) => ( ! [V10v1:$i] : (mem(V10v1,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V11v2:$i] : (mem(V11v2,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(ap(V0P,V9v),V10v1),V11v2))))))))))))))).
tff(conj_thm_2Efmapal_2Ebt__to__orl__ac,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1m:$i] : (mem(V1m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V2l:$i] : (mem(V2l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V3x:$i] : (mem(V3x,A_27a) => ( ! [V4y:$i] : (mem(V4y,A_27b) => ( ! [V5r:$i] : (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))))))))))))))))))))).
tff(ax_thm_2Efmapal_2EORWL,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1f:$i] : (mem(V1f,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ! [V2l:$i] : (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))))))))))))).
tff(conj_thm_2Efmapal_2EORWL__bt__to__orl,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1t:$i] : (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))))))))))).
tff(ax_thm_2Efmapal_2EOFU,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [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_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))))))))))).
tff(ax_thm_2Efmapal_2EUFO,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [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_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)))))))))))))).
tff(conj_thm_2Efmapal_2Ebl__to__fmap__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebl(ty_2Epair_2Eprod(A_27a,A_27b)),bool))) => ((( ! [V1cmp:$i] : (mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => p(ap(ap(V0P,V1cmp),c_2Eenumeral_2Enbl(ty_2Epair_2Eprod(A_27a,A_27b)))))) & (( ! [V2cmp:$i] : (mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V3b:$i] : (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:$i] : (mem(V4cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V5x:$i] : (mem(V5x,A_27a) => ( ! [V6y:$i] : (mem(V6y,A_27b) => ( ! [V7t:$i] : (mem(V7t,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V8b:$i] : (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:$i] : (mem(V9v,ty_2Etoto_2Etoto(A_27a)) => ( ! [V10v1:$i] : (mem(V10v1,ty_2Eenumeral_2Ebl(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(V0P,V9v),V10v1))))))))))))).
tff(conj_thm_2Efmapal_2Ebl__to__fmap,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0cmp:$i] : (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:$i] : (mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V2b:$i] : (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:$i] : (mem(V3y,A_27b) => ( ! [V4x:$i] : (mem(V4x,A_27a) => ( ! [V5t:$i] : (mem(V5t,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V6cmp:$i] : (mem(V6cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V7b:$i] : (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))))))))))))))))))).
tff(conj_thm_2Efmapal_2Ebt__to__orl__ID__IMP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1l:$i] : (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)))))))))).
tff(conj_thm_2Efmapal_2Efmap__FDOM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0l:$i] : (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))))))))).
tff(conj_thm_2Efmapal_2EORL__FUNION__IMP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1l:$i] : (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:$i] : (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)))))))))))))))).
tff(conj_thm_2Efmapal_2EFMAPAL__FDOM__THM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1x:$i] : (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:$i] : (mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V3x:$i] : (mem(V3x,A_27a) => ( ! [V4a:$i] : (mem(V4a,A_27a) => ( ! [V5b:$i] : (mem(V5b,A_27b) => ( ! [V6l:$i] : (mem(V6l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V7r:$i] : (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)))),inj__o(fo__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))))))))))))))))))))))).
tff(conj_thm_2Efmapal_2Einter__merge__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),arr(ty_2Elist_2Elist(A_27a),bool)))) => ((( ! [V1cmp:$i] : (mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => p(ap(ap(ap(V0P,V1cmp),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))),c_2Elist_2ENIL(A_27a))))) & (( ! [V2cmp:$i] : (mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V3a:$i] : (mem(V3a,A_27a) => ( ! [V4b:$i] : (mem(V4b,A_27b) => ( ! [V5l:$i] : (mem(V5l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(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)),c_2Elist_2ENIL(A_27a))))))))))) & (( ! [V6cmp:$i] : (mem(V6cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V7y:$i] : (mem(V7y,A_27a) => ( ! [V8m:$i] : (mem(V8m,ty_2Elist_2Elist(A_27a)) => p(ap(ap(ap(V0P,V6cmp),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))),ap(ap(c_2Elist_2ECONS(A_27a),V7y),V8m))))))))) & ( ! [V9cmp:$i] : (mem(V9cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V10a:$i] : (mem(V10a,A_27a) => ( ! [V11b:$i] : (mem(V11b,A_27b) => ( ! [V12l:$i] : (mem(V12l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V13y:$i] : (mem(V13y,A_27a) => ( ! [V14m:$i] : (mem(V14m,ty_2Elist_2Elist(A_27a)) => ((((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V9cmp),V10a),V13y)) = fo__c_2EternaryComparisons_2EEQUAL) => p(ap(ap(ap(V0P,V9cmp),V12l),V14m))) & (((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V9cmp),V10a),V13y)) = fo__c_2EternaryComparisons_2EGREATER) => p(ap(ap(ap(V0P,V9cmp),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V10a),V11b)),V12l)),V14m))) & ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V9cmp),V10a),V13y)) = fo__c_2EternaryComparisons_2ELESS) => p(ap(ap(ap(V0P,V9cmp),V12l),ap(ap(c_2Elist_2ECONS(A_27a),V13y),V14m)))))) => p(ap(ap(ap(V0P,V9cmp),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V10a),V11b)),V12l)),ap(ap(c_2Elist_2ECONS(A_27a),V13y),V14m))))))))))))))))))) => ( ! [V15v:$i] : (mem(V15v,ty_2Etoto_2Etoto(A_27a)) => ( ! [V16v1:$i] : (mem(V16v1,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V17v2:$i] : (mem(V17v2,ty_2Elist_2Elist(A_27a)) => p(ap(ap(ap(V0P,V15v),V16v1),V17v2))))))))))))))).
tff(conj_thm_2Efmapal_2Einter__merge,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => (ap(ap(ap(c_2Efmapal_2Einter__merge(A_27a,A_27b),V0cmp),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))),c_2Elist_2ENIL(A_27a)) = c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))))) & (( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V2cmp:$i] : (mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V3b:$i] : (mem(V3b,A_27b) => ( ! [V4a:$i] : (mem(V4a,A_27a) => (ap(ap(ap(c_2Efmapal_2Einter__merge(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)),c_2Elist_2ENIL(A_27a)) = c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))))))))))) & (( ! [V5y:$i] : (mem(V5y,A_27a) => ( ! [V6m:$i] : (mem(V6m,ty_2Elist_2Elist(A_27a)) => ( ! [V7cmp:$i] : (mem(V7cmp,ty_2Etoto_2Etoto(A_27a)) => (ap(ap(ap(c_2Efmapal_2Einter__merge(A_27a,A_27b),V7cmp),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))),ap(ap(c_2Elist_2ECONS(A_27a),V5y),V6m)) = c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))))))))) & ( ! [V8y:$i] : (mem(V8y,A_27a) => ( ! [V9m:$i] : (mem(V9m,ty_2Elist_2Elist(A_27a)) => ( ! [V10l:$i] : (mem(V10l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V11cmp:$i] : (mem(V11cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V12b:$i] : (mem(V12b,A_27b) => ( ! [V13a:$i] : (mem(V13a,A_27a) => (ap(ap(ap(c_2Efmapal_2Einter__merge(A_27a,A_27b),V11cmp),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V13a),V12b)),V10l)),ap(ap(c_2Elist_2ECONS(A_27a),V8y),V9m)) = 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),V11cmp),V13a),V8y)),ap(ap(ap(c_2Efmapal_2Einter__merge(A_27a,A_27b),V11cmp),V10l),ap(ap(c_2Elist_2ECONS(A_27a),V8y),V9m))),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V13a),V12b)),ap(ap(ap(c_2Efmapal_2Einter__merge(A_27a,A_27b),V11cmp),V10l),V9m))),ap(ap(ap(c_2Efmapal_2Einter__merge(A_27a,A_27b),V11cmp),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V13a),V12b)),V10l)),V9m)))))))))))))))))))))).
tff(conj_thm_2Efmapal_2EORL__DRESTRICT__IMP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1l:$i] : (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:$i] : (mem(V2m,ty_2Elist_2Elist(A_27a)) => (p(ap(ap(c_2Eenumeral_2EOL(A_27a),V0cmp),V2m)) => (p(ap(ap(c_2Efmapal_2EORL(A_27a,A_27b),V0cmp),ap(ap(ap(c_2Efmapal_2Einter__merge(A_27a,A_27b),V0cmp),V1l),V2m))) & (ap(c_2Efmapal_2Efmap(A_27a,A_27b),ap(ap(ap(c_2Efmapal_2Einter__merge(A_27a,A_27b),V0cmp),V1l),V2m)) = ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),ap(c_2Efmapal_2Efmap(A_27a,A_27b),V1l)),ap(c_2Elist_2ELIST__TO__SET(A_27a),V2m)))))))))))))))).
tff(conj_thm_2Efmapal_2Ediff__merge__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),arr(ty_2Elist_2Elist(A_27a),bool)))) => ((( ! [V1cmp:$i] : (mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => p(ap(ap(ap(V0P,V1cmp),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))),c_2Elist_2ENIL(A_27a))))) & (( ! [V2cmp:$i] : (mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V3a:$i] : (mem(V3a,A_27a) => ( ! [V4b:$i] : (mem(V4b,A_27b) => ( ! [V5l:$i] : (mem(V5l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(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)),c_2Elist_2ENIL(A_27a))))))))))) & (( ! [V6cmp:$i] : (mem(V6cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V7y:$i] : (mem(V7y,A_27a) => ( ! [V8m:$i] : (mem(V8m,ty_2Elist_2Elist(A_27a)) => p(ap(ap(ap(V0P,V6cmp),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))),ap(ap(c_2Elist_2ECONS(A_27a),V7y),V8m))))))))) & ( ! [V9cmp:$i] : (mem(V9cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V10a:$i] : (mem(V10a,A_27a) => ( ! [V11b:$i] : (mem(V11b,A_27b) => ( ! [V12l:$i] : (mem(V12l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V13y:$i] : (mem(V13y,A_27a) => ( ! [V14m:$i] : (mem(V14m,ty_2Elist_2Elist(A_27a)) => ((((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V9cmp),V10a),V13y)) = fo__c_2EternaryComparisons_2EEQUAL) => p(ap(ap(ap(V0P,V9cmp),V12l),V14m))) & (((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V9cmp),V10a),V13y)) = fo__c_2EternaryComparisons_2EGREATER) => p(ap(ap(ap(V0P,V9cmp),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V10a),V11b)),V12l)),V14m))) & ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V9cmp),V10a),V13y)) = fo__c_2EternaryComparisons_2ELESS) => p(ap(ap(ap(V0P,V9cmp),V12l),ap(ap(c_2Elist_2ECONS(A_27a),V13y),V14m)))))) => p(ap(ap(ap(V0P,V9cmp),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V10a),V11b)),V12l)),ap(ap(c_2Elist_2ECONS(A_27a),V13y),V14m))))))))))))))))))) => ( ! [V15v:$i] : (mem(V15v,ty_2Etoto_2Etoto(A_27a)) => ( ! [V16v1:$i] : (mem(V16v1,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V17v2:$i] : (mem(V17v2,ty_2Elist_2Elist(A_27a)) => p(ap(ap(ap(V0P,V15v),V16v1),V17v2))))))))))))))).
tff(conj_thm_2Efmapal_2Ediff__merge,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => (ap(ap(ap(c_2Efmapal_2Ediff__merge(A_27a,A_27b),V0cmp),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))),c_2Elist_2ENIL(A_27a)) = c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))))) & (( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V2cmp:$i] : (mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V3b:$i] : (mem(V3b,A_27b) => ( ! [V4a:$i] : (mem(V4a,A_27a) => (ap(ap(ap(c_2Efmapal_2Ediff__merge(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)),c_2Elist_2ENIL(A_27a)) = 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)))))))))) & (( ! [V5y:$i] : (mem(V5y,A_27a) => ( ! [V6m:$i] : (mem(V6m,ty_2Elist_2Elist(A_27a)) => ( ! [V7cmp:$i] : (mem(V7cmp,ty_2Etoto_2Etoto(A_27a)) => (ap(ap(ap(c_2Efmapal_2Ediff__merge(A_27a,A_27b),V7cmp),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))),ap(ap(c_2Elist_2ECONS(A_27a),V5y),V6m)) = c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))))))))) & ( ! [V8y:$i] : (mem(V8y,A_27a) => ( ! [V9m:$i] : (mem(V9m,ty_2Elist_2Elist(A_27a)) => ( ! [V10l:$i] : (mem(V10l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V11cmp:$i] : (mem(V11cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V12b:$i] : (mem(V12b,A_27b) => ( ! [V13a:$i] : (mem(V13a,A_27a) => (ap(ap(ap(c_2Efmapal_2Ediff__merge(A_27a,A_27b),V11cmp),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V13a),V12b)),V10l)),ap(ap(c_2Elist_2ECONS(A_27a),V8y),V9m)) = 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),V11cmp),V13a),V8y)),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V13a),V12b)),ap(ap(ap(c_2Efmapal_2Ediff__merge(A_27a,A_27b),V11cmp),V10l),ap(ap(c_2Elist_2ECONS(A_27a),V8y),V9m)))),ap(ap(ap(c_2Efmapal_2Ediff__merge(A_27a,A_27b),V11cmp),V10l),V9m)),ap(ap(ap(c_2Efmapal_2Ediff__merge(A_27a,A_27b),V11cmp),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V13a),V12b)),V10l)),V9m)))))))))))))))))))))).
tff(conj_thm_2Efmapal_2EORL__DRESTRICT__COMPL__IMP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1l:$i] : (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:$i] : (mem(V2m,ty_2Elist_2Elist(A_27a)) => (p(ap(ap(c_2Eenumeral_2EOL(A_27a),V0cmp),V2m)) => (p(ap(ap(c_2Efmapal_2EORL(A_27a,A_27b),V0cmp),ap(ap(ap(c_2Efmapal_2Ediff__merge(A_27a,A_27b),V0cmp),V1l),V2m))) & (ap(c_2Efmapal_2Efmap(A_27a,A_27b),ap(ap(ap(c_2Efmapal_2Ediff__merge(A_27a,A_27b),V0cmp),V1l),V2m)) = ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),ap(c_2Efmapal_2Efmap(A_27a,A_27b),V1l)),ap(c_2Epred__set_2ECOMPL(A_27a),ap(c_2Elist_2ELIST__TO__SET(A_27a),V2m))))))))))))))))).
tff(conj_thm_2Efmapal_2EFMAPAL__fmap,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => (ap(c_2Efmapal_2Efmap(A_27a,A_27b),V1l) = ap(ap(c_2Efmapal_2EFMAPAL(A_27a,A_27b),V0cmp),ap(c_2Eenumeral_2Elist__to__bt(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Efmapal_2Eincr__sort(A_27a,A_27b),V0cmp),V1l)))))))))))).
tff(conj_thm_2Efmapal_2EORL__FMAPAL,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1l:$i] : (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(c_2Efmapal_2Efmap(A_27a,A_27b),V1l) = ap(ap(c_2Efmapal_2EFMAPAL(A_27a,A_27b),V0cmp),ap(c_2Eenumeral_2Elist__to__bt(ty_2Epair_2Eprod(A_27a,A_27b)),V1l)))))))))))).
tff(conj_thm_2Efmapal_2EORWL__FUNION__THM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1s:$i] : (mem(V1s,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ! [V2l:$i] : (mem(V2l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V3t:$i] : (mem(V3t,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ! [V4m:$i] : (mem(V4m,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ((p(ap(ap(ap(c_2Efmapal_2EORWL(A_27a,A_27b),V0cmp),V1s),V2l)) & p(ap(ap(ap(c_2Efmapal_2EORWL(A_27a,A_27b),V0cmp),V3t),V4m))) => p(ap(ap(ap(c_2Efmapal_2EORWL(A_27a,A_27b),V0cmp),ap(ap(c_2Efinite__map_2EFUNION(A_27a,A_27b),V1s),V3t)),ap(ap(ap(c_2Efmapal_2Emerge(A_27a,A_27b),V0cmp),V2l),V4m)))))))))))))))))).
tff(conj_thm_2Efmapal_2EORWL__DRESTRICT__THM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1s:$i] : (mem(V1s,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ! [V2l:$i] : (mem(V2l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V3t:$i] : (mem(V3t,arr(A_27a,bool)) => ( ! [V4m:$i] : (mem(V4m,ty_2Elist_2Elist(A_27a)) => ((p(ap(ap(ap(c_2Efmapal_2EORWL(A_27a,A_27b),V0cmp),V1s),V2l)) & p(ap(ap(ap(c_2Eenumeral_2EOWL(A_27a),V0cmp),V3t),V4m))) => p(ap(ap(ap(c_2Efmapal_2EORWL(A_27a,A_27b),V0cmp),ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),V1s),V3t)),ap(ap(ap(c_2Efmapal_2Einter__merge(A_27a,A_27b),V0cmp),V2l),V4m)))))))))))))))))).
tff(conj_thm_2Efmapal_2EORWL__DRESTRICT__COMPL__THM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1s:$i] : (mem(V1s,ty_2Efinite__map_2Efmap(A_27a,A_27b)) => ( ! [V2l:$i] : (mem(V2l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V3t:$i] : (mem(V3t,arr(A_27a,bool)) => ( ! [V4m:$i] : (mem(V4m,ty_2Elist_2Elist(A_27a)) => ((p(ap(ap(ap(c_2Efmapal_2EORWL(A_27a,A_27b),V0cmp),V1s),V2l)) & p(ap(ap(ap(c_2Eenumeral_2EOWL(A_27a),V0cmp),V3t),V4m))) => p(ap(ap(ap(c_2Efmapal_2EORWL(A_27a,A_27b),V0cmp),ap(ap(c_2Efinite__map_2EDRESTRICT(A_27a,A_27b),V1s),ap(c_2Epred__set_2ECOMPL(A_27a),V3t))),ap(ap(ap(c_2Efmapal_2Ediff__merge(A_27a,A_27b),V0cmp),V2l),V4m)))))))))))))))))).
tff(ax_thm_2Efmapal_2EAP__SND,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27b,A_27c)) => ( ! [V1a:$i] : (mem(V1a,A_27a) => ( ! [V2b:$i] : (mem(V2b,A_27b) => (ap(ap(c_2Efmapal_2EAP__SND(A_27a,A_27b,A_27c),V0f),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V1a),V2b)) = ap(ap(c_2Epair_2E_2C(A_27a,A_27c),V1a),ap(V0f,V2b))))))))))))).
tff(conj_thm_2Efmapal_2Eo__f__bt__map,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1f:$i] : (mem(V1f,arr(A_27b,A_27c)) => ( ! [V2t:$i] : (mem(V2t,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => (ap(ap(c_2Efinite__map_2Eo__f(A_27a,A_27b,A_27c),V1f),ap(ap(c_2Efmapal_2EFMAPAL(A_27a,A_27b),V0cmp),V2t)) = ap(ap(c_2Efmapal_2EFMAPAL(A_27a,A_27c),V0cmp),ap(ap(c_2Efmapal_2Ebt__map(ty_2Epair_2Eprod(A_27a,A_27b),ty_2Epair_2Eprod(A_27a,A_27c)),ap(c_2Efmapal_2EAP__SND(A_27a,A_27b,A_27c),V1f)),V2t)))))))))))))).
tff(conj_thm_2Efmapal_2EFAPPLY__fmap__NIL,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => (ap(ap(c_2Efinite__map_2EFAPPLY(A_27a,A_27b),ap(c_2Efmapal_2Efmap(A_27a,A_27b),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b)))),V0x) = ap(ap(c_2Efinite__map_2EFAPPLY(A_27a,A_27b),c_2Efinite__map_2EFEMPTY(A_27a,A_27b)),V0x)))))))).
tff(conj_thm_2Efmapal_2EFAPPLY__fmap__CONS,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1y:$i] : (mem(V1y,A_27a) => ( ! [V2z:$i] : (mem(V2z,A_27b) => ( ! [V3l:$i] : (mem(V3l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => (ap(ap(c_2Efinite__map_2EFAPPLY(A_27a,A_27b),ap(c_2Efmapal_2Efmap(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),V1y),V2z)),V3l))),V0x) = ap(ap(ap(c_2Ebool_2ECOND(A_27b),ap(ap(c_2Emin_2E_3D(A_27a),V0x),V1y)),V2z),ap(ap(c_2Efinite__map_2EFAPPLY(A_27a,A_27b),ap(c_2Efmapal_2Efmap(A_27a,A_27b),V3l)),V0x))))))))))))))).
tff(conj_thm_2Efmapal_2Eo__f__fmap,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27b,A_27c)) => ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => (ap(ap(c_2Efinite__map_2Eo__f(A_27a,A_27b,A_27c),V0f),ap(c_2Efmapal_2Efmap(A_27a,A_27b),V1l)) = ap(c_2Efmapal_2Efmap(A_27a,A_27c),ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),ty_2Epair_2Eprod(A_27a,A_27c)),ap(c_2Efmapal_2EAP__SND(A_27a,A_27b,A_27c),V0f)),V1l)))))))))))).
tff(conj_thm_2Efmapal_2EORL__bt__lb__ub__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (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:$i] : (mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V2lb:$i] : (mem(V2lb,A_27a) => ( ! [V3ub:$i] : (mem(V3ub,A_27a) => p(ap(ap(ap(ap(V0P,V1cmp),V2lb),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b))),V3ub)))))))) & ( ! [V4cmp:$i] : (mem(V4cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V5lb:$i] : (mem(V5lb,A_27a) => ( ! [V6l:$i] : (mem(V6l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V7x:$i] : (mem(V7x,A_27a) => ( ! [V8y:$i] : (mem(V8y,A_27b) => ( ! [V9r:$i] : (mem(V9r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V10ub:$i] : (mem(V10ub,A_27a) => ((p(ap(ap(ap(ap(V0P,V4cmp),V5lb),V6l),V7x)) & 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:$i] : (mem(V11v,ty_2Etoto_2Etoto(A_27a)) => ( ! [V12v1:$i] : (mem(V12v1,A_27a) => ( ! [V13v2:$i] : (mem(V13v2,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V14v3:$i] : (mem(V14v3,A_27a) => p(ap(ap(ap(ap(V0P,V11v),V12v1),V13v2),V14v3))))))))))))))))).
tff(conj_thm_2Efmapal_2EORL__bt__lb__ub,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0ub:$i] : (mem(V0ub,A_27a) => ( ! [V1lb:$i] : (mem(V1lb,A_27a) => ( ! [V2cmp:$i] : (mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => (p(ap(ap(ap(ap(c_2Efmapal_2EORL__bt__lb__ub(A_27a,A_27b),V2cmp),V1lb),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b))),V0ub)) <=> (surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V2cmp),V1lb),V0ub)) = fo__c_2EternaryComparisons_2ELESS)))))))) & ( ! [V3y:$i] : (mem(V3y,A_27b) => ( ! [V4x:$i] : (mem(V4x,A_27a) => ( ! [V5ub:$i] : (mem(V5ub,A_27a) => ( ! [V6r:$i] : (mem(V6r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V7lb:$i] : (mem(V7lb,A_27a) => ( ! [V8l:$i] : (mem(V8l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V9cmp:$i] : (mem(V9cmp,ty_2Etoto_2Etoto(A_27a)) => (p(ap(ap(ap(ap(c_2Efmapal_2EORL__bt__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)) <=> (p(ap(ap(ap(ap(c_2Efmapal_2EORL__bt__lb__ub(A_27a,A_27b),V9cmp),V7lb),V8l),V4x)) & p(ap(ap(ap(ap(c_2Efmapal_2EORL__bt__lb__ub(A_27a,A_27b),V9cmp),V4x),V6r),V5ub))))))))))))))))))))))).
tff(conj_thm_2Efmapal_2EORL__bt__lb__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),bool)))) => ((( ! [V1cmp:$i] : (mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V2lb:$i] : (mem(V2lb,A_27a) => p(ap(ap(ap(V0P,V1cmp),V2lb),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b)))))))) & ( ! [V3cmp:$i] : (mem(V3cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V4lb:$i] : (mem(V4lb,A_27a) => ( ! [V5l:$i] : (mem(V5l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V6x:$i] : (mem(V6x,A_27a) => ( ! [V7y:$i] : (mem(V7y,A_27b) => ( ! [V8r:$i] : (mem(V8r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => (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:$i] : (mem(V9v,ty_2Etoto_2Etoto(A_27a)) => ( ! [V10v1:$i] : (mem(V10v1,A_27a) => ( ! [V11v2:$i] : (mem(V11v2,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(ap(V0P,V9v),V10v1),V11v2))))))))))))))).
tff(conj_thm_2Efmapal_2EORL__bt__lb,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0lb:$i] : (mem(V0lb,A_27a) => ( ! [V1cmp:$i] : (mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => (p(ap(ap(ap(c_2Efmapal_2EORL__bt__lb(A_27a,A_27b),V1cmp),V0lb),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b)))) <=> $true))))) & ( ! [V2y:$i] : (mem(V2y,A_27b) => ( ! [V3x:$i] : (mem(V3x,A_27a) => ( ! [V4r:$i] : (mem(V4r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V5lb:$i] : (mem(V5lb,A_27a) => ( ! [V6l:$i] : (mem(V6l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V7cmp:$i] : (mem(V7cmp,ty_2Etoto_2Etoto(A_27a)) => (p(ap(ap(ap(c_2Efmapal_2EORL__bt__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))) <=> (p(ap(ap(ap(ap(c_2Efmapal_2EORL__bt__lb__ub(A_27a,A_27b),V7cmp),V5lb),V6l),V3x)) & p(ap(ap(ap(c_2Efmapal_2EORL__bt__lb(A_27a,A_27b),V7cmp),V3x),V4r))))))))))))))))))))).
tff(conj_thm_2Efmapal_2EORL__bt__ub__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),arr(A_27a,bool)))) => ((( ! [V1cmp:$i] : (mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V2ub:$i] : (mem(V2ub,A_27a) => p(ap(ap(ap(V0P,V1cmp),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b))),V2ub)))))) & ( ! [V3cmp:$i] : (mem(V3cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V4l:$i] : (mem(V4l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V5x:$i] : (mem(V5x,A_27a) => ( ! [V6y:$i] : (mem(V6y,A_27b) => ( ! [V7r:$i] : (mem(V7r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V8ub:$i] : (mem(V8ub,A_27a) => (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:$i] : (mem(V9v,ty_2Etoto_2Etoto(A_27a)) => ( ! [V10v1:$i] : (mem(V10v1,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V11v2:$i] : (mem(V11v2,A_27a) => p(ap(ap(ap(V0P,V9v),V10v1),V11v2))))))))))))))).
tff(conj_thm_2Efmapal_2EORL__bt__ub,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0ub:$i] : (mem(V0ub,A_27a) => ( ! [V1cmp:$i] : (mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => (p(ap(ap(ap(c_2Efmapal_2EORL__bt__ub(A_27a,A_27b),V1cmp),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b))),V0ub)) <=> $true))))) & ( ! [V2y:$i] : (mem(V2y,A_27b) => ( ! [V3x:$i] : (mem(V3x,A_27a) => ( ! [V4ub:$i] : (mem(V4ub,A_27a) => ( ! [V5r:$i] : (mem(V5r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V6l:$i] : (mem(V6l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V7cmp:$i] : (mem(V7cmp,ty_2Etoto_2Etoto(A_27a)) => (p(ap(ap(ap(c_2Efmapal_2EORL__bt__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)) <=> (p(ap(ap(ap(c_2Efmapal_2EORL__bt__ub(A_27a,A_27b),V7cmp),V6l),V3x)) & p(ap(ap(ap(ap(c_2Efmapal_2EORL__bt__lb__ub(A_27a,A_27b),V7cmp),V3x),V5r),V4ub))))))))))))))))))))).
tff(conj_thm_2Efmapal_2EORL__bt__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),bool))) => ((( ! [V1cmp:$i] : (mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => p(ap(ap(V0P,V1cmp),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b)))))) & ( ! [V2cmp:$i] : (mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V3l:$i] : (mem(V3l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V4x:$i] : (mem(V4x,A_27a) => ( ! [V5y:$i] : (mem(V5y,A_27b) => ( ! [V6r:$i] : (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:$i] : (mem(V7v,ty_2Etoto_2Etoto(A_27a)) => ( ! [V8v1:$i] : (mem(V8v1,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(V0P,V7v),V8v1))))))))))))).
tff(conj_thm_2Efmapal_2EORL__bt,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1l:$i] : (mem(V1l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27b) => ( ! [V4r:$i] : (mem(V4r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ((p(ap(ap(c_2Efmapal_2EORL__bt(A_27a,A_27b),V0cmp),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b)))) <=> $true) & (p(ap(ap(c_2Efmapal_2EORL__bt(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))) <=> (p(ap(ap(ap(c_2Efmapal_2EORL__bt__ub(A_27a,A_27b),V0cmp),V1l),V2x)) & p(ap(ap(ap(c_2Efmapal_2EORL__bt__lb(A_27a,A_27b),V0cmp),V2x),V4r))))))))))))))))))).
tff(conj_thm_2Efmapal_2Ebetter__bt__to__orl,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1t:$i] : (mem(V1t,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => (ap(ap(c_2Efmapal_2Ebt__to__orl(A_27a,A_27b),V0cmp),V1t) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))),ap(ap(c_2Efmapal_2EORL__bt(A_27a,A_27b),V0cmp),V1t)),ap(ap(c_2Eenumeral_2Ebt__to__list__ac(ty_2Epair_2Eprod(A_27a,A_27b)),V1t),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b)))),ap(ap(ap(c_2Efmapal_2Ebt__to__orl__ac(A_27a,A_27b),V0cmp),V1t),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))))))))))))).
tff(conj_thm_2Efmapal_2Elist__rplacv__cn__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,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))),bool)))) => ((( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27b) => ( ! [V3cn:$i] : (mem(V3cn,arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))) => p(ap(ap(ap(V0P,ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V1x),V2y)),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))),V3cn)))))))) & ( ! [V4x:$i] : (mem(V4x,A_27a) => ( ! [V5y:$i] : (mem(V5y,A_27b) => ( ! [V6w:$i] : (mem(V6w,A_27a) => ( ! [V7z:$i] : (mem(V7z,A_27b) => ( ! [V8l:$i] : (mem(V8l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V9cn:$i] : (mem(V9cn,arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))) => (((~~ (V4x = V6w)) => p(ap(ap(ap(V0P,ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V4x),V5y)),V8l),f2650(A_27b,A_27a,V7z,V6w,V9cn)))) => p(ap(ap(ap(V0P,ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V4x),V5y)),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V6w),V7z)),V8l)),V9cn)))))))))))))))) => ( ! [V11v:$i] : (mem(V11v,A_27a) => ( ! [V12v1:$i] : (mem(V12v1,A_27b) => ( ! [V13v2:$i] : (mem(V13v2,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V14v3:$i] : (mem(V14v3,arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))) => p(ap(ap(ap(V0P,ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V11v),V12v1)),V13v2),V14v3))))))))))))))))).
tff(conj_thm_2Efmapal_2Elist__rplacv__cn,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0y:$i] : (mem(V0y,A_27b) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2cn:$i] : (mem(V2cn,arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))) => (ap(ap(ap(c_2Efmapal_2Elist__rplacv__cn(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V1x),V0y)),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))),V2cn) = c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))))))))) & ( ! [V3z:$i] : (mem(V3z,A_27b) => ( ! [V4y:$i] : (mem(V4y,A_27b) => ( ! [V5x:$i] : (mem(V5x,A_27a) => ( ! [V6w:$i] : (mem(V6w,A_27a) => ( ! [V7l:$i] : (mem(V7l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V8cn:$i] : (mem(V8cn,arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))) => (ap(ap(ap(c_2Efmapal_2Elist__rplacv__cn(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V5x),V4y)),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V6w),V3z)),V7l)),V8cn) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))),ap(ap(c_2Emin_2E_3D(A_27a),V5x),V6w)),ap(V8cn,ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V5x),V4y)),V7l))),ap(ap(ap(c_2Efmapal_2Elist__rplacv__cn(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V5x),V4y)),V7l),f2651(A_27b,A_27a,V3z,V6w,V8cn))))))))))))))))))))).
tff(conj_thm_2Efmapal_2Efmap__FDOM__rec,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0x:$i] : (mem(V0x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),ap(c_2Efmapal_2Efmap(A_27a,A_27b),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b)))))) <=> $false))) & ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2w:$i] : (mem(V2w,A_27a) => ( ! [V3z:$i] : (mem(V3z,A_27b) => ( ! [V4l:$i] : (mem(V4l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),ap(c_2Efmapal_2Efmap(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),V2w),V3z)),V4l))))) <=> ((V1x = V2w) | p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),ap(c_2Efinite__map_2EFDOM(A_27a,A_27b),ap(c_2Efmapal_2Efmap(A_27a,A_27b),V4l))))))))))))))))))).
tff(conj_thm_2Efmapal_2Elist__rplacv__thm,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1y:$i] : (mem(V1y,A_27b) => ( ! [V2l:$i] : (mem(V2l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(c_2Ebool_2ELET(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),bool),f2652(A_27b,A_27a,V1y,V0x,V2l)),ap(ap(ap(c_2Efmapal_2Elist__rplacv__cn(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V0x),V1y)),V2l),i(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))))))))))))))).
tff(conj_thm_2Efmapal_2Ebt__rplacv__cn__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,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))),bool))))) => ((( ! [V1cmp:$i] : (mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27b) => ( ! [V4cn:$i] : (mem(V4cn,arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)))) => p(ap(ap(ap(ap(V0P,V1cmp),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2x),V3y)),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b))),V4cn)))))))))) & ( ! [V5cmp:$i] : (mem(V5cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V6x:$i] : (mem(V6x,A_27a) => ( ! [V7y:$i] : (mem(V7y,A_27b) => ( ! [V8l:$i] : (mem(V8l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V9w:$i] : (mem(V9w,A_27a) => ( ! [V10z:$i] : (mem(V10z,A_27b) => ( ! [V11r:$i] : (mem(V11r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V12cn:$i] : (mem(V12cn,arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)))) => ((((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V5cmp),V6x),V9w)) = fo__c_2EternaryComparisons_2EGREATER) => p(ap(ap(ap(ap(V0P,V5cmp),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V6x),V7y)),V11r),f2653(A_27b,A_27a,V10z,V9w,V8l,V12cn)))) & ((surj__ty_2EternaryComparisons_2Eordering(ap(ap(ap(c_2Etoto_2Eapto(A_27a),V5cmp),V6x),V9w)) = fo__c_2EternaryComparisons_2ELESS) => p(ap(ap(ap(ap(V0P,V5cmp),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V6x),V7y)),V8l),f2654(A_27b,A_27a,V11r,V10z,V9w,V12cn))))) => p(ap(ap(ap(ap(V0P,V5cmp),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V6x),V7y)),ap(ap(ap(c_2Eenumeral_2Enode(ty_2Epair_2Eprod(A_27a,A_27b)),V8l),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V9w),V10z)),V11r)),V12cn)))))))))))))))))))) => ( ! [V15v:$i] : (mem(V15v,ty_2Etoto_2Etoto(A_27a)) => ( ! [V16v1:$i] : (mem(V16v1,A_27a) => ( ! [V17v2:$i] : (mem(V17v2,A_27b) => ( ! [V18v3:$i] : (mem(V18v3,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V19v4:$i] : (mem(V19v4,arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)))) => p(ap(ap(ap(ap(V0P,V15v),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V16v1),V17v2)),V18v3),V19v4))))))))))))))))))).
tff(conj_thm_2Efmapal_2Ebt__rplacv__cn,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0y:$i] : (mem(V0y,A_27b) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2cn:$i] : (mem(V2cn,arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)))) => ( ! [V3cmp:$i] : (mem(V3cmp,ty_2Etoto_2Etoto(A_27a)) => (ap(ap(ap(ap(c_2Efmapal_2Ebt__rplacv__cn(A_27a,A_27b),V3cmp),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V1x),V0y)),c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b))),V2cn) = c_2Eenumeral_2Ent(ty_2Epair_2Eprod(A_27a,A_27b))))))))))) & ( ! [V4z:$i] : (mem(V4z,A_27b) => ( ! [V5y:$i] : (mem(V5y,A_27b) => ( ! [V6x:$i] : (mem(V6x,A_27a) => ( ! [V7w:$i] : (mem(V7w,A_27a) => ( ! [V8r:$i] : (mem(V8r,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V9l:$i] : (mem(V9l,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ! [V10cn:$i] : (mem(V10cn,arr(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)))) => ( ! [V11cmp:$i] : (mem(V11cmp,ty_2Etoto_2Etoto(A_27a)) => (ap(ap(ap(ap(c_2Efmapal_2Ebt__rplacv__cn(A_27a,A_27b),V11cmp),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V6x),V5y)),ap(ap(ap(c_2Eenumeral_2Enode(ty_2Epair_2Eprod(A_27a,A_27b)),V9l),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V7w),V4z)),V8r)),V10cn) = ap(ap(ap(ap(c_2EternaryComparisons_2Eordering__CASE(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V11cmp),V6x),V7w)),ap(ap(ap(ap(c_2Efmapal_2Ebt__rplacv__cn(A_27a,A_27b),V11cmp),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V6x),V5y)),V9l),f2655(A_27b,A_27a,V8r,V4z,V7w,V10cn))),ap(V10cn,ap(ap(ap(c_2Eenumeral_2Enode(ty_2Epair_2Eprod(A_27a,A_27b)),V9l),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V6x),V5y)),V8r))),ap(ap(ap(ap(c_2Efmapal_2Ebt__rplacv__cn(A_27a,A_27b),V11cmp),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V6x),V5y)),V8r),f2656(A_27b,A_27a,V4z,V7w,V9l,V10cn))))))))))))))))))))))))).
tff(conj_thm_2Efmapal_2Ebt__rplacv__thm,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0cmp:$i] : (mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27b) => ( ! [V3t:$i] : (mem(V3t,ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b))) => p(ap(ap(c_2Ebool_2ELET(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)),bool),f2657(A_27b,A_27a,V2y,V0cmp,V3t,V1x)),ap(ap(ap(ap(c_2Efmapal_2Ebt__rplacv__cn(A_27a,A_27b),V0cmp),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V1x),V2y)),V3t),i(ty_2Eenumeral_2Ebt(ty_2Epair_2Eprod(A_27a,A_27b)))))))))))))))))).
tff(conj_thm_2Efmapal_2EFUN__fmap__thm,conjecture,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => (ap(c_2Efmapal_2Efmap(A_27a,A_27b),ap(ap(c_2Elist_2EMAP(A_27a,ty_2Epair_2Eprod(A_27a,A_27b)),f2658(A_27b,A_27a,V0f)),V1l)) = ap(ap(c_2Efinite__map_2EFUN__FMAP(A_27a,A_27b),V0f),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1l))))))))))).
