include('Axioms/dft^2.ax').
thf(tp_c_2EDecode_2Edec2enc,type,(c_2EDecode_2Edec2enc:(del>$i))).
thf(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)))))).
thf(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)).
thf(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))).
thf(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))).
thf(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))).
thf(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)))))).
thf(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)))))).
thf(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)).
thf(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))).
thf(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))).
thf(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))).
thf(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))))).
thf(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)))))).
thf(tp_c_2EDecode_2Edec__bnum,type,(c_2EDecode_2Edec__bnum:$i)).
thf(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))))))).
thf(tp_c_2EDecode_2Edecode__blist,type,(c_2EDecode_2Edecode__blist:(del>$i))).
thf(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)))))))))).
thf(tp_c_2EDecode_2Edecode__bnum,type,(c_2EDecode_2Edecode__bnum:$i)).
thf(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)))))))).
thf(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)).
thf(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))).
thf(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))).
thf(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))).
thf(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)))))).
thf(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)))))).
thf(tp_c_2EDecode_2Edecode__bool,type,(c_2EDecode_2Edecode__bool:$i)).
thf(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))))))).
thf(tp_c_2EDecode_2Edecode__list,type,(c_2EDecode_2Edecode__list:(del>$i))).
thf(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))))))))).
thf(tp_c_2EDecode_2Edecode__num,type,(c_2EDecode_2Edecode__num:$i)).
thf(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))))))).
thf(tp_c_2EDecode_2Edecode__option,type,(c_2EDecode_2Edecode__option:(del>$i))).
thf(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))))))))).
thf(tp_c_2EDecode_2Edecode__prod,type,(c_2EDecode_2Edecode__prod:(del>(del>$i)))).
thf(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))))))))))).
thf(tp_c_2EDecode_2Edecode__sum,type,(c_2EDecode_2Edecode__sum:(del>(del>$i)))).
thf(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))))))))))).
thf(tp_c_2EDecode_2Edecode__tree,type,(c_2EDecode_2Edecode__tree:(del>$i))).
thf(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))))))))).
thf(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)).
thf(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))).
thf(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))).
thf(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))).
thf(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)))))).
thf(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)))))).
thf(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)).
thf(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))).
thf(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))).
thf(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))).
thf(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))))).
thf(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)))))).
thf(tp_c_2EDecode_2Edecode__unit,type,(c_2EDecode_2Edecode__unit:$i)).
thf(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))))))).
thf(tp_c_2EDecode_2Eenc2dec,type,(c_2EDecode_2Eenc2dec:(del>$i))).
thf(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))))))))).
thf(tp_c_2EDecode_2Ewf__decoder,type,(c_2EDecode_2Ewf__decoder:(del>$i))).
thf(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))))).
thf(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))@(lam@(ty_2Elist_2Elist@bool)@(^ [V3a:$i] : (ap@(c_2Ebool_2E_21@(ty_2Elist_2Elist@bool))@(lam@(ty_2Elist_2Elist@bool)@(^ [V4b:$i] : (ap@(c_2Ebool_2E_21@(ty_2Elist_2Elist@bool))@(lam@(ty_2Elist_2Elist@bool)@(^ [V5c:$i] : (ap@(ap@(c_2Emin_2E_3D@bool)@(ap@(ap@(c_2Emin_2E_3D@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27a@(ty_2Elist_2Elist@bool))))@(ap@V1d@V4b))@(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)@V5c))))@(ap@(ap@(c_2Emin_2E_3D@(ty_2Elist_2Elist@bool))@V4b)@(ap@(ap@(c_2Elist_2EAPPEND@bool)@V3a)@V5c)))))))))))))@(ap@(c_2Ebool_2E_21@(ty_2Elist_2Elist@bool))@(lam@(ty_2Elist_2Elist@bool)@(^ [V6a:$i] : (ap@(c_2Ebool_2E_21@(ty_2Elist_2Elist@bool))@(lam@(ty_2Elist_2Elist@bool)@(^ [V7b:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(c_2Emin_2E_3D@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27a@(ty_2Elist_2Elist@bool))))@(ap@V1d@V6a))@(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)@V7b))))))))))))))))))))).
thf(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)@(lam@A_27a@(^ [V3x:$i] : (ap@(c_2Ebool_2E_3F@(ty_2Elist_2Elist@bool))@(lam@(ty_2Elist_2Elist@bool)@(^ [V4t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0p@V3x))@(ap@(ap@(c_2Emin_2E_3D@(ty_2Elist_2Elist@bool))@(inj__c_ty_2Elist_2Elist_o @ V2l))@(ap@(ap@(c_2Elist_2EAPPEND@bool)@(ap@V1e@V3x))@V4t))))))))))@(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)@(lam@A_27a@(^ [V5x:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V6t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0p@V5x))@(ap@(ap@(c_2Emin_2E_3D@(ty_2Elist_2Elist@bool))@(inj__c_ty_2Elist_2Elist_o @ V2l))@(ap@(ap@(c_2Elist_2EAPPEND@bool)@(ap@V1e@V5x))@V6t)))))))))))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@A_27a@(ty_2Elist_2Elist@bool)))))))))))).
thf(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))@(lam@(ty_2Elist_2Elist@bool)@(^ [V2l:$i] : (ap@(ap@(c_2Emin_2E_3D@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27a@(ty_2Elist_2Elist@bool))))@(ap@V0d@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))@V1x)@(c_2Elist_2ENIL@bool))))))))))))))).
thf(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))))))))))))))))).
thf(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))))))))))))))))).
thf(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)))))))))))))))).
thf(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)))))))))).
thf(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))))))))))))))).
thf(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))))))))))))).
thf(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)))))))))))))).
thf(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)))))))))).
thf(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)))))))))))).
thf(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)))))))).
thf(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))))).
thf(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)))))).
thf(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))))))))).
thf(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)))))))))).
thf(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))))).
thf(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)))))).
thf(conj_thm_2EDecode_2Edec2enc__decode__bool,lemma,( ! [V0p:$i] : ((mem@V0p@(arr@bool@bool)) => ( ! [V1x:$i] : ((mem@V1x@bool) => ((p@(ap@V0p@V1x)) => ((surj__c_ty_2Elist_2Elist_o @ (ap@(ap@(c_2EDecode_2Edec2enc@bool)@(ap@c_2EDecode_2Edecode__bool@V0p))@V1x)) = (surj__c_ty_2Elist_2Elist_o @ (ap@c_2EEncode_2Eencode__bool@V1x))))))))).
thf(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))))@(lam@bool@(^ [V2h:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V3t:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@bool@(ty_2Elist_2Elist@bool))))@(ap@V0p@V2h))@(ap@(c_2Eoption_2ESOME@(ty_2Epair_2Eprod@bool@(ty_2Elist_2Elist@bool)))@(ap@(ap@(c_2Epair_2E_2C@bool@(ty_2Elist_2Elist@bool))@V2h)@V3t)))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@bool@(ty_2Elist_2Elist@bool))))))))))))))).
thf(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))))))))))))).
thf(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))))))))))))))).
thf(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))))))))))))))))).
thf(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))))))))))))))))))).
thf(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))))@(lam@(ty_2Epair_2Eprod@A_27a@(ty_2Elist_2Elist@bool))@(^ [V5v1:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@(ty_2Epair_2Eprod@A_27a@A_27b)@(ty_2Elist_2Elist@bool)))@A_27a@(ty_2Elist_2Elist@bool))@V5v1)@(lam@A_27a@(^ [V6x:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V7t:$i] : (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Epair_2Eprod@A_27b@(ty_2Elist_2Elist@bool))@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@(ty_2Epair_2Eprod@A_27a@A_27b)@(ty_2Elist_2Elist@bool))))@(ap@V3d2@V7t))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@(ty_2Epair_2Eprod@A_27a@A_27b)@(ty_2Elist_2Elist@bool))))@(lam@(ty_2Epair_2Eprod@A_27b@(ty_2Elist_2Elist@bool))@(^ [V8v:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@(ty_2Epair_2Eprod@A_27a@A_27b)@(ty_2Elist_2Elist@bool)))@A_27b@(ty_2Elist_2Elist@bool))@V8v)@(lam@A_27b@(^ [V9y:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V10t_27:$i] : (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))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V6x)@V9y))@V10t_27)))))))))))))))))))))))))))))))).
thf(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))))))))))))).
thf(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))))))))))))))).
thf(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))))))))))))))))).
thf(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))))))))))))))))))).
thf(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))))@(lam@bool@(^ [V5v1:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V6t:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@(ty_2Esum_2Esum@A_27a@A_27b)@(ty_2Elist_2Elist@bool))))@V5v1)@(ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Epair_2Eprod@A_27a@(ty_2Elist_2Elist@bool))@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@(ty_2Esum_2Esum@A_27a@A_27b)@(ty_2Elist_2Elist@bool))))@(ap@V1d1@V6t))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@(ty_2Esum_2Esum@A_27a@A_27b)@(ty_2Elist_2Elist@bool))))@(lam@(ty_2Epair_2Eprod@A_27a@(ty_2Elist_2Elist@bool))@(^ [V7v:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@(ty_2Esum_2Esum@A_27a@A_27b)@(ty_2Elist_2Elist@bool)))@A_27a@(ty_2Elist_2Elist@bool))@V7v)@(lam@A_27a@(^ [V8x:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V9t_27:$i] : (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))@(ap@(c_2Esum_2EINL@A_27a@A_27b)@V8x))@V9t_27)))))))))))@(ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Epair_2Eprod@A_27b@(ty_2Elist_2Elist@bool))@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@(ty_2Esum_2Esum@A_27a@A_27b)@(ty_2Elist_2Elist@bool))))@(ap@V3d2@V6t))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@(ty_2Esum_2Esum@A_27a@A_27b)@(ty_2Elist_2Elist@bool))))@(lam@(ty_2Epair_2Eprod@A_27b@(ty_2Elist_2Elist@bool))@(^ [V10v:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@(ty_2Esum_2Esum@A_27a@A_27b)@(ty_2Elist_2Elist@bool)))@A_27b@(ty_2Elist_2Elist@bool))@V10v)@(lam@A_27b@(^ [V11x:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V12t_27:$i] : (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))@(ap@(c_2Esum_2EINR@A_27a@A_27b)@V11x))@V12t_27)))))))))))))))))))))))))))))).
thf(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)))))))))).
thf(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)))))))))).
thf(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)))))))))))).
thf(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)))))))))))))).
thf(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))))@(lam@bool@(^ [V3v1:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V4t:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@(ty_2Eoption_2Eoption@A_27a)@(ty_2Elist_2Elist@bool))))@V3v1)@(ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Epair_2Eprod@A_27a@(ty_2Elist_2Elist@bool))@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@(ty_2Eoption_2Eoption@A_27a)@(ty_2Elist_2Elist@bool))))@(ap@V1d@V4t))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@(ty_2Eoption_2Eoption@A_27a)@(ty_2Elist_2Elist@bool))))@(lam@(ty_2Epair_2Eprod@A_27a@(ty_2Elist_2Elist@bool))@(^ [V5v:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@(ty_2Eoption_2Eoption@A_27a)@(ty_2Elist_2Elist@bool)))@A_27a@(ty_2Elist_2Elist@bool))@V5v)@(lam@A_27a@(^ [V6x:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V7t_27:$i] : (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))@(ap@(c_2Eoption_2ESOME@A_27a)@V6x))@V7t_27)))))))))))@(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))@(c_2Eoption_2ENONE@A_27a))@V4t))))))))))))))))).
thf(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)))))))))).
thf(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)))))))))).
thf(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)))))))))))).
thf(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)))))))))))))).
thf(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))))@(lam@bool@(^ [V3v2:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V4t:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@bool))))@V3v2)@(ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Epair_2Eprod@A_27a@(ty_2Elist_2Elist@bool))@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@bool))))@(ap@V1d@V4t))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@bool))))@(lam@(ty_2Epair_2Eprod@A_27a@(ty_2Elist_2Elist@bool))@(^ [V5v1:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@bool)))@A_27a@(ty_2Elist_2Elist@bool))@V5v1)@(lam@A_27a@(^ [V6x:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V7t_27:$i] : (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@bool))@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@bool))))@(ap@(ap@(ap@(c_2EDecode_2Edecode__list@A_27a)@(ap@(c_2Elist_2EEVERY@A_27a)@V0p))@V1d)@V7t_27))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@bool))))@(lam@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@bool))@(^ [V8v:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@bool)))@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@bool))@V8v)@(lam@(ty_2Elist_2Elist@A_27a)@(^ [V9xs:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V10t_27_27:$i] : (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))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V6x)@V9xs))@V10t_27_27)))))))))))))))))))@(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))@(c_2Elist_2ENIL@A_27a))@V4t))))))))))))))))).
thf(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))))))))))).
thf(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))))))))))).
thf(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))))))))))))).
thf(conj_thm_2EDecode_2Eencode__then__decode__blist,lemma,( ! [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))))))))))))))).
thf(conj_thm_2EDecode_2Edecode__blist,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))))) => ( ! [V2m:tp__ty_2Enum_2Enum] : ( ! [V3l:tp__c_ty_2Elist_2Elist_o] : ((p@(ap@(ap@(c_2EDecode_2Ewf__decoder@A_27a)@V0p)@V1d)) => ((ap@(ap@(ap@(ap@(c_2EDecode_2Edecode__blist@A_27a)@(ap@(ap@(c_2EEncode_2Elift__blist@A_27a)@(inj__ty_2Enum_2Enum @ V2m))@V0p))@(inj__ty_2Enum_2Enum @ V2m))@V1d)@(inj__c_ty_2Elist_2Elist_o @ V3l)) = (ap@(ap@(ap@(c_2Earithmetic_2Enum__CASE@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@bool))))@(inj__ty_2Enum_2Enum @ V2m))@(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))@(c_2Elist_2ENIL@A_27a))@(inj__c_ty_2Elist_2Elist_o @ V3l))))@(lam@ty_2Enum_2Enum@(^ [V4n:$i] : (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Epair_2Eprod@A_27a@(ty_2Elist_2Elist@bool))@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@bool))))@(ap@V1d@(inj__c_ty_2Elist_2Elist_o @ V3l)))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@bool))))@(lam@(ty_2Epair_2Eprod@A_27a@(ty_2Elist_2Elist@bool))@(^ [V5v1:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@bool)))@A_27a@(ty_2Elist_2Elist@bool))@V5v1)@(lam@A_27a@(^ [V6x:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V7t:$i] : (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@bool))@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@bool))))@(ap@(ap@(ap@(ap@(c_2EDecode_2Edecode__blist@A_27a)@(ap@(ap@(c_2EEncode_2Elift__blist@A_27a)@V4n)@V0p))@V4n)@V1d)@V7t))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@bool))))@(lam@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@bool))@(^ [V8v:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@bool)))@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@bool))@V8v)@(lam@(ty_2Elist_2Elist@A_27a)@(^ [V9xs:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V10t_27:$i] : (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))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V6x)@V9xs))@V10t_27))))))))))))))))))))))))))))))).
thf(ax_thm_2EDecode_2Edecode__num__def,axiom,( ! [V0p:$i] : ((mem@V0p@(arr@ty_2Enum_2Enum@bool)) => ((ap@c_2EDecode_2Edecode__num@V0p) = (ap@(ap@(c_2EDecode_2Eenc2dec@ty_2Enum_2Enum)@V0p)@c_2EEncode_2Eencode__num))))).
thf(conj_thm_2EDecode_2Ewf__decode__num,lemma,( ! [V0p:$i] : ((mem@V0p@(arr@ty_2Enum_2Enum@bool)) => (p@(ap@(ap@(c_2EDecode_2Ewf__decoder@ty_2Enum_2Enum)@V0p)@(ap@c_2EDecode_2Edecode__num@V0p)))))).
thf(conj_thm_2EDecode_2Edec2enc__decode__num,lemma,( ! [V0p:$i] : ((mem@V0p@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1x:tp__ty_2Enum_2Enum] : ((p@(ap@V0p@(inj__ty_2Enum_2Enum @ V1x))) => ((surj__c_ty_2Elist_2Elist_o @ (ap@(ap@(c_2EDecode_2Edec2enc@ty_2Enum_2Enum)@(ap@c_2EDecode_2Edecode__num@V0p))@(inj__ty_2Enum_2Enum @ V1x))) = (surj__c_ty_2Elist_2Elist_o @ (ap@c_2EEncode_2Eencode__num@(inj__ty_2Enum_2Enum @ V1x))))))))).
thf(conj_thm_2EDecode_2Edecode__num__total,lemma,( ! [V0l:tp__c_ty_2Elist_2Elist_o] : ((surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o @ (ap@(ap@c_2EDecode_2Edecode__num@(ap@(c_2Ecombin_2EK@bool@ty_2Enum_2Enum)@c_2Ebool_2ET))@(inj__c_ty_2Elist_2Elist_o @ V0l))) = (surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o @ (ap@(ap@(ap@(c_2Elist_2Elist__CASE@bool@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(inj__c_ty_2Elist_2Elist_o @ V0l))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(lam@bool@(^ [V1v4:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V2t_27:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@V1v4)@(ap@(ap@(ap@(c_2Elist_2Elist__CASE@bool@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@V2t_27)@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(lam@bool@(^ [V3v8:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V4t:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@V3v8)@(ap@(c_2Eoption_2ESOME@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool)))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V4t)))@(ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(ap@(ap@c_2EDecode_2Edecode__num@(ap@(c_2Ecombin_2EK@bool@ty_2Enum_2Enum)@c_2Ebool_2ET))@V4t))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(^ [V5v1:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool)))@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@V5v1)@(lam@ty_2Enum_2Enum@(^ [V6v:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V7t_27:$i] : (ap@(c_2Eoption_2ESOME@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool)))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@c_2Earithmetic_2E_2A@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@V6v))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@V7t_27)))))))))))))))))@(ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(ap@(ap@c_2EDecode_2Edecode__num@(ap@(c_2Ecombin_2EK@bool@ty_2Enum_2Enum)@c_2Ebool_2ET))@V2t_27))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(^ [V8v1:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool)))@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@V8v1)@(lam@ty_2Enum_2Enum@(^ [V9v:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V10t_27:$i] : (ap@(c_2Eoption_2ESOME@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool)))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@c_2Earithmetic_2E_2A@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@V9v))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@V10t_27)))))))))))))))))))).
thf(conj_thm_2EDecode_2Edecode__num,lemma,( ! [V0p:$i] : ((mem@V0p@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1l:tp__c_ty_2Elist_2Elist_o] : ((surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o @ (ap@(ap@c_2EDecode_2Edecode__num@V0p)@(inj__c_ty_2Elist_2Elist_o @ V1l))) = (surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o @ (ap@(ap@(ap@(c_2Elist_2Elist__CASE@bool@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(inj__c_ty_2Elist_2Elist_o @ V1l))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(lam@bool@(^ [V2v4:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V3t_27:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@V2v4)@(ap@(ap@(ap@(c_2Elist_2Elist__CASE@bool@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@V3t_27)@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(lam@bool@(^ [V4v8:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V5t:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@V4v8)@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(ap@V0p@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(c_2Eoption_2ESOME@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool)))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V5t)))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool)))))@(ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(ap@(ap@c_2EDecode_2Edecode__num@(ap@(c_2Ecombin_2EK@bool@ty_2Enum_2Enum)@c_2Ebool_2ET))@V5t))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(^ [V6v1:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool)))@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@V6v1)@(lam@ty_2Enum_2Enum@(^ [V7v:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V8t_27:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(ap@V0p@(ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@c_2Earithmetic_2E_2A@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@V7v))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(ap@(c_2Eoption_2ESOME@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool)))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@c_2Earithmetic_2E_2A@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@V7v))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@V8t_27)))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool)))))))))))))))))))@(ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(ap@(ap@c_2EDecode_2Edecode__num@(ap@(c_2Ecombin_2EK@bool@ty_2Enum_2Enum)@c_2Ebool_2ET))@V3t_27))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(^ [V9v1:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool)))@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@V9v1)@(lam@ty_2Enum_2Enum@(^ [V10v:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V11t_27:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(ap@V0p@(ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@c_2Earithmetic_2E_2A@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@V10v))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(ap@(c_2Eoption_2ESOME@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool)))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@c_2Earithmetic_2E_2A@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@V10v))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@V11t_27)))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool)))))))))))))))))))))))).
thf(ax_thm_2EDecode_2Edecode__bnum__def,axiom,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1p:$i] : ((mem@V1p@(arr@ty_2Enum_2Enum@bool)) => ((ap@(ap@c_2EDecode_2Edecode__bnum@(inj__ty_2Enum_2Enum @ V0m))@V1p) = (ap@(ap@(c_2EDecode_2Eenc2dec@ty_2Enum_2Enum)@V1p)@(ap@c_2EEncode_2Eencode__bnum@(inj__ty_2Enum_2Enum @ V0m)))))))).
thf(ax_thm_2EDecode_2Edec__bnum__def,axiom,(( ! [V0l:tp__c_ty_2Elist_2Elist_o] : ((surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o @ (ap@(ap@c_2EDecode_2Edec__bnum@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__c_ty_2Elist_2Elist_o @ V0l))) = (surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o @ (ap@(c_2Eoption_2ESOME@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool)))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__c_ty_2Elist_2Elist_o @ V0l)))))) & ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2l:tp__c_ty_2Elist_2Elist_o] : ((surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o @ (ap@(ap@c_2EDecode_2Edec__bnum@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1m)))@(inj__c_ty_2Elist_2Elist_o @ V2l))) = (surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o @ (ap@(ap@(ap@(c_2Elist_2Elist__CASE@bool@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(inj__c_ty_2Elist_2Elist_o @ V2l))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(lam@bool@(^ [V3h:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V4t:$i] : (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(ap@(ap@c_2EDecode_2Edec__bnum@(inj__ty_2Enum_2Enum @ V1m))@V4t))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(^ [V5v:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool)))@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@V5v)@(lam@ty_2Enum_2Enum@(^ [V6n:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V7t_27:$i] : (ap@(c_2Eoption_2ESOME@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool)))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@c_2Earithmetic_2E_2A@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@V6n))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@V3h)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))@V7t_27))))))))))))))))))))).
thf(conj_thm_2EDecode_2Edec__bnum__def__compute,lemma,(( ! [V0l:tp__c_ty_2Elist_2Elist_o] : ((surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o @ (ap@(ap@c_2EDecode_2Edec__bnum@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__c_ty_2Elist_2Elist_o @ V0l))) = (surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o @ (ap@(c_2Eoption_2ESOME@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool)))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__c_ty_2Elist_2Elist_o @ V0l)))))) & (( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2l:tp__c_ty_2Elist_2Elist_o] : ((surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o @ (ap@(ap@c_2EDecode_2Edec__bnum@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1m))))@(inj__c_ty_2Elist_2Elist_o @ V2l))) = (surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o @ (ap@(ap@(ap@(c_2Elist_2Elist__CASE@bool@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(inj__c_ty_2Elist_2Elist_o @ V2l))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(lam@bool@(^ [V3h:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V4t:$i] : (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(ap@(ap@c_2EDecode_2Edec__bnum@(ap@(ap@c_2Earithmetic_2E_2D@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1m))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@V4t))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(^ [V5v:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool)))@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@V5v)@(lam@ty_2Enum_2Enum@(^ [V6n:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V7t_27:$i] : (ap@(c_2Eoption_2ESOME@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool)))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@c_2Earithmetic_2E_2A@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@V6n))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@V3h)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))@V7t_27))))))))))))))))))) & ( ! [V8m:tp__ty_2Enum_2Enum] : ( ! [V9l:tp__c_ty_2Elist_2Elist_o] : ((surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o @ (ap@(ap@c_2EDecode_2Edec__bnum@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V8m))))@(inj__c_ty_2Elist_2Elist_o @ V9l))) = (surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o @ (ap@(ap@(ap@(c_2Elist_2Elist__CASE@bool@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(inj__c_ty_2Elist_2Elist_o @ V9l))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(lam@bool@(^ [V10h:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V11t:$i] : (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(ap@(ap@c_2EDecode_2Edec__bnum@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V8m))))@V11t))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(^ [V12v:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool)))@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@V12v)@(lam@ty_2Enum_2Enum@(^ [V13n:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V14t_27:$i] : (ap@(c_2Eoption_2ESOME@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool)))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@c_2Earithmetic_2E_2A@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@V13n))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@V10h)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))@V14t_27)))))))))))))))))))))).
thf(conj_thm_2EDecode_2Edec__bnum__lt,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1l:tp__c_ty_2Elist_2Elist_o] : ( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3t:tp__c_ty_2Elist_2Elist_o] : (((surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o @ (ap@(ap@c_2EDecode_2Edec__bnum@(inj__ty_2Enum_2Enum @ V0m))@(inj__c_ty_2Elist_2Elist_o @ V1l))) = (surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o @ (ap@(c_2Eoption_2ESOME@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool)))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(inj__ty_2Enum_2Enum @ V2n))@(inj__c_ty_2Elist_2Elist_o @ V3t))))) => (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V2n))@(ap@(ap@c_2Earithmetic_2EEXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V0m)))))))))).
thf(conj_thm_2EDecode_2Edec__bnum__inj,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1l:tp__c_ty_2Elist_2Elist_o] : ( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3t:tp__c_ty_2Elist_2Elist_o] : (((surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o @ (ap@(ap@c_2EDecode_2Edec__bnum@(inj__ty_2Enum_2Enum @ V0m))@(inj__c_ty_2Elist_2Elist_o @ V1l))) = (surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o @ (ap@(c_2Eoption_2ESOME@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool)))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(inj__ty_2Enum_2Enum @ V2n))@(inj__c_ty_2Elist_2Elist_o @ V3t))))) => (V1l = (surj__c_ty_2Elist_2Elist_o @ (ap@(ap@(c_2Elist_2EAPPEND@bool)@(ap@(ap@c_2EEncode_2Eencode__bnum@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V2n)))@(inj__c_ty_2Elist_2Elist_o @ V3t)))))))))).
thf(conj_thm_2EDecode_2Ewf__decode__bnum,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1p:$i] : ((mem@V1p@(arr@ty_2Enum_2Enum@bool)) => ((p@(ap@(ap@c_2EEncode_2Ewf__pred__bnum@(inj__ty_2Enum_2Enum @ V0m))@V1p)) => (p@(ap@(ap@(c_2EDecode_2Ewf__decoder@ty_2Enum_2Enum)@V1p)@(ap@(ap@c_2EDecode_2Edecode__bnum@(inj__ty_2Enum_2Enum @ V0m))@V1p)))))))).
thf(conj_thm_2EDecode_2Edec2enc__decode__bnum,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1p:$i] : ((mem@V1p@(arr@ty_2Enum_2Enum@bool)) => ( ! [V2x:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2EEncode_2Ewf__pred__bnum@(inj__ty_2Enum_2Enum @ V0m))@V1p)) & (p@(ap@V1p@(inj__ty_2Enum_2Enum @ V2x)))) => ((surj__c_ty_2Elist_2Elist_o @ (ap@(ap@(c_2EDecode_2Edec2enc@ty_2Enum_2Enum)@(ap@(ap@c_2EDecode_2Edecode__bnum@(inj__ty_2Enum_2Enum @ V0m))@V1p))@(inj__ty_2Enum_2Enum @ V2x))) = (surj__c_ty_2Elist_2Elist_o @ (ap@(ap@c_2EEncode_2Eencode__bnum@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V2x)))))))))).
thf(conj_thm_2EDecode_2Edecode__bnum,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1p:$i] : ((mem@V1p@(arr@ty_2Enum_2Enum@bool)) => ( ! [V2l:tp__c_ty_2Elist_2Elist_o] : ((p@(ap@(ap@c_2EEncode_2Ewf__pred__bnum@(inj__ty_2Enum_2Enum @ V0m))@V1p)) => ((surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o @ (ap@(ap@(ap@c_2EDecode_2Edecode__bnum@(inj__ty_2Enum_2Enum @ V0m))@V1p)@(inj__c_ty_2Elist_2Elist_o @ V2l))) = (surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Elist_2Elist_o @ (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(ap@(ap@c_2EDecode_2Edec__bnum@(inj__ty_2Enum_2Enum @ V0m))@(inj__c_ty_2Elist_2Elist_o @ V2l)))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@(^ [V3v:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool)))@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@V3v)@(lam@ty_2Enum_2Enum@(^ [V4n:$i] : (lam@(ty_2Elist_2Elist@bool)@(^ [V5t:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))))@(ap@V1p@V4n))@(ap@(c_2Eoption_2ESOME@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool)))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool))@V4n)@V5t)))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Elist_2Elist@bool)))))))))))))))))))).
thf(ax_thm_2EDecode_2Edecode__tree__def,axiom,( ! [A_27a:del]: ( ! [V0p:$i] : ((mem@V0p@(arr@(ty_2EEncode_2Etree@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__tree@A_27a)@V0p)@V1d) = (ap@(ap@(c_2EDecode_2Eenc2dec@(ty_2EEncode_2Etree@A_27a))@V0p)@(ap@(c_2EEncode_2Eencode__tree@A_27a)@(ap@(c_2EDecode_2Edec2enc@A_27a)@V1d)))))))))).
thf(conj_thm_2EDecode_2Ewf__decode__tree,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))))) => ((p@(ap@(ap@(c_2EDecode_2Ewf__decoder@A_27a)@V0p)@V1d)) => (p@(ap@(ap@(c_2EDecode_2Ewf__decoder@(ty_2EEncode_2Etree@A_27a))@(ap@(c_2EEncode_2Elift__tree@A_27a)@V0p))@(ap@(ap@(c_2EDecode_2Edecode__tree@A_27a)@(ap@(c_2EEncode_2Elift__tree@A_27a)@V0p))@V1d)))))))))).
