include('Axioms/dft_2.ax').
tff(tp_c_2EDecode_2Edec2enc,type,(c_2EDecode_2Edec2enc:del > $i)).
tff(mem_c_2EDecode_2Edec2enc,axiom,( ! [A_27a:del] : mem(c_2EDecode_2Edec2enc(A_27a),arr(arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool)))),arr(A_27a,ty_2Elist_2Elist(bool)))))).
tff(stp_c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o,type,(tp__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o : $tType)).
tff(stp_inj_c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o,type,(inj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o : tp__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o > $i)).
tff(stp_surj_c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o,type,(surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o : $i > tp__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o)).
tff(stp_inj_surj_c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o,axiom,( ! [X:tp__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o] : (surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o(inj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o(X)) = X))).
tff(stp_inj_mem_c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o,axiom,( ! [X:tp__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o] : (mem(inj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o(X),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Elist_2Elist(bool))))))).
tff(stp_iso_mem_c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o,axiom,( ! [X:$i] : (mem(X,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Elist_2Elist(bool)))) => (X = inj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o(surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o(X)))))).
tff(stp_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o,type,(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o : $tType)).
tff(stp_inj_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o,type,(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o : tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o > $i)).
tff(stp_surj_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o,type,(surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o : $i > tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o)).
tff(stp_inj_surj_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o] : (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o(X)) = X))).
tff(stp_inj_mem_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o] : (mem(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o(X),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Elist_2Elist(bool)))))).
tff(stp_iso_mem_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o,axiom,( ! [X:$i] : (mem(X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Elist_2Elist(bool))) => (X = inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o(surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o(X)))))).
tff(tp_c_2EDecode_2Edec__bnum,type,(c_2EDecode_2Edec__bnum:$i)).
tff(mem_c_2EDecode_2Edec__bnum,axiom,mem(c_2EDecode_2Edec__bnum,arr(ty_2Enum_2Enum,arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Elist_2Elist(bool))))))).
tff(tp_c_2EDecode_2Edecode__blist,type,(c_2EDecode_2Edecode__blist:del > $i)).
tff(mem_c_2EDecode_2Edecode__blist,axiom,( ! [A_27a:del] : mem(c_2EDecode_2Edecode__blist(A_27a),arr(arr(ty_2Elist_2Elist(A_27a),bool),arr(ty_2Enum_2Enum,arr(arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool)))),arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(bool)))))))))).
tff(tp_c_2EDecode_2Edecode__bnum,type,(c_2EDecode_2Edecode__bnum:$i)).
tff(mem_c_2EDecode_2Edecode__bnum,axiom,mem(c_2EDecode_2Edecode__bnum,arr(ty_2Enum_2Enum,arr(arr(ty_2Enum_2Enum,bool),arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Elist_2Elist(bool)))))))).
tff(stp_c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o,type,(tp__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o : $tType)).
tff(stp_inj_c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o,type,(inj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o : tp__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o > $i)).
tff(stp_surj_c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o,type,(surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o : $i > tp__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o)).
tff(stp_inj_surj_c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o,axiom,( ! [X:tp__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o] : (surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o(inj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o(X)) = X))).
tff(stp_inj_mem_c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o,axiom,( ! [X:tp__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o] : (mem(inj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o(X),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(bool,ty_2Elist_2Elist(bool))))))).
tff(stp_iso_mem_c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o,axiom,( ! [X:$i] : (mem(X,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(bool,ty_2Elist_2Elist(bool)))) => (X = inj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o(surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o(X)))))).
tff(tp_c_2EDecode_2Edecode__bool,type,(c_2EDecode_2Edecode__bool:$i)).
tff(mem_c_2EDecode_2Edecode__bool,axiom,mem(c_2EDecode_2Edecode__bool,arr(arr(bool,bool),arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(bool,ty_2Elist_2Elist(bool))))))).
tff(tp_c_2EDecode_2Edecode__list,type,(c_2EDecode_2Edecode__list:del > $i)).
tff(mem_c_2EDecode_2Edecode__list,axiom,( ! [A_27a:del] : mem(c_2EDecode_2Edecode__list(A_27a),arr(arr(ty_2Elist_2Elist(A_27a),bool),arr(arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool)))),arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(bool))))))))).
tff(tp_c_2EDecode_2Edecode__num,type,(c_2EDecode_2Edecode__num:$i)).
tff(mem_c_2EDecode_2Edecode__num,axiom,mem(c_2EDecode_2Edecode__num,arr(arr(ty_2Enum_2Enum,bool),arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Elist_2Elist(bool))))))).
tff(tp_c_2EDecode_2Edecode__option,type,(c_2EDecode_2Edecode__option:del > $i)).
tff(mem_c_2EDecode_2Edecode__option,axiom,( ! [A_27a:del] : mem(c_2EDecode_2Edecode__option(A_27a),arr(arr(ty_2Eoption_2Eoption(A_27a),bool),arr(arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool)))),arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eoption_2Eoption(A_27a),ty_2Elist_2Elist(bool))))))))).
tff(tp_c_2EDecode_2Edecode__prod,type,(c_2EDecode_2Edecode__prod:(del * del) > $i)).
tff(mem_c_2EDecode_2Edecode__prod,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EDecode_2Edecode__prod(A_27a,A_27b),arr(arr(ty_2Epair_2Eprod(A_27a,A_27b),bool),arr(arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool)))),arr(arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,ty_2Elist_2Elist(bool)))),arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Epair_2Eprod(A_27a,A_27b),ty_2Elist_2Elist(bool))))))))))).
tff(tp_c_2EDecode_2Edecode__sum,type,(c_2EDecode_2Edecode__sum:(del * del) > $i)).
tff(mem_c_2EDecode_2Edecode__sum,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EDecode_2Edecode__sum(A_27a,A_27b),arr(arr(ty_2Esum_2Esum(A_27a,A_27b),bool),arr(arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool)))),arr(arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,ty_2Elist_2Elist(bool)))),arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Esum_2Esum(A_27a,A_27b),ty_2Elist_2Elist(bool))))))))))).
tff(tp_c_2EDecode_2Edecode__tree,type,(c_2EDecode_2Edecode__tree:del > $i)).
tff(mem_c_2EDecode_2Edecode__tree,axiom,( ! [A_27a:del] : mem(c_2EDecode_2Edecode__tree(A_27a),arr(arr(ty_2EEncode_2Etree(A_27a),bool),arr(arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool)))),arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2EEncode_2Etree(A_27a),ty_2Elist_2Elist(bool))))))))).
tff(stp_c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o,type,(tp__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o : $tType)).
tff(stp_inj_c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o,type,(inj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o : tp__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o > $i)).
tff(stp_surj_c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o,type,(surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o : $i > tp__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o)).
tff(stp_inj_surj_c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o,axiom,( ! [X:tp__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o] : (surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o(inj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o(X)) = X))).
tff(stp_inj_mem_c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o,axiom,( ! [X:tp__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o] : (mem(inj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o(X),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,ty_2Elist_2Elist(bool))))))).
tff(stp_iso_mem_c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o,axiom,( ! [X:$i] : (mem(X,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,ty_2Elist_2Elist(bool)))) => (X = inj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o(surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o(X)))))).
tff(stp_c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o,type,(tp__c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o : $tType)).
tff(stp_inj_c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o,type,(inj__c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o : tp__c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o > $i)).
tff(stp_surj_c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o,type,(surj__c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o : $i > tp__c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o)).
tff(stp_inj_surj_c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o] : (surj__c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o(inj__c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o(X)) = X))).
tff(stp_inj_mem_c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o] : (mem(inj__c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o(X),ty_2Epair_2Eprod(ty_2Eone_2Eone,ty_2Elist_2Elist(bool)))))).
tff(stp_iso_mem_c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o,axiom,( ! [X:$i] : (mem(X,ty_2Epair_2Eprod(ty_2Eone_2Eone,ty_2Elist_2Elist(bool))) => (X = inj__c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o(surj__c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o(X)))))).
tff(tp_c_2EDecode_2Edecode__unit,type,(c_2EDecode_2Edecode__unit:$i)).
tff(mem_c_2EDecode_2Edecode__unit,axiom,mem(c_2EDecode_2Edecode__unit,arr(arr(ty_2Eone_2Eone,bool),arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,ty_2Elist_2Elist(bool))))))).
tff(tp_c_2EDecode_2Eenc2dec,type,(c_2EDecode_2Eenc2dec:del > $i)).
tff(mem_c_2EDecode_2Eenc2dec,axiom,( ! [A_27a:del] : mem(c_2EDecode_2Eenc2dec(A_27a),arr(arr(A_27a,bool),arr(arr(A_27a,ty_2Elist_2Elist(bool)),arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))))))))).
tff(tp_c_2EDecode_2Ewf__decoder,type,(c_2EDecode_2Ewf__decoder:del > $i)).
tff(mem_c_2EDecode_2Ewf__decoder,axiom,( ! [A_27a:del] : mem(c_2EDecode_2Ewf__decoder(A_27a),arr(arr(A_27a,bool),arr(arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool)))),bool))))).
tff(ax_thm_2EDecode_2Ewf__decoder__def,axiom,( ! [A_27a:del]: ( ! [V0p:$i] : (mem(V0p,arr(A_27a,bool)) => ( ! [V1d:$i] : (mem(V1d,arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))))) => (p(ap(ap(c_2EDecode_2Ewf__decoder(A_27a),V0p),V1d)) <=> ( ! [V2x:$i] : (mem(V2x,A_27a) => p(ap(ap(ap(c_2Ebool_2ECOND(bool),ap(V0p,V2x)),ap(c_2Ebool_2E_3F(ty_2Elist_2Elist(bool)),f1717(A_27a,V1d,V2x))),ap(c_2Ebool_2E_21(ty_2Elist_2Elist(bool)),f1719(A_27a,V1d,V2x))))))))))))).
tff(ax_thm_2EDecode_2Eenc2dec__def,axiom,( ! [A_27a:del]: ( ! [V0p:$i] : (mem(V0p,arr(A_27a,bool)) => ( ! [V1e:$i] : (mem(V1e,arr(A_27a,ty_2Elist_2Elist(bool))) => ( ! [V2l:tp__c_ty_2Elist_2Elist_o] : (ap(ap(ap(c_2EDecode_2Eenc2dec(A_27a),V0p),V1e),inj__c_ty_2Elist_2Elist_o(V2l)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool)))),ap(c_2Ebool_2E_3F(A_27a),f1721(A_27a,V0p,V1e,V2l))),ap(c_2Eoption_2ESOME(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))),ap(c_2Emin_2E_40(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))),ap(c_2Epair_2EUNCURRY(A_27a,ty_2Elist_2Elist(bool),bool),f1723(A_27a,V2l,V1e,V0p))))),c_2Eoption_2ENONE(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool)))))))))))).
tff(ax_thm_2EDecode_2Edec2enc__def,axiom,( ! [A_27a:del]: ( ! [V0d:$i] : (mem(V0d,arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))))) => ( ! [V1x:$i] : (mem(V1x,A_27a) => (surj__c_ty_2Elist_2Elist_o(ap(ap(c_2EDecode_2Edec2enc(A_27a),V0d),V1x)) = surj__c_ty_2Elist_2Elist_o(ap(c_2Emin_2E_40(ty_2Elist_2Elist(bool)),f1724(A_27a,V0d,V1x)))))))))).
tff(conj_thm_2EDecode_2Eenc2dec__none,lemma,(( ! [A_27a:del]: ( ! [V0p:$i] : (mem(V0p,arr(A_27a,bool)) => ( ! [V1e:$i] : (mem(V1e,arr(A_27a,ty_2Elist_2Elist(bool))) => ( ! [V2l:tp__c_ty_2Elist_2Elist_o] : ((ap(ap(ap(c_2EDecode_2Eenc2dec(A_27a),V0p),V1e),inj__c_ty_2Elist_2Elist_o(V2l)) = c_2Eoption_2ENONE(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool)))) <=> ( ! [V3x:$i] : (mem(V3x,A_27a) => ( ! [V4t:tp__c_ty_2Elist_2Elist_o] : (p(ap(V0p,V3x)) => (~~ (V2l = surj__c_ty_2Elist_2Elist_o(ap(ap(c_2Elist_2EAPPEND(bool),ap(V1e,V3x)),inj__c_ty_2Elist_2Elist_o(V4t)))))))))))))))))).
tff(conj_thm_2EDecode_2Eenc2dec__some,lemma,(( ! [A_27a:del]: ( ! [V0p:$i] : (mem(V0p,arr(A_27a,bool)) => ( ! [V1e:$i] : (mem(V1e,arr(A_27a,ty_2Elist_2Elist(bool))) => ( ! [V2l:tp__c_ty_2Elist_2Elist_o] : ( ! [V3x:$i] : (mem(V3x,A_27a) => ( ! [V4t:tp__c_ty_2Elist_2Elist_o] : (p(ap(ap(c_2EEncode_2Ewf__encoder(A_27a),V0p),V1e)) => ((ap(ap(ap(c_2EDecode_2Eenc2dec(A_27a),V0p),V1e),inj__c_ty_2Elist_2Elist_o(V2l)) = ap(c_2Eoption_2ESOME(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))),ap(ap(c_2Epair_2E_2C(A_27a,ty_2Elist_2Elist(bool)),V3x),inj__c_ty_2Elist_2Elist_o(V4t)))) <=> (p(ap(V0p,V3x)) & (V2l = surj__c_ty_2Elist_2Elist_o(ap(ap(c_2Elist_2EAPPEND(bool),ap(V1e,V3x)),inj__c_ty_2Elist_2Elist_o(V4t)))))))))))))))))).
tff(conj_thm_2EDecode_2Eenc2dec__some__alt,lemma,(( ! [A_27a:del]: ( ! [V0p:$i] : (mem(V0p,arr(A_27a,bool)) => ( ! [V1e:$i] : (mem(V1e,arr(A_27a,ty_2Elist_2Elist(bool))) => ( ! [V2l:tp__c_ty_2Elist_2Elist_o] : ( ! [V3x:$i] : (mem(V3x,ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))) => (p(ap(ap(c_2EEncode_2Ewf__encoder(A_27a),V0p),V1e)) => ((ap(ap(ap(c_2EDecode_2Eenc2dec(A_27a),V0p),V1e),inj__c_ty_2Elist_2Elist_o(V2l)) = ap(c_2Eoption_2ESOME(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))),V3x)) <=> (p(ap(V0p,ap(c_2Epair_2EFST(A_27a,ty_2Elist_2Elist(bool)),V3x))) & (V2l = surj__c_ty_2Elist_2Elist_o(ap(ap(c_2Elist_2EAPPEND(bool),ap(V1e,ap(c_2Epair_2EFST(A_27a,ty_2Elist_2Elist(bool)),V3x))),ap(c_2Epair_2ESND(A_27a,ty_2Elist_2Elist(bool)),V3x))))))))))))))))).
tff(conj_thm_2EDecode_2Ewf__enc2dec,lemma,(( ! [A_27a:del]: ( ! [V0p:$i] : (mem(V0p,arr(A_27a,bool)) => ( ! [V1e:$i] : (mem(V1e,arr(A_27a,ty_2Elist_2Elist(bool))) => (p(ap(ap(c_2EEncode_2Ewf__encoder(A_27a),V0p),V1e)) => p(ap(ap(c_2EDecode_2Ewf__decoder(A_27a),V0p),ap(ap(c_2EDecode_2Eenc2dec(A_27a),V0p),V1e))))))))))).
tff(conj_thm_2EDecode_2Edec2enc__some,lemma,(( ! [A_27a:del]: ( ! [V0p:$i] : (mem(V0p,arr(A_27a,bool)) => ( ! [V1d:$i] : (mem(V1d,arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))))) => ( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3l:tp__c_ty_2Elist_2Elist_o] : (p(ap(ap(c_2EDecode_2Ewf__decoder(A_27a),V0p),V1d)) => (((surj__c_ty_2Elist_2Elist_o(ap(ap(c_2EDecode_2Edec2enc(A_27a),V1d),V2x)) = V3l) & p(ap(V0p,V2x))) <=> (ap(V1d,inj__c_ty_2Elist_2Elist_o(V3l)) = ap(c_2Eoption_2ESOME(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))),ap(ap(c_2Epair_2E_2C(A_27a,ty_2Elist_2Elist(bool)),V2x),c_2Elist_2ENIL(bool)))))))))))))))).
tff(conj_thm_2EDecode_2Edecode__dec2enc,conjecture,(( ! [A_27a:del]: ( ! [V0p:$i] : (mem(V0p,arr(A_27a,bool)) => ( ! [V1d:$i] : (mem(V1d,arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))))) => ( ! [V2x:$i] : (mem(V2x,A_27a) => ((p(ap(ap(c_2EDecode_2Ewf__decoder(A_27a),V0p),V1d)) & p(ap(V0p,V2x))) => (ap(V1d,ap(ap(c_2EDecode_2Edec2enc(A_27a),V1d),V2x)) = ap(c_2Eoption_2ESOME(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))),ap(ap(c_2Epair_2E_2C(A_27a,ty_2Elist_2Elist(bool)),V2x),c_2Elist_2ENIL(bool)))))))))))))).