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,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) => ((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)))))))))))))).
tff(conj_thm_2EDecode_2Edecode__dec2enc__append,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) => ( ! [V3t:tp__c_ty_2Elist_2Elist_o] : ((p(ap(ap(c_2EDecode_2Ewf__decoder(A_27a),V0p),V1d)) & p(ap(V0p,V2x))) => (ap(V1d,ap(ap(c_2Elist_2EAPPEND(bool),ap(ap(c_2EDecode_2Edec2enc(A_27a),V1d),V2x)),inj__c_ty_2Elist_2Elist_o(V3t))) = 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),inj__c_ty_2Elist_2Elist_o(V3t))))))))))))))).
tff(conj_thm_2EDecode_2Ewf__dec2enc,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))))) => (p(ap(ap(c_2EDecode_2Ewf__decoder(A_27a),V0p),V1d)) => p(ap(ap(c_2EEncode_2Ewf__encoder(A_27a),V0p),ap(c_2EDecode_2Edec2enc(A_27a),V1d))))))))))).
tff(conj_thm_2EDecode_2Edec2enc__enc2dec,lemma,(( ! [A_27a:del]: ( ! [V0p:$i] : (mem(V0p,arr(A_27a,bool)) => ( ! [V1e:$i] : (mem(V1e,arr(A_27a,ty_2Elist_2Elist(bool))) => ( ! [V2x:$i] : (mem(V2x,A_27a) => ((p(ap(ap(c_2EEncode_2Ewf__encoder(A_27a),V0p),V1e)) & p(ap(V0p,V2x))) => (surj__c_ty_2Elist_2Elist_o(ap(ap(c_2EDecode_2Edec2enc(A_27a),ap(ap(c_2EDecode_2Eenc2dec(A_27a),V0p),V1e)),V2x)) = surj__c_ty_2Elist_2Elist_o(ap(V1e,V2x))))))))))))).
tff(conj_thm_2EDecode_2Eenc2dec__dec2enc,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))))) => (p(ap(ap(c_2EDecode_2Ewf__decoder(A_27a),V0p),V1d)) => (ap(ap(c_2EDecode_2Eenc2dec(A_27a),V0p),ap(c_2EDecode_2Edec2enc(A_27a),V1d)) = V1d))))))))).
tff(ax_thm_2EDecode_2Edecode__unit__def,axiom,( ! [V0p:$i] : (mem(V0p,arr(ty_2Eone_2Eone,bool)) => (ap(c_2EDecode_2Edecode__unit,V0p) = ap(ap(c_2EDecode_2Eenc2dec(ty_2Eone_2Eone),V0p),c_2EEncode_2Eencode__unit))))).
tff(conj_thm_2EDecode_2Ewf__decode__unit,lemma,(( ! [V0p:$i] : (mem(V0p,arr(ty_2Eone_2Eone,bool)) => p(ap(ap(c_2EDecode_2Ewf__decoder(ty_2Eone_2Eone),V0p),ap(c_2EDecode_2Edecode__unit,V0p))))))).
tff(conj_thm_2EDecode_2Edec2enc__decode__unit,lemma,(( ! [V0p:$i] : (mem(V0p,arr(ty_2Eone_2Eone,bool)) => ( ! [V1x:tp__ty_2Eone_2Eone] : (p(ap(V0p,inj__ty_2Eone_2Eone(V1x))) => (surj__c_ty_2Elist_2Elist_o(ap(ap(c_2EDecode_2Edec2enc(ty_2Eone_2Eone),ap(c_2EDecode_2Edecode__unit,V0p)),inj__ty_2Eone_2Eone(V1x))) = surj__c_ty_2Elist_2Elist_o(ap(c_2EEncode_2Eencode__unit,inj__ty_2Eone_2Eone(V1x)))))))))).
tff(conj_thm_2EDecode_2Edecode__unit,lemma,(( ! [V0p:$i] : (mem(V0p,arr(ty_2Eone_2Eone,bool)) => ( ! [V1l:tp__c_ty_2Elist_2Elist_o] : (surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o(ap(ap(c_2EDecode_2Edecode__unit,V0p),inj__c_ty_2Elist_2Elist_o(V1l))) = surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Eone_2Eone_c_ty_2Elist_2Elist_o(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,ty_2Elist_2Elist(bool)))),ap(V0p,inj__ty_2Eone_2Eone(fo__c_2Eone_2Eone))),ap(c_2Eoption_2ESOME(ty_2Epair_2Eprod(ty_2Eone_2Eone,ty_2Elist_2Elist(bool))),ap(ap(c_2Epair_2E_2C(ty_2Eone_2Eone,ty_2Elist_2Elist(bool)),inj__ty_2Eone_2Eone(fo__c_2Eone_2Eone)),inj__c_ty_2Elist_2Elist_o(V1l)))),c_2Eoption_2ENONE(ty_2Epair_2Eprod(ty_2Eone_2Eone,ty_2Elist_2Elist(bool))))))))))).
tff(ax_thm_2EDecode_2Edecode__bool__def,axiom,( ! [V0p:$i] : (mem(V0p,arr(bool,bool)) => (ap(c_2EDecode_2Edecode__bool,V0p) = ap(ap(c_2EDecode_2Eenc2dec(bool),V0p),c_2EEncode_2Eencode__bool))))).
tff(conj_thm_2EDecode_2Ewf__decode__bool,lemma,(( ! [V0p:$i] : (mem(V0p,arr(bool,bool)) => p(ap(ap(c_2EDecode_2Ewf__decoder(bool),V0p),ap(c_2EDecode_2Edecode__bool,V0p))))))).
tff(conj_thm_2EDecode_2Edec2enc__decode__bool,lemma,(( ! [V0p:$i] : (mem(V0p,arr(bool,bool)) => ( ! [V1x:tp__o] : (p(ap(V0p,inj__o(V1x))) => (surj__c_ty_2Elist_2Elist_o(ap(ap(c_2EDecode_2Edec2enc(bool),ap(c_2EDecode_2Edecode__bool,V0p)),inj__o(V1x))) = surj__c_ty_2Elist_2Elist_o(ap(c_2EEncode_2Eencode__bool,inj__o(V1x)))))))))).
tff(conj_thm_2EDecode_2Edecode__bool,lemma,(( ! [V0p:$i] : (mem(V0p,arr(bool,bool)) => ( ! [V1l:tp__c_ty_2Elist_2Elist_o] : (surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o(ap(ap(c_2EDecode_2Edecode__bool,V0p),inj__c_ty_2Elist_2Elist_o(V1l))) = surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o(ap(ap(ap(c_2Elist_2Elist__CASE(bool,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(bool,ty_2Elist_2Elist(bool)))),inj__c_ty_2Elist_2Elist_o(V1l)),c_2Eoption_2ENONE(ty_2Epair_2Eprod(bool,ty_2Elist_2Elist(bool)))),f1726(V0p))))))))).
tff(ax_thm_2EDecode_2Edecode__prod__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p:$i] : (mem(V0p,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ! [V1d1:$i] : (mem(V1d1,arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))))) => ( ! [V2d2:$i] : (mem(V2d2,arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,ty_2Elist_2Elist(bool))))) => (ap(ap(ap(c_2EDecode_2Edecode__prod(A_27a,A_27b),V0p),V1d1),V2d2) = ap(ap(c_2EDecode_2Eenc2dec(ty_2Epair_2Eprod(A_27a,A_27b)),V0p),ap(ap(c_2EEncode_2Eencode__prod(A_27a,A_27b),ap(c_2EDecode_2Edec2enc(A_27a),V1d1)),ap(c_2EDecode_2Edec2enc(A_27b),V2d2))))))))))))).
tff(conj_thm_2EDecode_2Ewf__decode__prod,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p1:$i] : (mem(V0p1,arr(A_27a,bool)) => ( ! [V1p2:$i] : (mem(V1p2,arr(A_27b,bool)) => ( ! [V2d1:$i] : (mem(V2d1,arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))))) => ( ! [V3d2:$i] : (mem(V3d2,arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,ty_2Elist_2Elist(bool))))) => ((p(ap(ap(c_2EDecode_2Ewf__decoder(A_27a),V0p1),V2d1)) & p(ap(ap(c_2EDecode_2Ewf__decoder(A_27b),V1p2),V3d2))) => p(ap(ap(c_2EDecode_2Ewf__decoder(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2EEncode_2Elift__prod(A_27a,A_27b),V0p1),V1p2)),ap(ap(ap(c_2EDecode_2Edecode__prod(A_27a,A_27b),ap(ap(c_2EEncode_2Elift__prod(A_27a,A_27b),V0p1),V1p2)),V2d1),V3d2)))))))))))))))).
tff(conj_thm_2EDecode_2Edec2enc__decode__prod,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p1:$i] : (mem(V0p1,arr(A_27a,bool)) => ( ! [V1p2:$i] : (mem(V1p2,arr(A_27b,bool)) => ( ! [V2d1:$i] : (mem(V2d1,arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))))) => ( ! [V3d2:$i] : (mem(V3d2,arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,ty_2Elist_2Elist(bool))))) => ( ! [V4x:$i] : (mem(V4x,ty_2Epair_2Eprod(A_27a,A_27b)) => ((p(ap(ap(c_2EDecode_2Ewf__decoder(A_27a),V0p1),V2d1)) & (p(ap(ap(c_2EDecode_2Ewf__decoder(A_27b),V1p2),V3d2)) & p(ap(ap(ap(c_2EEncode_2Elift__prod(A_27a,A_27b),V0p1),V1p2),V4x)))) => (surj__c_ty_2Elist_2Elist_o(ap(ap(c_2EDecode_2Edec2enc(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(ap(c_2EDecode_2Edecode__prod(A_27a,A_27b),ap(ap(c_2EEncode_2Elift__prod(A_27a,A_27b),V0p1),V1p2)),V2d1),V3d2)),V4x)) = surj__c_ty_2Elist_2Elist_o(ap(ap(ap(c_2EEncode_2Eencode__prod(A_27a,A_27b),ap(c_2EDecode_2Edec2enc(A_27a),V2d1)),ap(c_2EDecode_2Edec2enc(A_27b),V3d2)),V4x)))))))))))))))))).
tff(conj_thm_2EDecode_2Eencode__then__decode__prod,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p1:$i] : (mem(V0p1,arr(A_27a,bool)) => ( ! [V1p2:$i] : (mem(V1p2,arr(A_27b,bool)) => ( ! [V2e1:$i] : (mem(V2e1,arr(A_27a,ty_2Elist_2Elist(bool))) => ( ! [V3e2:$i] : (mem(V3e2,arr(A_27b,ty_2Elist_2Elist(bool))) => ( ! [V4l:$i] : (mem(V4l,ty_2Epair_2Eprod(A_27a,A_27b)) => ( ! [V5t:tp__c_ty_2Elist_2Elist_o] : ((p(ap(ap(c_2EEncode_2Ewf__encoder(A_27a),V0p1),V2e1)) & (p(ap(ap(c_2EEncode_2Ewf__encoder(A_27b),V1p2),V3e2)) & p(ap(ap(ap(c_2EEncode_2Elift__prod(A_27a,A_27b),V0p1),V1p2),V4l)))) => (ap(ap(ap(ap(c_2EDecode_2Edecode__prod(A_27a,A_27b),ap(ap(c_2EEncode_2Elift__prod(A_27a,A_27b),V0p1),V1p2)),ap(ap(c_2EDecode_2Eenc2dec(A_27a),V0p1),V2e1)),ap(ap(c_2EDecode_2Eenc2dec(A_27b),V1p2),V3e2)),ap(ap(c_2Elist_2EAPPEND(bool),ap(ap(ap(c_2EEncode_2Eencode__prod(A_27a,A_27b),V2e1),V3e2),V4l)),inj__c_ty_2Elist_2Elist_o(V5t))) = ap(c_2Eoption_2ESOME(ty_2Epair_2Eprod(ty_2Epair_2Eprod(A_27a,A_27b),ty_2Elist_2Elist(bool))),ap(ap(c_2Epair_2E_2C(ty_2Epair_2Eprod(A_27a,A_27b),ty_2Elist_2Elist(bool)),V4l),inj__c_ty_2Elist_2Elist_o(V5t)))))))))))))))))))).
tff(conj_thm_2EDecode_2Edecode__prod,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p1:$i] : (mem(V0p1,arr(A_27a,bool)) => ( ! [V1d1:$i] : (mem(V1d1,arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))))) => ( ! [V2p2:$i] : (mem(V2p2,arr(A_27b,bool)) => ( ! [V3d2:$i] : (mem(V3d2,arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,ty_2Elist_2Elist(bool))))) => ( ! [V4l:tp__c_ty_2Elist_2Elist_o] : ((p(ap(ap(c_2EDecode_2Ewf__decoder(A_27a),V0p1),V1d1)) & p(ap(ap(c_2EDecode_2Ewf__decoder(A_27b),V2p2),V3d2))) => (ap(ap(ap(ap(c_2EDecode_2Edecode__prod(A_27a,A_27b),ap(ap(c_2EEncode_2Elift__prod(A_27a,A_27b),V0p1),V2p2)),V1d1),V3d2),inj__c_ty_2Elist_2Elist_o(V4l)) = ap(ap(ap(c_2Eoption_2Eoption__CASE(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool)),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Epair_2Eprod(A_27a,A_27b),ty_2Elist_2Elist(bool)))),ap(V1d1,inj__c_ty_2Elist_2Elist_o(V4l))),c_2Eoption_2ENONE(ty_2Epair_2Eprod(ty_2Epair_2Eprod(A_27a,A_27b),ty_2Elist_2Elist(bool)))),f1732(A_27b,A_27a,V3d2))))))))))))))))).
tff(ax_thm_2EDecode_2Edecode__sum__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p:$i] : (mem(V0p,arr(ty_2Esum_2Esum(A_27a,A_27b),bool)) => ( ! [V1d1:$i] : (mem(V1d1,arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))))) => ( ! [V2d2:$i] : (mem(V2d2,arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,ty_2Elist_2Elist(bool))))) => (ap(ap(ap(c_2EDecode_2Edecode__sum(A_27a,A_27b),V0p),V1d1),V2d2) = ap(ap(c_2EDecode_2Eenc2dec(ty_2Esum_2Esum(A_27a,A_27b)),V0p),ap(ap(c_2EEncode_2Eencode__sum(A_27a,A_27b),ap(c_2EDecode_2Edec2enc(A_27a),V1d1)),ap(c_2EDecode_2Edec2enc(A_27b),V2d2))))))))))))).
tff(conj_thm_2EDecode_2Ewf__decode__sum,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p1:$i] : (mem(V0p1,arr(A_27a,bool)) => ( ! [V1p2:$i] : (mem(V1p2,arr(A_27b,bool)) => ( ! [V2d1:$i] : (mem(V2d1,arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))))) => ( ! [V3d2:$i] : (mem(V3d2,arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,ty_2Elist_2Elist(bool))))) => ((p(ap(ap(c_2EDecode_2Ewf__decoder(A_27a),V0p1),V2d1)) & p(ap(ap(c_2EDecode_2Ewf__decoder(A_27b),V1p2),V3d2))) => p(ap(ap(c_2EDecode_2Ewf__decoder(ty_2Esum_2Esum(A_27a,A_27b)),ap(ap(c_2EEncode_2Elift__sum(A_27a,A_27b),V0p1),V1p2)),ap(ap(ap(c_2EDecode_2Edecode__sum(A_27a,A_27b),ap(ap(c_2EEncode_2Elift__sum(A_27a,A_27b),V0p1),V1p2)),V2d1),V3d2)))))))))))))))).
tff(conj_thm_2EDecode_2Edec2enc__decode__sum,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p1:$i] : (mem(V0p1,arr(A_27a,bool)) => ( ! [V1p2:$i] : (mem(V1p2,arr(A_27b,bool)) => ( ! [V2d1:$i] : (mem(V2d1,arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))))) => ( ! [V3d2:$i] : (mem(V3d2,arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,ty_2Elist_2Elist(bool))))) => ( ! [V4x:$i] : (mem(V4x,ty_2Esum_2Esum(A_27a,A_27b)) => ((p(ap(ap(c_2EDecode_2Ewf__decoder(A_27a),V0p1),V2d1)) & (p(ap(ap(c_2EDecode_2Ewf__decoder(A_27b),V1p2),V3d2)) & p(ap(ap(ap(c_2EEncode_2Elift__sum(A_27a,A_27b),V0p1),V1p2),V4x)))) => (surj__c_ty_2Elist_2Elist_o(ap(ap(c_2EDecode_2Edec2enc(ty_2Esum_2Esum(A_27a,A_27b)),ap(ap(ap(c_2EDecode_2Edecode__sum(A_27a,A_27b),ap(ap(c_2EEncode_2Elift__sum(A_27a,A_27b),V0p1),V1p2)),V2d1),V3d2)),V4x)) = surj__c_ty_2Elist_2Elist_o(ap(ap(ap(c_2EEncode_2Eencode__sum(A_27a,A_27b),ap(c_2EDecode_2Edec2enc(A_27a),V2d1)),ap(c_2EDecode_2Edec2enc(A_27b),V3d2)),V4x)))))))))))))))))).
tff(conj_thm_2EDecode_2Eencode__then__decode__sum,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p1:$i] : (mem(V0p1,arr(A_27a,bool)) => ( ! [V1p2:$i] : (mem(V1p2,arr(A_27b,bool)) => ( ! [V2e1:$i] : (mem(V2e1,arr(A_27a,ty_2Elist_2Elist(bool))) => ( ! [V3e2:$i] : (mem(V3e2,arr(A_27b,ty_2Elist_2Elist(bool))) => ( ! [V4l:$i] : (mem(V4l,ty_2Esum_2Esum(A_27a,A_27b)) => ( ! [V5t:tp__c_ty_2Elist_2Elist_o] : ((p(ap(ap(c_2EEncode_2Ewf__encoder(A_27a),V0p1),V2e1)) & (p(ap(ap(c_2EEncode_2Ewf__encoder(A_27b),V1p2),V3e2)) & p(ap(ap(ap(c_2EEncode_2Elift__sum(A_27a,A_27b),V0p1),V1p2),V4l)))) => (ap(ap(ap(ap(c_2EDecode_2Edecode__sum(A_27a,A_27b),ap(ap(c_2EEncode_2Elift__sum(A_27a,A_27b),V0p1),V1p2)),ap(ap(c_2EDecode_2Eenc2dec(A_27a),V0p1),V2e1)),ap(ap(c_2EDecode_2Eenc2dec(A_27b),V1p2),V3e2)),ap(ap(c_2Elist_2EAPPEND(bool),ap(ap(ap(c_2EEncode_2Eencode__sum(A_27a,A_27b),V2e1),V3e2),V4l)),inj__c_ty_2Elist_2Elist_o(V5t))) = ap(c_2Eoption_2ESOME(ty_2Epair_2Eprod(ty_2Esum_2Esum(A_27a,A_27b),ty_2Elist_2Elist(bool))),ap(ap(c_2Epair_2E_2C(ty_2Esum_2Esum(A_27a,A_27b),ty_2Elist_2Elist(bool)),V4l),inj__c_ty_2Elist_2Elist_o(V5t)))))))))))))))))))).
tff(conj_thm_2EDecode_2Edecode__sum,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p1:$i] : (mem(V0p1,arr(A_27a,bool)) => ( ! [V1d1:$i] : (mem(V1d1,arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))))) => ( ! [V2p2:$i] : (mem(V2p2,arr(A_27b,bool)) => ( ! [V3d2:$i] : (mem(V3d2,arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,ty_2Elist_2Elist(bool))))) => ( ! [V4l:tp__c_ty_2Elist_2Elist_o] : ((p(ap(ap(c_2EDecode_2Ewf__decoder(A_27a),V0p1),V1d1)) & p(ap(ap(c_2EDecode_2Ewf__decoder(A_27b),V2p2),V3d2))) => (ap(ap(ap(ap(c_2EDecode_2Edecode__sum(A_27a,A_27b),ap(ap(c_2EEncode_2Elift__sum(A_27a,A_27b),V0p1),V2p2)),V1d1),V3d2),inj__c_ty_2Elist_2Elist_o(V4l)) = ap(ap(ap(c_2Elist_2Elist__CASE(bool,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Esum_2Esum(A_27a,A_27b),ty_2Elist_2Elist(bool)))),inj__c_ty_2Elist_2Elist_o(V4l)),c_2Eoption_2ENONE(ty_2Epair_2Eprod(ty_2Esum_2Esum(A_27a,A_27b),ty_2Elist_2Elist(bool)))),f1740(A_27b,A_27a,V1d1,V3d2))))))))))))))))).
tff(ax_thm_2EDecode_2Edecode__option__def,axiom,( ! [A_27a:del]: ( ! [V0p:$i] : (mem(V0p,arr(ty_2Eoption_2Eoption(A_27a),bool)) => ( ! [V1d:$i] : (mem(V1d,arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))))) => (ap(ap(c_2EDecode_2Edecode__option(A_27a),V0p),V1d) = ap(ap(c_2EDecode_2Eenc2dec(ty_2Eoption_2Eoption(A_27a)),V0p),ap(c_2EEncode_2Eencode__option(A_27a),ap(c_2EDecode_2Edec2enc(A_27a),V1d)))))))))).
tff(conj_thm_2EDecode_2Ewf__decode__option,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))))) => (p(ap(ap(c_2EDecode_2Ewf__decoder(A_27a),V0p),V1d)) => p(ap(ap(c_2EDecode_2Ewf__decoder(ty_2Eoption_2Eoption(A_27a)),ap(c_2EEncode_2Elift__option(A_27a),V0p)),ap(ap(c_2EDecode_2Edecode__option(A_27a),ap(c_2EEncode_2Elift__option(A_27a),V0p)),V1d))))))))))).
tff(conj_thm_2EDecode_2Edec2enc__decode__option,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,ty_2Eoption_2Eoption(A_27a)) => ((p(ap(ap(c_2EDecode_2Ewf__decoder(A_27a),V0p),V1d)) & p(ap(ap(c_2EEncode_2Elift__option(A_27a),V0p),V2x))) => (surj__c_ty_2Elist_2Elist_o(ap(ap(c_2EDecode_2Edec2enc(ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2EDecode_2Edecode__option(A_27a),ap(c_2EEncode_2Elift__option(A_27a),V0p)),V1d)),V2x)) = surj__c_ty_2Elist_2Elist_o(ap(ap(c_2EEncode_2Eencode__option(A_27a),ap(c_2EDecode_2Edec2enc(A_27a),V1d)),V2x))))))))))))).
tff(conj_thm_2EDecode_2Eencode__then__decode__option,lemma,(( ! [A_27a:del]: ( ! [V0p:$i] : (mem(V0p,arr(A_27a,bool)) => ( ! [V1e:$i] : (mem(V1e,arr(A_27a,ty_2Elist_2Elist(bool))) => ( ! [V2l:$i] : (mem(V2l,ty_2Eoption_2Eoption(A_27a)) => ( ! [V3t:tp__c_ty_2Elist_2Elist_o] : ((p(ap(ap(c_2EEncode_2Ewf__encoder(A_27a),V0p),V1e)) & p(ap(ap(c_2EEncode_2Elift__option(A_27a),V0p),V2l))) => (ap(ap(ap(c_2EDecode_2Edecode__option(A_27a),ap(c_2EEncode_2Elift__option(A_27a),V0p)),ap(ap(c_2EDecode_2Eenc2dec(A_27a),V0p),V1e)),ap(ap(c_2Elist_2EAPPEND(bool),ap(ap(c_2EEncode_2Eencode__option(A_27a),V1e),V2l)),inj__c_ty_2Elist_2Elist_o(V3t))) = ap(c_2Eoption_2ESOME(ty_2Epair_2Eprod(ty_2Eoption_2Eoption(A_27a),ty_2Elist_2Elist(bool))),ap(ap(c_2Epair_2E_2C(ty_2Eoption_2Eoption(A_27a),ty_2Elist_2Elist(bool)),V2l),inj__c_ty_2Elist_2Elist_o(V3t))))))))))))))).
tff(conj_thm_2EDecode_2Edecode__option,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))))) => ( ! [V2l:tp__c_ty_2Elist_2Elist_o] : (p(ap(ap(c_2EDecode_2Ewf__decoder(A_27a),V0p),V1d)) => (ap(ap(ap(c_2EDecode_2Edecode__option(A_27a),ap(c_2EEncode_2Elift__option(A_27a),V0p)),V1d),inj__c_ty_2Elist_2Elist_o(V2l)) = ap(ap(ap(c_2Elist_2Elist__CASE(bool,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eoption_2Eoption(A_27a),ty_2Elist_2Elist(bool)))),inj__c_ty_2Elist_2Elist_o(V2l)),c_2Eoption_2ENONE(ty_2Epair_2Eprod(ty_2Eoption_2Eoption(A_27a),ty_2Elist_2Elist(bool)))),f1745(A_27a,V1d)))))))))))).
tff(ax_thm_2EDecode_2Edecode__list__def,axiom,( ! [A_27a:del]: ( ! [V0p:$i] : (mem(V0p,arr(ty_2Elist_2Elist(A_27a),bool)) => ( ! [V1d:$i] : (mem(V1d,arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))))) => (ap(ap(c_2EDecode_2Edecode__list(A_27a),V0p),V1d) = ap(ap(c_2EDecode_2Eenc2dec(ty_2Elist_2Elist(A_27a)),V0p),ap(c_2EEncode_2Eencode__list(A_27a),ap(c_2EDecode_2Edec2enc(A_27a),V1d)))))))))).
tff(conj_thm_2EDecode_2Ewf__decode__list,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))))) => (p(ap(ap(c_2EDecode_2Ewf__decoder(A_27a),V0p),V1d)) => p(ap(ap(c_2EDecode_2Ewf__decoder(ty_2Elist_2Elist(A_27a)),ap(c_2Elist_2EEVERY(A_27a),V0p)),ap(ap(c_2EDecode_2Edecode__list(A_27a),ap(c_2Elist_2EEVERY(A_27a),V0p)),V1d))))))))))).
tff(conj_thm_2EDecode_2Edec2enc__decode__list,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,ty_2Elist_2Elist(A_27a)) => ((p(ap(ap(c_2EDecode_2Ewf__decoder(A_27a),V0p),V1d)) & p(ap(ap(c_2Elist_2EEVERY(A_27a),V0p),V2x))) => (surj__c_ty_2Elist_2Elist_o(ap(ap(c_2EDecode_2Edec2enc(ty_2Elist_2Elist(A_27a)),ap(ap(c_2EDecode_2Edecode__list(A_27a),ap(c_2Elist_2EEVERY(A_27a),V0p)),V1d)),V2x)) = surj__c_ty_2Elist_2Elist_o(ap(ap(c_2EEncode_2Eencode__list(A_27a),ap(c_2EDecode_2Edec2enc(A_27a),V1d)),V2x))))))))))))).
tff(conj_thm_2EDecode_2Eencode__then__decode__list,lemma,(( ! [A_27a:del]: ( ! [V0p:$i] : (mem(V0p,arr(A_27a,bool)) => ( ! [V1e:$i] : (mem(V1e,arr(A_27a,ty_2Elist_2Elist(bool))) => ( ! [V2l:$i] : (mem(V2l,ty_2Elist_2Elist(A_27a)) => ( ! [V3t:tp__c_ty_2Elist_2Elist_o] : ((p(ap(ap(c_2EEncode_2Ewf__encoder(A_27a),V0p),V1e)) & p(ap(ap(c_2Elist_2EEVERY(A_27a),V0p),V2l))) => (ap(ap(ap(c_2EDecode_2Edecode__list(A_27a),ap(c_2Elist_2EEVERY(A_27a),V0p)),ap(ap(c_2EDecode_2Eenc2dec(A_27a),V0p),V1e)),ap(ap(c_2Elist_2EAPPEND(bool),ap(ap(c_2EEncode_2Eencode__list(A_27a),V1e),V2l)),inj__c_ty_2Elist_2Elist_o(V3t))) = ap(c_2Eoption_2ESOME(ty_2Epair_2Eprod(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(bool))),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(bool)),V2l),inj__c_ty_2Elist_2Elist_o(V3t))))))))))))))).
tff(conj_thm_2EDecode_2Edecode__list,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))))) => ( ! [V2l:tp__c_ty_2Elist_2Elist_o] : (p(ap(ap(c_2EDecode_2Ewf__decoder(A_27a),V0p),V1d)) => (ap(ap(ap(c_2EDecode_2Edecode__list(A_27a),ap(c_2Elist_2EEVERY(A_27a),V0p)),V1d),inj__c_ty_2Elist_2Elist_o(V2l)) = ap(ap(ap(c_2Elist_2Elist__CASE(bool,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(bool)))),inj__c_ty_2Elist_2Elist_o(V2l)),c_2Eoption_2ENONE(ty_2Epair_2Eprod(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(bool)))),f1753(A_27a,V1d,V0p)))))))))))).
tff(ax_thm_2EDecode_2Edecode__blist__def,axiom,( ! [A_27a:del]: ( ! [V0p:$i] : (mem(V0p,arr(ty_2Elist_2Elist(A_27a),bool)) => ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2d:$i] : (mem(V2d,arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))))) => (ap(ap(ap(c_2EDecode_2Edecode__blist(A_27a),V0p),inj__ty_2Enum_2Enum(V1m)),V2d) = ap(ap(c_2EDecode_2Eenc2dec(ty_2Elist_2Elist(A_27a)),V0p),ap(ap(c_2EEncode_2Eencode__blist(bool,A_27a),inj__ty_2Enum_2Enum(V1m)),ap(c_2EDecode_2Edec2enc(A_27a),V2d))))))))))).
tff(conj_thm_2EDecode_2Ewf__decode__blist,lemma,(( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1p:$i] : (mem(V1p,arr(A_27a,bool)) => ( ! [V2d:$i] : (mem(V2d,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),V1p),V2d)) => p(ap(ap(c_2EDecode_2Ewf__decoder(ty_2Elist_2Elist(A_27a)),ap(ap(c_2EEncode_2Elift__blist(A_27a),inj__ty_2Enum_2Enum(V0m)),V1p)),ap(ap(ap(c_2EDecode_2Edecode__blist(A_27a),ap(ap(c_2EEncode_2Elift__blist(A_27a),inj__ty_2Enum_2Enum(V0m)),V1p)),inj__ty_2Enum_2Enum(V0m)),V2d)))))))))))).
tff(conj_thm_2EDecode_2Edec2enc__decode__blist,lemma,(( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1p:$i] : (mem(V1p,arr(A_27a,bool)) => ( ! [V2d:$i] : (mem(V2d,arr(ty_2Elist_2Elist(bool),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Elist_2Elist(bool))))) => ( ! [V3l:$i] : (mem(V3l,ty_2Elist_2Elist(A_27a)) => ((p(ap(ap(c_2EDecode_2Ewf__decoder(A_27a),V1p),V2d)) & p(ap(ap(ap(c_2EEncode_2Elift__blist(A_27a),inj__ty_2Enum_2Enum(V0m)),V1p),V3l))) => (surj__c_ty_2Elist_2Elist_o(ap(ap(c_2EDecode_2Edec2enc(ty_2Elist_2Elist(A_27a)),ap(ap(ap(c_2EDecode_2Edecode__blist(A_27a),ap(ap(c_2EEncode_2Elift__blist(A_27a),inj__ty_2Enum_2Enum(V0m)),V1p)),inj__ty_2Enum_2Enum(V0m)),V2d)),V3l)) = surj__c_ty_2Elist_2Elist_o(ap(ap(ap(c_2EEncode_2Eencode__blist(bool,A_27a),inj__ty_2Enum_2Enum(V0m)),ap(c_2EDecode_2Edec2enc(A_27a),V2d)),V3l)))))))))))))).
tff(conj_thm_2EDecode_2Eencode__then__decode__blist,conjecture,(( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1p:$i] : (mem(V1p,arr(A_27a,bool)) => ( ! [V2e:$i] : (mem(V2e,arr(A_27a,ty_2Elist_2Elist(bool))) => ( ! [V3l:$i] : (mem(V3l,ty_2Elist_2Elist(A_27a)) => ( ! [V4t:tp__c_ty_2Elist_2Elist_o] : ((p(ap(ap(c_2EEncode_2Ewf__encoder(A_27a),V1p),V2e)) & p(ap(ap(ap(c_2EEncode_2Elift__blist(A_27a),inj__ty_2Enum_2Enum(V0m)),V1p),V3l))) => (ap(ap(ap(ap(c_2EDecode_2Edecode__blist(A_27a),ap(ap(c_2EEncode_2Elift__blist(A_27a),inj__ty_2Enum_2Enum(V0m)),V1p)),inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2EDecode_2Eenc2dec(A_27a),V1p),V2e)),ap(ap(c_2Elist_2EAPPEND(bool),ap(ap(ap(c_2EEncode_2Eencode__blist(bool,A_27a),inj__ty_2Enum_2Enum(V0m)),V2e),V3l)),inj__c_ty_2Elist_2Elist_o(V4t))) = ap(c_2Eoption_2ESOME(ty_2Epair_2Eprod(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(bool))),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(bool)),V3l),inj__c_ty_2Elist_2Elist_o(V4t)))))))))))))))).