include('Axioms/DeepSyntax^2.ax').
thf(tp_c_2Efmapal_2EAP__SND,type,(c_2Efmapal_2EAP__SND:(del>(del>(del>$i))))).
thf(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)))))))).
thf(tp_c_2Efmapal_2EFMAPAL,type,(c_2Efmapal_2EFMAPAL:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Efmapal_2EOFU,type,(c_2Efmapal_2EOFU:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2Efmapal_2EOPTION__FLAT,type,(c_2Efmapal_2EOPTION__FLAT:(del>$i))).
thf(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))))).
thf(tp_c_2Efmapal_2EOPTION__UPDATE,type,(c_2Efmapal_2EOPTION__UPDATE:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2Efmapal_2EORL,type,(c_2Efmapal_2EORL:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Efmapal_2EORL__bt,type,(c_2Efmapal_2EORL__bt:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Efmapal_2EORL__bt__lb,type,(c_2Efmapal_2EORL__bt__lb:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Efmapal_2EORL__bt__lb__ub,type,(c_2Efmapal_2EORL__bt__lb__ub:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2Efmapal_2EORL__bt__ub,type,(c_2Efmapal_2EORL__bt__ub:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Efmapal_2EORL__sublists,type,(c_2Efmapal_2EORL__sublists:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Efmapal_2EORWL,type,(c_2Efmapal_2EORWL:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Efmapal_2EUFO,type,(c_2Efmapal_2EUFO:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2Efmapal_2Eassocv,type,(c_2Efmapal_2Eassocv:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Efmapal_2Ebl__to__fmap,type,(c_2Efmapal_2Ebl__to__fmap:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Efmapal_2Ebt__map,type,(c_2Efmapal_2Ebt__map:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Efmapal_2Ebt__rplacv__cn,type,(c_2Efmapal_2Ebt__rplacv__cn:(del>(del>$i)))).
thf(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)))))))))).
thf(tp_c_2Efmapal_2Ebt__to__fmap__lb,type,(c_2Efmapal_2Ebt__to__fmap__lb:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2Efmapal_2Ebt__to__fmap__lb__ub,type,(c_2Efmapal_2Ebt__to__fmap__lb__ub:(del>(del>$i)))).
thf(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))))))))).
thf(tp_c_2Efmapal_2Ebt__to__fmap__ub,type,(c_2Efmapal_2Ebt__to__fmap__ub:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2Efmapal_2Ebt__to__orl,type,(c_2Efmapal_2Ebt__to__orl:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2Efmapal_2Ebt__to__orl__ac,type,(c_2Efmapal_2Ebt__to__orl__ac:(del>(del>$i)))).
thf(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))))))))).
thf(tp_c_2Efmapal_2Ebt__to__orl__lb,type,(c_2Efmapal_2Ebt__to__orl__lb:(del>(del>$i)))).
thf(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))))))))).
thf(tp_c_2Efmapal_2Ebt__to__orl__lb__ac,type,(c_2Efmapal_2Ebt__to__orl__lb__ac:(del>(del>$i)))).
thf(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)))))))))).
thf(tp_c_2Efmapal_2Ebt__to__orl__lb__ub,type,(c_2Efmapal_2Ebt__to__orl__lb__ub:(del>(del>$i)))).
thf(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)))))))))).
thf(tp_c_2Efmapal_2Ebt__to__orl__lb__ub__ac,type,(c_2Efmapal_2Ebt__to__orl__lb__ub__ac:(del>(del>$i)))).
thf(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))))))))))).
thf(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)))).
thf(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)))))))).
thf(tp_c_2Efmapal_2Ebt__to__orl__ub,type,(c_2Efmapal_2Ebt__to__orl__ub:(del>(del>$i)))).
thf(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))))))))).
thf(tp_c_2Efmapal_2Ebt__to__orl__ub__ac,type,(c_2Efmapal_2Ebt__to__orl__ub__ac:(del>(del>$i)))).
thf(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)))))))))).
thf(tp_c_2Efmapal_2Ediff__merge,type,(c_2Efmapal_2Ediff__merge:(del>(del>$i)))).
thf(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))))))))).
thf(tp_c_2Efmapal_2Efmap,type,(c_2Efmapal_2Efmap:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Efmapal_2Eincr__build,type,(c_2Efmapal_2Eincr__build:(del>(del>$i)))).
thf(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)))))))))).
thf(tp_c_2Efmapal_2Eincr__flat,type,(c_2Efmapal_2Eincr__flat:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2Efmapal_2Eincr__merge,type,(c_2Efmapal_2Eincr__merge:(del>(del>$i)))).
thf(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))))))))))).
thf(tp_c_2Efmapal_2Eincr__sort,type,(c_2Efmapal_2Eincr__sort:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2Efmapal_2Einter__merge,type,(c_2Efmapal_2Einter__merge:(del>(del>$i)))).
thf(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))))))))).
thf(tp_c_2Efmapal_2Elist__rplacv__cn,type,(c_2Efmapal_2Elist__rplacv__cn:(del>(del>$i)))).
thf(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))))))))).
thf(tp_c_2Efmapal_2Emerge,type,(c_2Efmapal_2Emerge:(del>(del>$i)))).
thf(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))))))))).
thf(tp_c_2Efmapal_2Emerge__out,type,(c_2Efmapal_2Emerge__out:(del>(del>$i)))).
thf(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))))))))).
thf(tp_c_2Efmapal_2Eoptry,type,(c_2Efmapal_2Eoptry:(del>$i))).
thf(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)))))).
thf(tp_c_2Efmapal_2Eoptry__list,type,(c_2Efmapal_2Eoptry__list:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Efmapal_2Eunlookup,type,(c_2Efmapal_2Eunlookup:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Efmapal_2Evcossa,type,(c_2Efmapal_2Evcossa:(del>(del>$i)))).
thf(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))))))).
thf(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)))))))))))).
thf(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)))))))))))))))))))).
thf(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)))))).
thf(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)))))))))))).
thf(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)))))))))))))).
thf(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)))))))))))).
thf(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))))))))))))))).
thf(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))))))))).
thf(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)))))))))))).
thf(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)))))))))))))).
thf(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))))))))))))))))))))))).
thf(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)))))))))))))).
thf(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)))))))))))))))).
thf(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)))))))))))).
thf(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))))))))))))))).
thf(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))))))))))))).
thf(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)))))))))))))).
thf(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))))))))))))))).
thf(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))))))))).
thf(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)))))))))).
thf(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)))@(lam@(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))@(^ [V0R:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(c_2Erelation_2EWF@(ty_2Elist_2Elist@(ty_2Eoption_2Eoption@(ty_2Elist_2Elist@A_27z))))@V0R))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(c_2Ebool_2E_21@(ty_2Elist_2Elist@(ty_2Eoption_2Eoption@(ty_2Elist_2Elist@A_27z))))@(lam@(ty_2Elist_2Elist@(ty_2Eoption_2Eoption@(ty_2Elist_2Elist@A_27z)))@(^ [V1l:$i] : (ap@(ap@V0R@V1l)@(ap@(ap@(c_2Elist_2ECONS@(ty_2Eoption_2Eoption@(ty_2Elist_2Elist@A_27z)))@(c_2Eoption_2ENONE@(ty_2Elist_2Elist@A_27z)))@V1l))))))@(ap@(c_2Ebool_2E_21@(ty_2Elist_2Elist@A_27z))@(lam@(ty_2Elist_2Elist@A_27z)@(^ [V2a:$i] : (ap@(c_2Ebool_2E_21@(ty_2Elist_2Elist@(ty_2Eoption_2Eoption@(ty_2Elist_2Elist@A_27z))))@(lam@(ty_2Elist_2Elist@(ty_2Eoption_2Eoption@(ty_2Elist_2Elist@A_27z)))@(^ [V3l:$i] : (ap@(ap@V0R@V3l)@(ap@(ap@(c_2Elist_2ECONS@(ty_2Eoption_2Eoption@(ty_2Elist_2Elist@A_27z)))@(ap@(c_2Eoption_2ESOME@(ty_2Elist_2Elist@A_27z))@V2a))@V3l))))))))))))))@(lam@(arr@(ty_2Elist_2Elist@(ty_2Eoption_2Eoption@(ty_2Elist_2Elist@A_27z)))@(ty_2Elist_2Elist@A_27z))@(^ [V4OPTION__FLAT:$i] : (lam@(ty_2Elist_2Elist@(ty_2Eoption_2Eoption@(ty_2Elist_2Elist@A_27z)))@(^ [V5a_27:$i] : (ap@(ap@(ap@(c_2Elist_2Elist__CASE@(ty_2Eoption_2Eoption@(ty_2Elist_2Elist@A_27z))@(ty_2Elist_2Elist@A_27z))@V5a_27)@(ap@(c_2Ecombin_2EI@(ty_2Elist_2Elist@A_27z))@(c_2Elist_2ENIL@A_27z)))@(lam@(ty_2Eoption_2Eoption@(ty_2Elist_2Elist@A_27z))@(^ [V6v:$i] : (lam@(ty_2Elist_2Elist@(ty_2Eoption_2Eoption@(ty_2Elist_2Elist@A_27z)))@(^ [V7l:$i] : (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Elist_2Elist@A_27z)@(ty_2Elist_2Elist@A_27z))@V6v)@(ap@(c_2Ecombin_2EI@(ty_2Elist_2Elist@A_27z))@(ap@V4OPTION__FLAT@V7l)))@(lam@(ty_2Elist_2Elist@A_27z)@(^ [V8a:$i] : (ap@(c_2Ecombin_2EI@(ty_2Elist_2Elist@A_27z))@(ap@(ap@(c_2Elist_2EAPPEND@A_27z)@V8a)@(ap@V4OPTION__FLAT@V7l))))))))))))))))))).
thf(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))))))))).
thf(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))))))))))).
thf(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)))))))).
thf(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)))))))))))).
thf(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)@(lam@A_27a@(^ [V6y:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V6y)@(ap@(ap@(c_2Emin_2E_3D@ty_2EternaryComparisons_2Eordering)@(ap@(ap@(ap@(c_2Etoto_2Eapto@A_27a)@V5cmp)@V6y)@V1x))@(inj__ty_2EternaryComparisons_2Eordering @ fo__c_2EternaryComparisons_2ELESS))))))))@(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)@(lam@A_27a@(^ [V7z:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V7z)@(ap@(ap@(c_2Emin_2E_3D@ty_2EternaryComparisons_2Eordering)@(ap@(ap@(ap@(c_2Etoto_2Eapto@A_27a)@V5cmp)@V1x)@V7z))@(inj__ty_2EternaryComparisons_2Eordering @ fo__c_2EternaryComparisons_2ELESS))))))))))))))))))))))).
thf(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))))))))).
thf(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)))))))))))))))))).
thf(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)@(lam@A_27a@(^ [V3x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V3x)@(ap@(ap@(c_2Emin_2E_3D@ty_2EternaryComparisons_2Eordering)@(ap@(ap@(ap@(c_2Etoto_2Eapto@A_27a)@V0cmp)@V1lb)@V3x))@(inj__ty_2EternaryComparisons_2Eordering @ fo__c_2EternaryComparisons_2ELESS))))))))))))))))).
thf(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)@(lam@A_27a@(^ [V3x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V3x)@(ap@(ap@(c_2Emin_2E_3D@ty_2EternaryComparisons_2Eordering)@(ap@(ap@(ap@(c_2Etoto_2Eapto@A_27a)@V0cmp)@V3x)@V2ub))@(inj__ty_2EternaryComparisons_2Eordering @ fo__c_2EternaryComparisons_2ELESS))))))))))))))))).
thf(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)@(lam@A_27a@(^ [V4x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V4x)@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@ty_2EternaryComparisons_2Eordering)@(ap@(ap@(ap@(c_2Etoto_2Eapto@A_27a)@V0cmp)@V1lb)@V4x))@(inj__ty_2EternaryComparisons_2Eordering @ fo__c_2EternaryComparisons_2ELESS)))@(ap@(ap@(c_2Emin_2E_3D@ty_2EternaryComparisons_2Eordering)@(ap@(ap@(ap@(c_2Etoto_2Eapto@A_27a)@V0cmp)@V4x)@V3ub))@(inj__ty_2EternaryComparisons_2Eordering @ fo__c_2EternaryComparisons_2ELESS)))))))))))))))))))).
thf(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))))))))))))))).
thf(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)))))))))).
thf(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)))))))))))))))).
thf(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))))))))))))))))))))).
thf(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)))))))))))))).
thf(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))))))))))))))))))).
thf(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)))))))))))))).
thf(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))))))))))))))))))).
thf(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)))))))))))).
thf(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))))))))))))))))).
thf(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)))))))).
thf(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)@(lam@(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)))@(^ [V1bt__to__orl__lb__ub__ac__tupled:$i] : (lam@(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))))))@(^ [V2a:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@A_27a@A_27b))@(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))))))@V2a)@(lam@(ty_2Etoto_2Etoto@A_27a)@(^ [V3cmp:$i] : (lam@(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)))))@(^ [V4v1:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@A_27a@A_27b))@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)))))@V4v1)@(lam@A_27a@(^ [V5lb:$i] : (lam@(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))))@(^ [V6v3:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@A_27a@A_27b))@(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))))@V6v3)@(lam@(ty_2Eenumeral_2Ebt@(ty_2Epair_2Eprod@A_27a@A_27b))@(^ [V7v4:$i] : (lam@(ty_2Epair_2Eprod@A_27a@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@A_27a@A_27b)))@(^ [V8v5:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@A_27a@A_27b))@A_27a@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@A_27a@A_27b)))@V8v5)@(lam@A_27a@(^ [V9ub:$i] : (lam@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@A_27a@A_27b))@(^ [V10m:$i] : (ap@(ap@(ap@(c_2Eenumeral_2Ebt__CASE@(ty_2Epair_2Eprod@A_27a@A_27b)@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@A_27a@A_27b)))@V7v4)@(ap@(c_2Ecombin_2EI@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@A_27a@A_27b)))@V10m))@(lam@(ty_2Eenumeral_2Ebt@(ty_2Epair_2Eprod@A_27a@A_27b))@(^ [V11l:$i] : (lam@(ty_2Epair_2Eprod@A_27a@A_27b)@(^ [V12v9:$i] : (lam@(ty_2Eenumeral_2Ebt@(ty_2Epair_2Eprod@A_27a@A_27b))@(^ [V13r:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@A_27a@A_27b))@A_27a@A_27b)@V12v9)@(lam@A_27a@(^ [V14x:$i] : (lam@A_27b@(^ [V15y:$i] : (ap@(c_2Ecombin_2EI@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@A_27a@A_27b)))@(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)@V3cmp)@V5lb)@V14x))@(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)@V3cmp)@V14x)@V9ub))@(inj__ty_2EternaryComparisons_2Eordering @ fo__c_2EternaryComparisons_2ELESS)))@(ap@V1bt__to__orl__lb__ub__ac__tupled@(ap@(ap@(c_2Epair_2E_2C@(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))))))@V3cmp)@(ap@(ap@(c_2Epair_2E_2C@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)))))@V5lb)@(ap@(ap@(c_2Epair_2E_2C@(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))))@V11l)@(ap@(ap@(c_2Epair_2E_2C@A_27a@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@A_27a@A_27b)))@V14x)@(ap@(ap@(c_2Elist_2ECONS@(ty_2Epair_2Eprod@A_27a@A_27b))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V14x)@V15y))@(ap@V1bt__to__orl__lb__ub__ac__tupled@(ap@(ap@(c_2Epair_2E_2C@(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))))))@V3cmp)@(ap@(ap@(c_2Epair_2E_2C@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)))))@V14x)@(ap@(ap@(c_2Epair_2E_2C@(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))))@V13r)@(ap@(ap@(c_2Epair_2E_2C@A_27a@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@A_27a@A_27b)))@V9ub)@V10m))))))))))))@(ap@V1bt__to__orl__lb__ub__ac__tupled@(ap@(ap@(c_2Epair_2E_2C@(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))))))@V3cmp)@(ap@(ap@(c_2Epair_2E_2C@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)))))@V5lb)@(ap@(ap@(c_2Epair_2E_2C@(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))))@V11l)@(ap@(ap@(c_2Epair_2E_2C@A_27a@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@A_27a@A_27b)))@V9ub)@V10m)))))))@(ap@V1bt__to__orl__lb__ub__ac__tupled@(ap@(ap@(c_2Epair_2E_2C@(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))))))@V3cmp)@(ap@(ap@(c_2Epair_2E_2C@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)))))@V5lb)@(ap@(ap@(c_2Epair_2E_2C@(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))))@V13r)@(ap@(ap@(c_2Epair_2E_2C@A_27a@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@A_27a@A_27b)))@V9ub)@V10m)))))))))))))))))))))))))))))))))))))))))))))))))).
thf(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)))))))))))))))))).
thf(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))))))))))))))))))))))).
thf(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)))))))))))))))).
thf(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))))))))))))))))))))).
thf(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)))))))))))))))).
thf(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))))))))))))))))))))).
thf(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)))))))))))))).
thf(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)))))))))))))))))))).
thf(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))))))))))))).
thf(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)))))))))).
thf(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)@(lam@A_27a@(^ [V3x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V3x)@(ap@(ap@(ap@(c_2Eenumeral_2ELESS__ALL@A_27a)@V0cmp)@V3x)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V2g))))))))@V2g))))))))))).
thf(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)@(lam@A_27a@(^ [V3y:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V3y)@(ap@(c_2Ebool_2E_21@A_27a)@(lam@A_27a@(^ [V4z:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4z)@(ap@(c_2Efinite__map_2EFDOM@A_27a@A_27b)@V1f)))@(ap@(ap@(c_2Emin_2E_3D@ty_2EternaryComparisons_2Eordering)@(ap@(ap@(ap@(c_2Etoto_2Eapto@A_27a)@V0cmp)@V4z)@V3y))@(inj__ty_2EternaryComparisons_2Eordering @ fo__c_2EternaryComparisons_2ELESS)))))))))))))))))))))).
thf(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)))))))))))).
thf(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)@(lam@A_27a@(^ [V8z:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V8z)@(ap@(ap@(c_2Emin_2E_3D@ty_2EternaryComparisons_2Eordering)@(ap@(ap@(ap@(c_2Etoto_2Eapto@A_27a)@V6cmp)@V4x)@V8z))@(inj__ty_2EternaryComparisons_2Eordering @ fo__c_2EternaryComparisons_2ELESS)))))))))@(ap@(ap@(c_2Efmapal_2Ebl__to__fmap@A_27a@A_27b)@V6cmp)@V7b)))))))))))))))))).
thf(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))))))))).
thf(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)))))))).
thf(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))))))))))))))).
thf(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))))@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)))))))))))))))))))))).
thf(conj_thm_2Efmapal_2Einter__merge__ind,conjecture,( ! [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)))))))))))))).
