include('Axioms/sorting_2.ax').
tff(tp_ty_2Estring_2Echar,type,( ty_2Estring_2Echar: del )).
tff(stp_ty_2Estring_2Echar,type,(tp__ty_2Estring_2Echar : $tType)).
tff(stp_inj_ty_2Estring_2Echar,type,(inj__ty_2Estring_2Echar : tp__ty_2Estring_2Echar > $i)).
tff(stp_surj_ty_2Estring_2Echar,type,(surj__ty_2Estring_2Echar : $i > tp__ty_2Estring_2Echar)).
tff(stp_inj_surj_ty_2Estring_2Echar,axiom,( ! [X:tp__ty_2Estring_2Echar] : (surj__ty_2Estring_2Echar(inj__ty_2Estring_2Echar(X)) = X))).
tff(stp_inj_mem_ty_2Estring_2Echar,axiom,( ! [X:tp__ty_2Estring_2Echar] : (mem(inj__ty_2Estring_2Echar(X),ty_2Estring_2Echar)))).
tff(stp_iso_mem_ty_2Estring_2Echar,axiom,( ! [X:$i] : (mem(X,ty_2Estring_2Echar) => (X = inj__ty_2Estring_2Echar(surj__ty_2Estring_2Echar(X)))))).
tff(tp_c_2Estring_2ECHR,type,(c_2Estring_2ECHR:$i)).
tff(mem_c_2Estring_2ECHR,axiom,mem(c_2Estring_2ECHR,arr(ty_2Enum_2Enum,ty_2Estring_2Echar))).
tff(stp_fo_c_2Estring_2ECHR,type,(fo__c_2Estring_2ECHR:(tp__ty_2Enum_2Enum) > tp__ty_2Estring_2Echar)).
tff(stp_eq_fo_c_2Estring_2ECHR,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Estring_2Echar(fo__c_2Estring_2ECHR(X0)) = ap(c_2Estring_2ECHR,inj__ty_2Enum_2Enum(X0))))).
tff(stp_c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar,type,(tp__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar : $tType)).
tff(stp_inj_c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar,type,(inj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar : tp__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar > $i)).
tff(stp_surj_c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar,type,(surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar : $i > tp__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar)).
tff(stp_inj_surj_c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar,axiom,( ! [X:tp__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(inj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(X)) = X))).
tff(stp_inj_mem_c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar,axiom,( ! [X:tp__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (mem(inj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(X),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Estring_2Echar,ty_2Elist_2Elist(ty_2Estring_2Echar))))))).
tff(stp_iso_mem_c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar,axiom,( ! [X:$i] : (mem(X,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Estring_2Echar,ty_2Elist_2Elist(ty_2Estring_2Echar)))) => (X = inj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(X)))))).
tff(stp_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar,type,(tp__c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar : $tType)).
tff(stp_inj_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar,type,(inj__c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar : tp__c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar > $i)).
tff(stp_surj_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar,type,(surj__c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar : $i > tp__c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar)).
tff(stp_inj_surj_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(inj__c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(X)) = X))).
tff(stp_inj_mem_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (mem(inj__c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(X),ty_2Epair_2Eprod(ty_2Estring_2Echar,ty_2Elist_2Elist(ty_2Estring_2Echar)))))).
tff(stp_iso_mem_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar,axiom,( ! [X:$i] : (mem(X,ty_2Epair_2Eprod(ty_2Estring_2Echar,ty_2Elist_2Elist(ty_2Estring_2Echar))) => (X = inj__c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(surj__c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(X)))))).
tff(stp_c_ty_2Elist_2Elist_ty_2Estring_2Echar,type,(tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar : $tType)).
tff(stp_inj_c_ty_2Elist_2Elist_ty_2Estring_2Echar,type,(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar : tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar > $i)).
tff(stp_surj_c_ty_2Elist_2Elist_ty_2Estring_2Echar,type,(surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar : $i > tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar)).
tff(stp_inj_surj_c_ty_2Elist_2Elist_ty_2Estring_2Echar,axiom,( ! [X:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(X)) = X))).
tff(stp_inj_mem_c_ty_2Elist_2Elist_ty_2Estring_2Echar,axiom,( ! [X:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (mem(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(X),ty_2Elist_2Elist(ty_2Estring_2Echar))))).
tff(stp_iso_mem_c_ty_2Elist_2Elist_ty_2Estring_2Echar,axiom,( ! [X:$i] : (mem(X,ty_2Elist_2Elist(ty_2Estring_2Echar)) => (X = inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(X)))))).
tff(tp_c_2Estring_2EDEST__STRING,type,(c_2Estring_2EDEST__STRING:$i)).
tff(mem_c_2Estring_2EDEST__STRING,axiom,mem(c_2Estring_2EDEST__STRING,arr(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Estring_2Echar,ty_2Elist_2Elist(ty_2Estring_2Echar)))))).
tff(tp_c_2Estring_2EEXPLODE,type,(c_2Estring_2EEXPLODE:$i)).
tff(mem_c_2Estring_2EEXPLODE,axiom,mem(c_2Estring_2EEXPLODE,arr(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Elist_2Elist(ty_2Estring_2Echar)))).
tff(stp_c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum,type,(tp__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum : $tType)).
tff(stp_inj_c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum,type,(inj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum : tp__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum > $i)).
tff(stp_surj_c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum,type,(surj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum : $i > tp__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum)).
tff(stp_inj_surj_c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum] : (surj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(inj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(X)) = X))).
tff(stp_inj_mem_c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum] : (mem(inj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(X),ty_2Epair_2Eprod(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Eoption_2Eoption(ty_2Enum_2Enum))))))).
tff(stp_iso_mem_c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum,axiom,( ! [X:$i] : (mem(X,ty_2Epair_2Eprod(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Eoption_2Eoption(ty_2Enum_2Enum)))) => (X = inj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(surj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(X)))))).
tff(stp_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum,type,(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum : $tType)).
tff(stp_inj_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum,type,(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum : tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum > $i)).
tff(stp_surj_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum,type,(surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum : $i > tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum)).
tff(stp_inj_surj_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum] : (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(X)) = X))).
tff(stp_inj_mem_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum] : (mem(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(X),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Eoption_2Eoption(ty_2Enum_2Enum)))))).
tff(stp_iso_mem_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum,axiom,( ! [X:$i] : (mem(X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Eoption_2Eoption(ty_2Enum_2Enum))) => (X = inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(X)))))).
tff(tp_c_2Estring_2EEXTRACT,type,(c_2Estring_2EEXTRACT:$i)).
tff(mem_c_2Estring_2EEXTRACT,axiom,mem(c_2Estring_2EEXTRACT,arr(ty_2Epair_2Eprod(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Eoption_2Eoption(ty_2Enum_2Enum))),ty_2Elist_2Elist(ty_2Estring_2Echar)))).
tff(stp_c_ty_2Elist_2Elist_c_ty_2Elist_2Elist_ty_2Estring_2Echar,type,(tp__c_ty_2Elist_2Elist_c_ty_2Elist_2Elist_ty_2Estring_2Echar : $tType)).
tff(stp_inj_c_ty_2Elist_2Elist_c_ty_2Elist_2Elist_ty_2Estring_2Echar,type,(inj__c_ty_2Elist_2Elist_c_ty_2Elist_2Elist_ty_2Estring_2Echar : tp__c_ty_2Elist_2Elist_c_ty_2Elist_2Elist_ty_2Estring_2Echar > $i)).
tff(stp_surj_c_ty_2Elist_2Elist_c_ty_2Elist_2Elist_ty_2Estring_2Echar,type,(surj__c_ty_2Elist_2Elist_c_ty_2Elist_2Elist_ty_2Estring_2Echar : $i > tp__c_ty_2Elist_2Elist_c_ty_2Elist_2Elist_ty_2Estring_2Echar)).
tff(stp_inj_surj_c_ty_2Elist_2Elist_c_ty_2Elist_2Elist_ty_2Estring_2Echar,axiom,( ! [X:tp__c_ty_2Elist_2Elist_c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__c_ty_2Elist_2Elist_c_ty_2Elist_2Elist_ty_2Estring_2Echar(inj__c_ty_2Elist_2Elist_c_ty_2Elist_2Elist_ty_2Estring_2Echar(X)) = X))).
tff(stp_inj_mem_c_ty_2Elist_2Elist_c_ty_2Elist_2Elist_ty_2Estring_2Echar,axiom,( ! [X:tp__c_ty_2Elist_2Elist_c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (mem(inj__c_ty_2Elist_2Elist_c_ty_2Elist_2Elist_ty_2Estring_2Echar(X),ty_2Elist_2Elist(ty_2Elist_2Elist(ty_2Estring_2Echar)))))).
tff(stp_iso_mem_c_ty_2Elist_2Elist_c_ty_2Elist_2Elist_ty_2Estring_2Echar,axiom,( ! [X:$i] : (mem(X,ty_2Elist_2Elist(ty_2Elist_2Elist(ty_2Estring_2Echar))) => (X = inj__c_ty_2Elist_2Elist_c_ty_2Elist_2Elist_ty_2Estring_2Echar(surj__c_ty_2Elist_2Elist_c_ty_2Elist_2Elist_ty_2Estring_2Echar(X)))))).
tff(tp_c_2Estring_2EFIELDS,type,(c_2Estring_2EFIELDS:$i)).
tff(mem_c_2Estring_2EFIELDS,axiom,mem(c_2Estring_2EFIELDS,arr(arr(ty_2Estring_2Echar,bool),arr(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Elist_2Elist(ty_2Elist_2Elist(ty_2Estring_2Echar)))))).
tff(tp_c_2Estring_2EIMPLODE,type,(c_2Estring_2EIMPLODE:$i)).
tff(mem_c_2Estring_2EIMPLODE,axiom,mem(c_2Estring_2EIMPLODE,arr(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Elist_2Elist(ty_2Estring_2Echar)))).
tff(tp_c_2Estring_2EORD,type,(c_2Estring_2EORD:$i)).
tff(mem_c_2Estring_2EORD,axiom,mem(c_2Estring_2EORD,arr(ty_2Estring_2Echar,ty_2Enum_2Enum))).
tff(stp_fo_c_2Estring_2EORD,type,(fo__c_2Estring_2EORD:(tp__ty_2Estring_2Echar) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Estring_2EORD,axiom,( ! [X0:tp__ty_2Estring_2Echar] : (inj__ty_2Enum_2Enum(fo__c_2Estring_2EORD(X0)) = ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(X0))))).
tff(tp_c_2Estring_2ESTR,type,(c_2Estring_2ESTR:$i)).
tff(mem_c_2Estring_2ESTR,axiom,mem(c_2Estring_2ESTR,arr(ty_2Estring_2Echar,ty_2Elist_2Elist(ty_2Estring_2Echar)))).
tff(stp_c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_ty_2Enum_2Enum,type,(tp__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_ty_2Enum_2Enum : $tType)).
tff(stp_inj_c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_ty_2Enum_2Enum,type,(inj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_ty_2Enum_2Enum : tp__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_ty_2Enum_2Enum > $i)).
tff(stp_surj_c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_ty_2Enum_2Enum,type,(surj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_ty_2Enum_2Enum : $i > tp__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_ty_2Enum_2Enum)).
tff(stp_inj_surj_c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_ty_2Enum_2Enum] : (surj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_ty_2Enum_2Enum(inj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_ty_2Enum_2Enum(X)) = X))).
tff(stp_inj_mem_c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_ty_2Enum_2Enum] : (mem(inj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_ty_2Enum_2Enum(X),ty_2Epair_2Eprod(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Enum_2Enum))))).
tff(stp_iso_mem_c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_ty_2Enum_2Enum,axiom,( ! [X:$i] : (mem(X,ty_2Epair_2Eprod(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Enum_2Enum)) => (X = inj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_ty_2Enum_2Enum(surj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_ty_2Enum_2Enum(X)))))).
tff(tp_c_2Estring_2ESUB,type,(c_2Estring_2ESUB:$i)).
tff(mem_c_2Estring_2ESUB,axiom,mem(c_2Estring_2ESUB,arr(ty_2Epair_2Eprod(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Enum_2Enum),ty_2Estring_2Echar))).
tff(stp_fo_c_2Estring_2ESUB,type,(fo__c_2Estring_2ESUB:(tp__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_ty_2Enum_2Enum) > tp__ty_2Estring_2Echar)).
tff(stp_eq_fo_c_2Estring_2ESUB,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_ty_2Enum_2Enum] : (inj__ty_2Estring_2Echar(fo__c_2Estring_2ESUB(X0)) = ap(c_2Estring_2ESUB,inj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_ty_2Enum_2Enum(X0))))).
tff(stp_c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum,type,(tp__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum : $tType)).
tff(stp_inj_c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum,type,(inj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum : tp__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > $i)).
tff(stp_surj_c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum,type,(surj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum : $i > tp__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum)).
tff(stp_inj_surj_c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (surj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(inj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(X)) = X))).
tff(stp_inj_mem_c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (mem(inj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(X),ty_2Epair_2Eprod(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)))))).
tff(stp_iso_mem_c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum,axiom,( ! [X:$i] : (mem(X,ty_2Epair_2Eprod(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) => (X = inj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(surj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(X)))))).
tff(tp_c_2Estring_2ESUBSTRING,type,(c_2Estring_2ESUBSTRING:$i)).
tff(mem_c_2Estring_2ESUBSTRING,axiom,mem(c_2Estring_2ESUBSTRING,arr(ty_2Epair_2Eprod(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),ty_2Elist_2Elist(ty_2Estring_2Echar)))).
tff(tp_c_2Estring_2ETOCHAR,type,(c_2Estring_2ETOCHAR:$i)).
tff(mem_c_2Estring_2ETOCHAR,axiom,mem(c_2Estring_2ETOCHAR,arr(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Estring_2Echar))).
tff(stp_fo_c_2Estring_2ETOCHAR,type,(fo__c_2Estring_2ETOCHAR:(tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar) > tp__ty_2Estring_2Echar)).
tff(stp_eq_fo_c_2Estring_2ETOCHAR,axiom,( ! [X0:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (inj__ty_2Estring_2Echar(fo__c_2Estring_2ETOCHAR(X0)) = ap(c_2Estring_2ETOCHAR,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(X0))))).
tff(tp_c_2Estring_2ETOKENS,type,(c_2Estring_2ETOKENS:$i)).
tff(mem_c_2Estring_2ETOKENS,axiom,mem(c_2Estring_2ETOKENS,arr(arr(ty_2Estring_2Echar,bool),arr(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Elist_2Elist(ty_2Elist_2Elist(ty_2Estring_2Echar)))))).
tff(tp_c_2Estring_2ETRANSLATE,type,(c_2Estring_2ETRANSLATE:$i)).
tff(mem_c_2Estring_2ETRANSLATE,axiom,mem(c_2Estring_2ETRANSLATE,arr(arr(ty_2Estring_2Echar,ty_2Elist_2Elist(ty_2Estring_2Echar)),arr(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Elist_2Elist(ty_2Estring_2Echar))))).
tff(tp_c_2Estring_2Echar__ge,type,(c_2Estring_2Echar__ge:$i)).
tff(mem_c_2Estring_2Echar__ge,axiom,mem(c_2Estring_2Echar__ge,arr(ty_2Estring_2Echar,arr(ty_2Estring_2Echar,bool)))).
tff(stp_fo_c_2Estring_2Echar__ge,type,(fo__c_2Estring_2Echar__ge:(tp__ty_2Estring_2Echar * tp__ty_2Estring_2Echar) > tp__o)).
tff(stp_eq_fo_c_2Estring_2Echar__ge,axiom,( ! [X0:tp__ty_2Estring_2Echar] : ( ! [X1:tp__ty_2Estring_2Echar] : (inj__o(fo__c_2Estring_2Echar__ge(X0,X1)) = ap(ap(c_2Estring_2Echar__ge,inj__ty_2Estring_2Echar(X0)),inj__ty_2Estring_2Echar(X1)))))).
tff(tp_c_2Estring_2Echar__gt,type,(c_2Estring_2Echar__gt:$i)).
tff(mem_c_2Estring_2Echar__gt,axiom,mem(c_2Estring_2Echar__gt,arr(ty_2Estring_2Echar,arr(ty_2Estring_2Echar,bool)))).
tff(stp_fo_c_2Estring_2Echar__gt,type,(fo__c_2Estring_2Echar__gt:(tp__ty_2Estring_2Echar * tp__ty_2Estring_2Echar) > tp__o)).
tff(stp_eq_fo_c_2Estring_2Echar__gt,axiom,( ! [X0:tp__ty_2Estring_2Echar] : ( ! [X1:tp__ty_2Estring_2Echar] : (inj__o(fo__c_2Estring_2Echar__gt(X0,X1)) = ap(ap(c_2Estring_2Echar__gt,inj__ty_2Estring_2Echar(X0)),inj__ty_2Estring_2Echar(X1)))))).
tff(tp_c_2Estring_2Echar__le,type,(c_2Estring_2Echar__le:$i)).
tff(mem_c_2Estring_2Echar__le,axiom,mem(c_2Estring_2Echar__le,arr(ty_2Estring_2Echar,arr(ty_2Estring_2Echar,bool)))).
tff(stp_fo_c_2Estring_2Echar__le,type,(fo__c_2Estring_2Echar__le:(tp__ty_2Estring_2Echar * tp__ty_2Estring_2Echar) > tp__o)).
tff(stp_eq_fo_c_2Estring_2Echar__le,axiom,( ! [X0:tp__ty_2Estring_2Echar] : ( ! [X1:tp__ty_2Estring_2Echar] : (inj__o(fo__c_2Estring_2Echar__le(X0,X1)) = ap(ap(c_2Estring_2Echar__le,inj__ty_2Estring_2Echar(X0)),inj__ty_2Estring_2Echar(X1)))))).
tff(tp_c_2Estring_2Echar__lt,type,(c_2Estring_2Echar__lt:$i)).
tff(mem_c_2Estring_2Echar__lt,axiom,mem(c_2Estring_2Echar__lt,arr(ty_2Estring_2Echar,arr(ty_2Estring_2Echar,bool)))).
tff(stp_fo_c_2Estring_2Echar__lt,type,(fo__c_2Estring_2Echar__lt:(tp__ty_2Estring_2Echar * tp__ty_2Estring_2Echar) > tp__o)).
tff(stp_eq_fo_c_2Estring_2Echar__lt,axiom,( ! [X0:tp__ty_2Estring_2Echar] : ( ! [X1:tp__ty_2Estring_2Echar] : (inj__o(fo__c_2Estring_2Echar__lt(X0,X1)) = ap(ap(c_2Estring_2Echar__lt,inj__ty_2Estring_2Echar(X0)),inj__ty_2Estring_2Echar(X1)))))).
tff(tp_c_2Estring_2Echar__size,type,(c_2Estring_2Echar__size:$i)).
tff(mem_c_2Estring_2Echar__size,axiom,mem(c_2Estring_2Echar__size,arr(ty_2Estring_2Echar,ty_2Enum_2Enum))).
tff(stp_fo_c_2Estring_2Echar__size,type,(fo__c_2Estring_2Echar__size:(tp__ty_2Estring_2Echar) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Estring_2Echar__size,axiom,( ! [X0:tp__ty_2Estring_2Echar] : (inj__ty_2Enum_2Enum(fo__c_2Estring_2Echar__size(X0)) = ap(c_2Estring_2Echar__size,inj__ty_2Estring_2Echar(X0))))).
tff(tp_c_2Estring_2EisAlpha,type,(c_2Estring_2EisAlpha:$i)).
tff(mem_c_2Estring_2EisAlpha,axiom,mem(c_2Estring_2EisAlpha,arr(ty_2Estring_2Echar,bool))).
tff(stp_fo_c_2Estring_2EisAlpha,type,(fo__c_2Estring_2EisAlpha:(tp__ty_2Estring_2Echar) > tp__o)).
tff(stp_eq_fo_c_2Estring_2EisAlpha,axiom,( ! [X0:tp__ty_2Estring_2Echar] : (inj__o(fo__c_2Estring_2EisAlpha(X0)) = ap(c_2Estring_2EisAlpha,inj__ty_2Estring_2Echar(X0))))).
tff(tp_c_2Estring_2EisAlphaNum,type,(c_2Estring_2EisAlphaNum:$i)).
tff(mem_c_2Estring_2EisAlphaNum,axiom,mem(c_2Estring_2EisAlphaNum,arr(ty_2Estring_2Echar,bool))).
tff(stp_fo_c_2Estring_2EisAlphaNum,type,(fo__c_2Estring_2EisAlphaNum:(tp__ty_2Estring_2Echar) > tp__o)).
tff(stp_eq_fo_c_2Estring_2EisAlphaNum,axiom,( ! [X0:tp__ty_2Estring_2Echar] : (inj__o(fo__c_2Estring_2EisAlphaNum(X0)) = ap(c_2Estring_2EisAlphaNum,inj__ty_2Estring_2Echar(X0))))).
tff(tp_c_2Estring_2EisAscii,type,(c_2Estring_2EisAscii:$i)).
tff(mem_c_2Estring_2EisAscii,axiom,mem(c_2Estring_2EisAscii,arr(ty_2Estring_2Echar,bool))).
tff(stp_fo_c_2Estring_2EisAscii,type,(fo__c_2Estring_2EisAscii:(tp__ty_2Estring_2Echar) > tp__o)).
tff(stp_eq_fo_c_2Estring_2EisAscii,axiom,( ! [X0:tp__ty_2Estring_2Echar] : (inj__o(fo__c_2Estring_2EisAscii(X0)) = ap(c_2Estring_2EisAscii,inj__ty_2Estring_2Echar(X0))))).
tff(tp_c_2Estring_2EisCntrl,type,(c_2Estring_2EisCntrl:$i)).
tff(mem_c_2Estring_2EisCntrl,axiom,mem(c_2Estring_2EisCntrl,arr(ty_2Estring_2Echar,bool))).
tff(stp_fo_c_2Estring_2EisCntrl,type,(fo__c_2Estring_2EisCntrl:(tp__ty_2Estring_2Echar) > tp__o)).
tff(stp_eq_fo_c_2Estring_2EisCntrl,axiom,( ! [X0:tp__ty_2Estring_2Echar] : (inj__o(fo__c_2Estring_2EisCntrl(X0)) = ap(c_2Estring_2EisCntrl,inj__ty_2Estring_2Echar(X0))))).
tff(tp_c_2Estring_2EisDigit,type,(c_2Estring_2EisDigit:$i)).
tff(mem_c_2Estring_2EisDigit,axiom,mem(c_2Estring_2EisDigit,arr(ty_2Estring_2Echar,bool))).
tff(stp_fo_c_2Estring_2EisDigit,type,(fo__c_2Estring_2EisDigit:(tp__ty_2Estring_2Echar) > tp__o)).
tff(stp_eq_fo_c_2Estring_2EisDigit,axiom,( ! [X0:tp__ty_2Estring_2Echar] : (inj__o(fo__c_2Estring_2EisDigit(X0)) = ap(c_2Estring_2EisDigit,inj__ty_2Estring_2Echar(X0))))).
tff(tp_c_2Estring_2EisGraph,type,(c_2Estring_2EisGraph:$i)).
tff(mem_c_2Estring_2EisGraph,axiom,mem(c_2Estring_2EisGraph,arr(ty_2Estring_2Echar,bool))).
tff(stp_fo_c_2Estring_2EisGraph,type,(fo__c_2Estring_2EisGraph:(tp__ty_2Estring_2Echar) > tp__o)).
tff(stp_eq_fo_c_2Estring_2EisGraph,axiom,( ! [X0:tp__ty_2Estring_2Echar] : (inj__o(fo__c_2Estring_2EisGraph(X0)) = ap(c_2Estring_2EisGraph,inj__ty_2Estring_2Echar(X0))))).
tff(tp_c_2Estring_2EisHexDigit,type,(c_2Estring_2EisHexDigit:$i)).
tff(mem_c_2Estring_2EisHexDigit,axiom,mem(c_2Estring_2EisHexDigit,arr(ty_2Estring_2Echar,bool))).
tff(stp_fo_c_2Estring_2EisHexDigit,type,(fo__c_2Estring_2EisHexDigit:(tp__ty_2Estring_2Echar) > tp__o)).
tff(stp_eq_fo_c_2Estring_2EisHexDigit,axiom,( ! [X0:tp__ty_2Estring_2Echar] : (inj__o(fo__c_2Estring_2EisHexDigit(X0)) = ap(c_2Estring_2EisHexDigit,inj__ty_2Estring_2Echar(X0))))).
tff(tp_c_2Estring_2EisLower,type,(c_2Estring_2EisLower:$i)).
tff(mem_c_2Estring_2EisLower,axiom,mem(c_2Estring_2EisLower,arr(ty_2Estring_2Echar,bool))).
tff(stp_fo_c_2Estring_2EisLower,type,(fo__c_2Estring_2EisLower:(tp__ty_2Estring_2Echar) > tp__o)).
tff(stp_eq_fo_c_2Estring_2EisLower,axiom,( ! [X0:tp__ty_2Estring_2Echar] : (inj__o(fo__c_2Estring_2EisLower(X0)) = ap(c_2Estring_2EisLower,inj__ty_2Estring_2Echar(X0))))).
tff(tp_c_2Estring_2EisPrint,type,(c_2Estring_2EisPrint:$i)).
tff(mem_c_2Estring_2EisPrint,axiom,mem(c_2Estring_2EisPrint,arr(ty_2Estring_2Echar,bool))).
tff(stp_fo_c_2Estring_2EisPrint,type,(fo__c_2Estring_2EisPrint:(tp__ty_2Estring_2Echar) > tp__o)).
tff(stp_eq_fo_c_2Estring_2EisPrint,axiom,( ! [X0:tp__ty_2Estring_2Echar] : (inj__o(fo__c_2Estring_2EisPrint(X0)) = ap(c_2Estring_2EisPrint,inj__ty_2Estring_2Echar(X0))))).
tff(tp_c_2Estring_2EisPunct,type,(c_2Estring_2EisPunct:$i)).
tff(mem_c_2Estring_2EisPunct,axiom,mem(c_2Estring_2EisPunct,arr(ty_2Estring_2Echar,bool))).
tff(stp_fo_c_2Estring_2EisPunct,type,(fo__c_2Estring_2EisPunct:(tp__ty_2Estring_2Echar) > tp__o)).
tff(stp_eq_fo_c_2Estring_2EisPunct,axiom,( ! [X0:tp__ty_2Estring_2Echar] : (inj__o(fo__c_2Estring_2EisPunct(X0)) = ap(c_2Estring_2EisPunct,inj__ty_2Estring_2Echar(X0))))).
tff(tp_c_2Estring_2EisSpace,type,(c_2Estring_2EisSpace:$i)).
tff(mem_c_2Estring_2EisSpace,axiom,mem(c_2Estring_2EisSpace,arr(ty_2Estring_2Echar,bool))).
tff(stp_fo_c_2Estring_2EisSpace,type,(fo__c_2Estring_2EisSpace:(tp__ty_2Estring_2Echar) > tp__o)).
tff(stp_eq_fo_c_2Estring_2EisSpace,axiom,( ! [X0:tp__ty_2Estring_2Echar] : (inj__o(fo__c_2Estring_2EisSpace(X0)) = ap(c_2Estring_2EisSpace,inj__ty_2Estring_2Echar(X0))))).
tff(tp_c_2Estring_2EisUpper,type,(c_2Estring_2EisUpper:$i)).
tff(mem_c_2Estring_2EisUpper,axiom,mem(c_2Estring_2EisUpper,arr(ty_2Estring_2Echar,bool))).
tff(stp_fo_c_2Estring_2EisUpper,type,(fo__c_2Estring_2EisUpper:(tp__ty_2Estring_2Echar) > tp__o)).
tff(stp_eq_fo_c_2Estring_2EisUpper,axiom,( ! [X0:tp__ty_2Estring_2Echar] : (inj__o(fo__c_2Estring_2EisUpper(X0)) = ap(c_2Estring_2EisUpper,inj__ty_2Estring_2Echar(X0))))).
tff(tp_c_2Estring_2Estring__ge,type,(c_2Estring_2Estring__ge:$i)).
tff(mem_c_2Estring_2Estring__ge,axiom,mem(c_2Estring_2Estring__ge,arr(ty_2Elist_2Elist(ty_2Estring_2Echar),arr(ty_2Elist_2Elist(ty_2Estring_2Echar),bool)))).
tff(stp_fo_c_2Estring_2Estring__ge,type,(fo__c_2Estring_2Estring__ge:(tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar * tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar) > tp__o)).
tff(stp_eq_fo_c_2Estring_2Estring__ge,axiom,( ! [X0:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [X1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (inj__o(fo__c_2Estring_2Estring__ge(X0,X1)) = ap(ap(c_2Estring_2Estring__ge,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(X0)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(X1)))))).
tff(tp_c_2Estring_2Estring__gt,type,(c_2Estring_2Estring__gt:$i)).
tff(mem_c_2Estring_2Estring__gt,axiom,mem(c_2Estring_2Estring__gt,arr(ty_2Elist_2Elist(ty_2Estring_2Echar),arr(ty_2Elist_2Elist(ty_2Estring_2Echar),bool)))).
tff(stp_fo_c_2Estring_2Estring__gt,type,(fo__c_2Estring_2Estring__gt:(tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar * tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar) > tp__o)).
tff(stp_eq_fo_c_2Estring_2Estring__gt,axiom,( ! [X0:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [X1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (inj__o(fo__c_2Estring_2Estring__gt(X0,X1)) = ap(ap(c_2Estring_2Estring__gt,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(X0)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(X1)))))).
tff(tp_c_2Estring_2Estring__le,type,(c_2Estring_2Estring__le:$i)).
tff(mem_c_2Estring_2Estring__le,axiom,mem(c_2Estring_2Estring__le,arr(ty_2Elist_2Elist(ty_2Estring_2Echar),arr(ty_2Elist_2Elist(ty_2Estring_2Echar),bool)))).
tff(stp_fo_c_2Estring_2Estring__le,type,(fo__c_2Estring_2Estring__le:(tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar * tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar) > tp__o)).
tff(stp_eq_fo_c_2Estring_2Estring__le,axiom,( ! [X0:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [X1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (inj__o(fo__c_2Estring_2Estring__le(X0,X1)) = ap(ap(c_2Estring_2Estring__le,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(X0)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(X1)))))).
tff(tp_c_2Estring_2Estring__lt,type,(c_2Estring_2Estring__lt:$i)).
tff(mem_c_2Estring_2Estring__lt,axiom,mem(c_2Estring_2Estring__lt,arr(ty_2Elist_2Elist(ty_2Estring_2Echar),arr(ty_2Elist_2Elist(ty_2Estring_2Echar),bool)))).
tff(stp_fo_c_2Estring_2Estring__lt,type,(fo__c_2Estring_2Estring__lt:(tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar * tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar) > tp__o)).
tff(stp_eq_fo_c_2Estring_2Estring__lt,axiom,( ! [X0:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [X1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (inj__o(fo__c_2Estring_2Estring__lt(X0,X1)) = ap(ap(c_2Estring_2Estring__lt,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(X0)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(X1)))))).
tff(tp_c_2Estring_2EtoLower,type,(c_2Estring_2EtoLower:$i)).
tff(mem_c_2Estring_2EtoLower,axiom,mem(c_2Estring_2EtoLower,arr(ty_2Estring_2Echar,ty_2Estring_2Echar))).
tff(stp_fo_c_2Estring_2EtoLower,type,(fo__c_2Estring_2EtoLower:(tp__ty_2Estring_2Echar) > tp__ty_2Estring_2Echar)).
tff(stp_eq_fo_c_2Estring_2EtoLower,axiom,( ! [X0:tp__ty_2Estring_2Echar] : (inj__ty_2Estring_2Echar(fo__c_2Estring_2EtoLower(X0)) = ap(c_2Estring_2EtoLower,inj__ty_2Estring_2Echar(X0))))).
tff(tp_c_2Estring_2EtoUpper,type,(c_2Estring_2EtoUpper:$i)).
tff(mem_c_2Estring_2EtoUpper,axiom,mem(c_2Estring_2EtoUpper,arr(ty_2Estring_2Echar,ty_2Estring_2Echar))).
tff(stp_fo_c_2Estring_2EtoUpper,type,(fo__c_2Estring_2EtoUpper:(tp__ty_2Estring_2Echar) > tp__ty_2Estring_2Echar)).
tff(stp_eq_fo_c_2Estring_2EtoUpper,axiom,( ! [X0:tp__ty_2Estring_2Echar] : (inj__ty_2Estring_2Echar(fo__c_2Estring_2EtoUpper(X0)) = ap(c_2Estring_2EtoUpper,inj__ty_2Estring_2Echar(X0))))).
tff(ax_thm_2Estring_2Echar__TY__DEF,axiom,(? [V0rep:$i] : (mem(V0rep,arr(ty_2Estring_2Echar,ty_2Enum_2Enum)) & p(ap(ap(c_2Ebool_2ETYPE__DEFINITION(ty_2Enum_2Enum,ty_2Estring_2Echar),f1123),V0rep))))).
tff(ax_thm_2Estring_2Echar__BIJ,axiom,(( ! [V0a:tp__ty_2Estring_2Echar] : (surj__ty_2Estring_2Echar(ap(c_2Estring_2ECHR,ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0a)))) = V0a)) & ( ! [V1r:tp__ty_2Enum_2Enum] : (p(ap(f1124,inj__ty_2Enum_2Enum(V1r))) <=> (surj__ty_2Enum_2Enum(ap(c_2Estring_2EORD,ap(c_2Estring_2ECHR,inj__ty_2Enum_2Enum(V1r)))) = V1r))))).
tff(conj_thm_2Estring_2EORD__11,lemma,(( ! [V0a:tp__ty_2Estring_2Echar] : ( ! [V1a_27:tp__ty_2Estring_2Echar] : ((surj__ty_2Enum_2Enum(ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0a))) = surj__ty_2Enum_2Enum(ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V1a_27)))) <=> (V0a = V1a_27)))))).
tff(conj_thm_2Estring_2ECHR__11,lemma,(( ! [V0r:tp__ty_2Enum_2Enum] : ( ! [V1r_27:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0r)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))) => (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1r_27)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))) => ((surj__ty_2Estring_2Echar(ap(c_2Estring_2ECHR,inj__ty_2Enum_2Enum(V0r))) = surj__ty_2Estring_2Echar(ap(c_2Estring_2ECHR,inj__ty_2Enum_2Enum(V1r_27)))) <=> (V0r = V1r_27)))))))).
tff(conj_thm_2Estring_2EORD__ONTO,lemma,(( ! [V0r:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0r)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))) <=> (? [V1a:tp__ty_2Estring_2Echar] : (V0r = surj__ty_2Enum_2Enum(ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V1a))))))))).
tff(conj_thm_2Estring_2ECHR__ONTO,lemma,(( ! [V0a:tp__ty_2Estring_2Echar] : (? [V1r:tp__ty_2Enum_2Enum] : ((V0a = surj__ty_2Estring_2Echar(ap(c_2Estring_2ECHR,inj__ty_2Enum_2Enum(V1r)))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1r)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))))))))).
tff(conj_thm_2Estring_2ECHR__ORD,lemma,(( ! [V0a:tp__ty_2Estring_2Echar] : (surj__ty_2Estring_2Echar(ap(c_2Estring_2ECHR,ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0a)))) = V0a)))).
tff(conj_thm_2Estring_2EORD__CHR,lemma,(( ! [V0r:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0r)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))) <=> (surj__ty_2Enum_2Enum(ap(c_2Estring_2EORD,ap(c_2Estring_2ECHR,inj__ty_2Enum_2Enum(V0r)))) = V0r))))).
tff(conj_thm_2Estring_2EORD__CHR__RWT,lemma,(( ! [V0r:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0r)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))) => (surj__ty_2Enum_2Enum(ap(c_2Estring_2EORD,ap(c_2Estring_2ECHR,inj__ty_2Enum_2Enum(V0r)))) = V0r))))).
tff(conj_thm_2Estring_2EORD__CHR__COMPUTE,lemma,(( ! [V0_3E_20255:tp__o] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Estring_2EORD,ap(c_2Estring_2ECHR,inj__ty_2Enum_2Enum(V1n)))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))),inj__ty_2Enum_2Enum(V1n)),ap(ap(ap(c_2Ecombin_2EFAIL(arr(ty_2Estring_2Echar,ty_2Enum_2Enum),bool),c_2Estring_2EORD),inj__o(V0_3E_20255)),ap(c_2Estring_2ECHR,inj__ty_2Enum_2Enum(V1n)))))))))).
tff(conj_thm_2Estring_2EORD__BOUND,lemma,(( ! [V0c:tp__ty_2Estring_2Echar] : p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0c))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))))))).
tff(conj_thm_2Estring_2Echar__nchotomy,lemma,(( ! [V0c:tp__ty_2Estring_2Echar] : (? [V1n:tp__ty_2Enum_2Enum] : (V0c = surj__ty_2Estring_2Echar(ap(c_2Estring_2ECHR,inj__ty_2Enum_2Enum(V1n)))))))).
tff(conj_thm_2Estring_2Eranged__char__nchotomy,lemma,(( ! [V0c:tp__ty_2Estring_2Echar] : (? [V1n:tp__ty_2Enum_2Enum] : ((V0c = surj__ty_2Estring_2Echar(ap(c_2Estring_2ECHR,inj__ty_2Enum_2Enum(V1n)))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))))))))).
tff(ax_thm_2Estring_2EisLower__def,axiom,( ! [V0c:tp__ty_2Estring_2Echar] : (p(ap(c_2Estring_2EisLower,inj__ty_2Estring_2Echar(V0c))) <=> (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))),ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0c)))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0c))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))))).
tff(ax_thm_2Estring_2EisUpper__def,axiom,( ! [V0c:tp__ty_2Estring_2Echar] : (p(ap(c_2Estring_2EisUpper,inj__ty_2Estring_2Echar(V0c))) <=> (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))),ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0c)))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0c))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))))).
tff(ax_thm_2Estring_2EisDigit__def,axiom,( ! [V0c:tp__ty_2Estring_2Echar] : (p(ap(c_2Estring_2EisDigit,inj__ty_2Estring_2Echar(V0c))) <=> (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))),ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0c)))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0c))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))))).
tff(ax_thm_2Estring_2EisAlpha__def,axiom,( ! [V0c:tp__ty_2Estring_2Echar] : (p(ap(c_2Estring_2EisAlpha,inj__ty_2Estring_2Echar(V0c))) <=> (p(ap(c_2Estring_2EisLower,inj__ty_2Estring_2Echar(V0c))) | p(ap(c_2Estring_2EisUpper,inj__ty_2Estring_2Echar(V0c))))))).
tff(ax_thm_2Estring_2EisHexDigit__def,axiom,( ! [V0c:tp__ty_2Estring_2Echar] : (p(ap(c_2Estring_2EisHexDigit,inj__ty_2Estring_2Echar(V0c))) <=> ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))),ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0c)))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0c))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))) | ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))),ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0c)))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0c))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))) | (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))),ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0c)))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0c))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))))))).
tff(ax_thm_2Estring_2EisAlphaNum__def,axiom,( ! [V0c:tp__ty_2Estring_2Echar] : (p(ap(c_2Estring_2EisAlphaNum,inj__ty_2Estring_2Echar(V0c))) <=> (p(ap(c_2Estring_2EisAlpha,inj__ty_2Estring_2Echar(V0c))) | p(ap(c_2Estring_2EisDigit,inj__ty_2Estring_2Echar(V0c))))))).
tff(ax_thm_2Estring_2EisPrint__def,axiom,( ! [V0c:tp__ty_2Estring_2Echar] : (p(ap(c_2Estring_2EisPrint,inj__ty_2Estring_2Echar(V0c))) <=> (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))),ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0c)))) & p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0c))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))))))).
tff(ax_thm_2Estring_2EisSpace__def,axiom,( ! [V0c:tp__ty_2Estring_2Echar] : (p(ap(c_2Estring_2EisSpace,inj__ty_2Estring_2Echar(V0c))) <=> ((surj__ty_2Enum_2Enum(ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0c))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))) | (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0c)))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0c))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))).
tff(ax_thm_2Estring_2EisGraph__def,axiom,( ! [V0c:tp__ty_2Estring_2Echar] : (p(ap(c_2Estring_2EisGraph,inj__ty_2Estring_2Echar(V0c))) <=> (p(ap(c_2Estring_2EisPrint,inj__ty_2Estring_2Echar(V0c))) & (~~ p(ap(c_2Estring_2EisSpace,inj__ty_2Estring_2Echar(V0c)))))))).
tff(ax_thm_2Estring_2EisPunct__def,axiom,( ! [V0c:tp__ty_2Estring_2Echar] : (p(ap(c_2Estring_2EisPunct,inj__ty_2Estring_2Echar(V0c))) <=> (p(ap(c_2Estring_2EisGraph,inj__ty_2Estring_2Echar(V0c))) & (~~ p(ap(c_2Estring_2EisAlphaNum,inj__ty_2Estring_2Echar(V0c)))))))).
tff(ax_thm_2Estring_2EisAscii__def,axiom,( ! [V0c:tp__ty_2Estring_2Echar] : (p(ap(c_2Estring_2EisAscii,inj__ty_2Estring_2Echar(V0c))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0c))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))))).
tff(ax_thm_2Estring_2EisCntrl__def,axiom,( ! [V0c:tp__ty_2Estring_2Echar] : (p(ap(c_2Estring_2EisCntrl,inj__ty_2Estring_2Echar(V0c))) <=> (p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0c))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))) | p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))),ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0c)))))))).
tff(ax_thm_2Estring_2EtoLower__def,axiom,( ! [V0c:tp__ty_2Estring_2Echar] : (surj__ty_2Estring_2Echar(ap(c_2Estring_2EtoLower,inj__ty_2Estring_2Echar(V0c))) = surj__ty_2Estring_2Echar(ap(ap(ap(c_2Ebool_2ECOND(ty_2Estring_2Echar),ap(c_2Estring_2EisUpper,inj__ty_2Estring_2Echar(V0c))),ap(c_2Estring_2ECHR,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0c))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))),inj__ty_2Estring_2Echar(V0c)))))).
tff(ax_thm_2Estring_2EtoUpper__def,axiom,( ! [V0c:tp__ty_2Estring_2Echar] : (surj__ty_2Estring_2Echar(ap(c_2Estring_2EtoUpper,inj__ty_2Estring_2Echar(V0c))) = surj__ty_2Estring_2Echar(ap(ap(ap(c_2Ebool_2ECOND(ty_2Estring_2Echar),ap(c_2Estring_2EisLower,inj__ty_2Estring_2Echar(V0c))),ap(c_2Estring_2ECHR,ap(ap(c_2Earithmetic_2E_2D,ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0c))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))),inj__ty_2Estring_2Echar(V0c)))))).
tff(ax_thm_2Estring_2Echar__lt__def,axiom,( ! [V0a:tp__ty_2Estring_2Echar] : ( ! [V1b:tp__ty_2Estring_2Echar] : (p(ap(ap(c_2Estring_2Echar__lt,inj__ty_2Estring_2Echar(V0a)),inj__ty_2Estring_2Echar(V1b))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0a))),ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V1b)))))))).
tff(ax_thm_2Estring_2Echar__le__def,axiom,( ! [V0a:tp__ty_2Estring_2Echar] : ( ! [V1b:tp__ty_2Estring_2Echar] : (p(ap(ap(c_2Estring_2Echar__le,inj__ty_2Estring_2Echar(V0a)),inj__ty_2Estring_2Echar(V1b))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0a))),ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V1b)))))))).
tff(ax_thm_2Estring_2Echar__gt__def,axiom,( ! [V0a:tp__ty_2Estring_2Echar] : ( ! [V1b:tp__ty_2Estring_2Echar] : (p(ap(ap(c_2Estring_2Echar__gt,inj__ty_2Estring_2Echar(V0a)),inj__ty_2Estring_2Echar(V1b))) <=> p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0a))),ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V1b)))))))).
tff(ax_thm_2Estring_2Echar__ge__def,axiom,( ! [V0a:tp__ty_2Estring_2Echar] : ( ! [V1b:tp__ty_2Estring_2Echar] : (p(ap(ap(c_2Estring_2Echar__ge,inj__ty_2Estring_2Echar(V0a)),inj__ty_2Estring_2Echar(V1b))) <=> p(ap(ap(c_2Earithmetic_2E_3E_3D,ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0a))),ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V1b)))))))).
tff(conj_thm_2Estring_2ECHAR__EQ__THM,lemma,(( ! [V0c1:tp__ty_2Estring_2Echar] : ( ! [V1c2:tp__ty_2Estring_2Echar] : ((V0c1 = V1c2) <=> (surj__ty_2Enum_2Enum(ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0c1))) = surj__ty_2Enum_2Enum(ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V1c2))))))))).
tff(conj_thm_2Estring_2ECHAR__INDUCT__THM,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2Estring_2Echar,bool)) => (( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))) => p(ap(V0P,ap(c_2Estring_2ECHR,inj__ty_2Enum_2Enum(V1n)))))) => ( ! [V2c:tp__ty_2Estring_2Echar] : p(ap(V0P,inj__ty_2Estring_2Echar(V2c))))))))).
tff(ax_thm_2Estring_2Echar__size__def,axiom,( ! [V0c:tp__ty_2Estring_2Echar] : (surj__ty_2Enum_2Enum(ap(c_2Estring_2Echar__size,inj__ty_2Estring_2Echar(V0c))) = fo__c_2Enum_2E0))).
tff(ax_thm_2Estring_2ESUB__def,axiom,( ! [V0s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Estring_2Echar(ap(c_2Estring_2ESUB,ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Enum_2Enum),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s)),inj__ty_2Enum_2Enum(V1n)))) = surj__ty_2Estring_2Echar(ap(ap(c_2Elist_2EEL(ty_2Estring_2Echar),inj__ty_2Enum_2Enum(V1n)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s))))))).
tff(ax_thm_2Estring_2ESTR__def,axiom,( ! [V0c:tp__ty_2Estring_2Echar] : (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2ESTR,inj__ty_2Estring_2Echar(V0c))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V0c)),c_2Elist_2ENIL(ty_2Estring_2Echar)))))).
tff(ax_thm_2Estring_2ETOCHAR__primitive__def,axiom,(c_2Estring_2ETOCHAR = ap(ap(c_2Erelation_2EWFREC(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Estring_2Echar),ap(c_2Emin_2E_40(arr(ty_2Elist_2Elist(ty_2Estring_2Echar),arr(ty_2Elist_2Elist(ty_2Estring_2Echar),bool))),f1125)),k(arr(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Estring_2Echar),f1128)))).
tff(conj_thm_2Estring_2ETOCHAR__ind,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2Elist_2Elist(ty_2Estring_2Echar),bool)) => ((( ! [V1c:tp__ty_2Estring_2Echar] : p(ap(V0P,ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V1c)),c_2Elist_2ENIL(ty_2Estring_2Echar))))) & (p(ap(V0P,c_2Elist_2ENIL(ty_2Estring_2Echar))) & ( ! [V2v6:tp__ty_2Estring_2Echar] : ( ! [V3v4:tp__ty_2Estring_2Echar] : ( ! [V4v5:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : p(ap(V0P,ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V2v6)),ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V3v4)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V4v5)))))))))) => ( ! [V5v:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : p(ap(V0P,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V5v))))))))).
tff(conj_thm_2Estring_2ETOCHAR__def,lemma,(( ! [V0c:tp__ty_2Estring_2Echar] : (surj__ty_2Estring_2Echar(ap(c_2Estring_2ETOCHAR,ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V0c)),c_2Elist_2ENIL(ty_2Estring_2Echar)))) = V0c)))).
tff(ax_thm_2Estring_2ESUBSTRING__def,axiom,( ! [V0s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V1i:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2ESUBSTRING,ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1i)),inj__ty_2Enum_2Enum(V2n))))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(ap(c_2Erich__list_2ESEG(ty_2Estring_2Echar),inj__ty_2Enum_2Enum(V2n)),inj__ty_2Enum_2Enum(V1i)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s)))))))).
tff(ax_thm_2Estring_2ETRANSLATE__def,axiom,( ! [V0f:$i] : (mem(V0f,arr(ty_2Estring_2Echar,ty_2Elist_2Elist(ty_2Estring_2Echar))) => ( ! [V1s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Estring_2ETRANSLATE,V0f),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Elist_2EFLAT(ty_2Estring_2Echar),ap(ap(c_2Elist_2EMAP(ty_2Estring_2Echar,ty_2Elist_2Elist(ty_2Estring_2Echar)),V0f),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s))))))))).
tff(stp_c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar,type,(tp__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar : $tType)).
tff(stp_inj_c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar,type,(inj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar : tp__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar > $i)).
tff(stp_surj_c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar,type,(surj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar : $i > tp__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar)).
tff(stp_inj_surj_c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(inj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(X)) = X))).
tff(stp_inj_mem_c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (mem(inj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(X),ty_2Epair_2Eprod(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Elist_2Elist(ty_2Estring_2Echar)))))).
tff(stp_iso_mem_c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar,axiom,( ! [X:$i] : (mem(X,ty_2Epair_2Eprod(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Elist_2Elist(ty_2Estring_2Echar))) => (X = inj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(surj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(X)))))).
tff(conj_thm_2Estring_2ETOKENS__ind,lemma,(( ! [V0P_27:$i] : (mem(V0P_27,arr(arr(ty_2Estring_2Echar,bool),arr(ty_2Elist_2Elist(ty_2Estring_2Echar),bool))) => ((( ! [V1P:$i] : (mem(V1P,arr(ty_2Estring_2Echar,bool)) => p(ap(ap(V0P_27,V1P),c_2Elist_2ENIL(ty_2Estring_2Echar))))) & ( ! [V2P:$i] : (mem(V2P,arr(ty_2Estring_2Echar,bool)) => ( ! [V3h:tp__ty_2Estring_2Echar] : ( ! [V4t:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ((( ! [V5l:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V6r:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (((surj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Elist_2Elist(ty_2Estring_2Echar)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V5l)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V6r))) = surj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Erich__list_2ESPLITP(ty_2Estring_2Echar),V2P),ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V3h)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V4t))))) & p(ap(c_2Elist_2ENULL(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V5l)))) => p(ap(ap(V0P_27,V2P),ap(c_2Elist_2ETL(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V6r))))))) & ( ! [V7l:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V8r:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (((surj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Elist_2Elist(ty_2Estring_2Echar)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V7l)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V8r))) = surj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Erich__list_2ESPLITP(ty_2Estring_2Echar),V2P),ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V3h)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V4t))))) & (~~ p(ap(c_2Elist_2ENULL(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V7l))))) => p(ap(ap(V0P_27,V2P),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V8r))))))) => p(ap(ap(V0P_27,V2P),ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V3h)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V4t)))))))))) => ( ! [V9v:$i] : (mem(V9v,arr(ty_2Estring_2Echar,bool)) => ( ! [V10v1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : p(ap(ap(V0P_27,V9v),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V10v1))))))))))).
tff(conj_thm_2Estring_2ETOKENS__def,lemma,((( ! [V0P:$i] : (mem(V0P,arr(ty_2Estring_2Echar,bool)) => (surj__c_ty_2Elist_2Elist_c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Estring_2ETOKENS,V0P),c_2Elist_2ENIL(ty_2Estring_2Echar))) = surj__c_ty_2Elist_2Elist_c_ty_2Elist_2Elist_ty_2Estring_2Echar(c_2Elist_2ENIL(ty_2Elist_2Elist(ty_2Estring_2Echar)))))) & ( ! [V1t:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V2h:tp__ty_2Estring_2Echar] : ( ! [V3P:$i] : (mem(V3P,arr(ty_2Estring_2Echar,bool)) => (surj__c_ty_2Elist_2Elist_c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Estring_2ETOKENS,V3P),ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V2h)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1t)))) = surj__c_ty_2Elist_2Elist_c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Ebool_2ELET(ty_2Epair_2Eprod(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Elist_2Elist(ty_2Estring_2Echar)),ty_2Elist_2Elist(ty_2Elist_2Elist(ty_2Estring_2Echar))),ap(c_2Epair_2EUNCURRY(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Elist_2Elist(ty_2Elist_2Elist(ty_2Estring_2Echar))),f1130(V3P))),ap(ap(c_2Erich__list_2ESPLITP(ty_2Estring_2Echar),V3P),ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V2h)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1t))))))))))))).
tff(conj_thm_2Estring_2EFIELDS__ind,lemma,(( ! [V0P_27:$i] : (mem(V0P_27,arr(arr(ty_2Estring_2Echar,bool),arr(ty_2Elist_2Elist(ty_2Estring_2Echar),bool))) => ((( ! [V1P:$i] : (mem(V1P,arr(ty_2Estring_2Echar,bool)) => p(ap(ap(V0P_27,V1P),c_2Elist_2ENIL(ty_2Estring_2Echar))))) & ( ! [V2P:$i] : (mem(V2P,arr(ty_2Estring_2Echar,bool)) => ( ! [V3h:tp__ty_2Estring_2Echar] : ( ! [V4t:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ((( ! [V5l:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V6r:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (((surj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Elist_2Elist(ty_2Estring_2Echar)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V5l)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V6r))) = surj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Erich__list_2ESPLITP(ty_2Estring_2Echar),V2P),ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V3h)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V4t))))) & p(ap(c_2Elist_2ENULL(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V5l)))) => p(ap(ap(V0P_27,V2P),ap(c_2Elist_2ETL(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V6r))))))) & ( ! [V7l:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V8r:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (((surj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Elist_2Elist(ty_2Estring_2Echar)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V7l)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V8r))) = surj__c_ty_2Epair_2Eprod_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Erich__list_2ESPLITP(ty_2Estring_2Echar),V2P),ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V3h)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V4t))))) & ((~~ p(ap(c_2Elist_2ENULL(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V7l)))) & (~~ p(ap(c_2Elist_2ENULL(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V8r)))))) => p(ap(ap(V0P_27,V2P),ap(c_2Elist_2ETL(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V8r)))))))) => p(ap(ap(V0P_27,V2P),ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V3h)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V4t)))))))))) => ( ! [V9v:$i] : (mem(V9v,arr(ty_2Estring_2Echar,bool)) => ( ! [V10v1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : p(ap(ap(V0P_27,V9v),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V10v1))))))))))).
tff(conj_thm_2Estring_2EFIELDS__def,lemma,((( ! [V0P:$i] : (mem(V0P,arr(ty_2Estring_2Echar,bool)) => (surj__c_ty_2Elist_2Elist_c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Estring_2EFIELDS,V0P),c_2Elist_2ENIL(ty_2Estring_2Echar))) = surj__c_ty_2Elist_2Elist_c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2ECONS(ty_2Elist_2Elist(ty_2Estring_2Echar)),c_2Elist_2ENIL(ty_2Estring_2Echar)),c_2Elist_2ENIL(ty_2Elist_2Elist(ty_2Estring_2Echar))))))) & ( ! [V1t:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V2h:tp__ty_2Estring_2Echar] : ( ! [V3P:$i] : (mem(V3P,arr(ty_2Estring_2Echar,bool)) => (surj__c_ty_2Elist_2Elist_c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Estring_2EFIELDS,V3P),ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V2h)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1t)))) = surj__c_ty_2Elist_2Elist_c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Ebool_2ELET(ty_2Epair_2Eprod(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Elist_2Elist(ty_2Estring_2Echar)),ty_2Elist_2Elist(ty_2Elist_2Elist(ty_2Estring_2Echar))),ap(c_2Epair_2EUNCURRY(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Elist_2Elist(ty_2Elist_2Elist(ty_2Estring_2Echar))),f1132(V3P))),ap(ap(c_2Erich__list_2ESPLITP(ty_2Estring_2Echar),V3P),ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V2h)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1t))))))))))))).
tff(ax_thm_2Estring_2EIMPLODE__def,axiom,((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EIMPLODE,c_2Elist_2ENIL(ty_2Estring_2Echar))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(c_2Elist_2ENIL(ty_2Estring_2Echar))) & ( ! [V0c:tp__ty_2Estring_2Echar] : ( ! [V1cs:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EIMPLODE,ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V0c)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1cs)))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V0c)),ap(c_2Estring_2EIMPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1cs))))))))).
tff(ax_thm_2Estring_2EEXPLODE__def,axiom,((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EEXPLODE,c_2Elist_2ENIL(ty_2Estring_2Echar))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(c_2Elist_2ENIL(ty_2Estring_2Echar))) & ( ! [V0c:tp__ty_2Estring_2Echar] : ( ! [V1s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EEXPLODE,ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V0c)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s)))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V0c)),ap(c_2Estring_2EEXPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s))))))))).
tff(conj_thm_2Estring_2EIMPLODE__EXPLODE__I,lemma,(( ! [V0s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EEXPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s))) = V0s) & (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EIMPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s))) = V0s))))).
tff(conj_thm_2Estring_2EIMPLODE__EXPLODE,lemma,(( ! [V0s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EIMPLODE,ap(c_2Estring_2EEXPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s)))) = V0s)))).
tff(conj_thm_2Estring_2EEXPLODE__IMPLODE,lemma,(( ! [V0cs:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EEXPLODE,ap(c_2Estring_2EIMPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0cs)))) = V0cs)))).
tff(conj_thm_2Estring_2EEXPLODE__ONTO,lemma,(( ! [V0cs:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (? [V1s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (V0cs = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EEXPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s)))))))).
tff(conj_thm_2Estring_2EIMPLODE__ONTO,lemma,(( ! [V0s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (? [V1cs:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (V0s = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EIMPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1cs)))))))).
tff(conj_thm_2Estring_2EEXPLODE__11,lemma,(( ! [V0s1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V1s2:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EEXPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s1))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EEXPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s2)))) <=> (V0s1 = V1s2)))))).
tff(conj_thm_2Estring_2EIMPLODE__11,lemma,(( ! [V0cs1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V1cs2:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EIMPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0cs1))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EIMPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1cs2)))) <=> (V0cs1 = V1cs2)))))).
tff(conj_thm_2Estring_2ESTRING__ACYCLIC,lemma,(( ! [V0s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V1c:tp__ty_2Estring_2Echar] : ((~~ (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V1c)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s))) = V0s)) & (~~ (V0s = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V1c)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s)))))))))).
tff(ax_thm_2Estring_2EEXTRACT__primitive__def,axiom,(c_2Estring_2EEXTRACT = ap(ap(c_2Erelation_2EWFREC(ty_2Epair_2Eprod(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Eoption_2Eoption(ty_2Enum_2Enum))),ty_2Elist_2Elist(ty_2Estring_2Echar)),ap(c_2Emin_2E_40(arr(ty_2Epair_2Eprod(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Eoption_2Eoption(ty_2Enum_2Enum))),arr(ty_2Epair_2Eprod(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Eoption_2Eoption(ty_2Enum_2Enum))),bool))),f1133)),k(arr(ty_2Epair_2Eprod(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Eoption_2Eoption(ty_2Enum_2Enum))),ty_2Elist_2Elist(ty_2Estring_2Echar)),f1139)))).
tff(conj_thm_2Estring_2EEXTRACT__ind,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2Epair_2Eprod(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Eoption_2Eoption(ty_2Enum_2Enum))),bool)) => ((( ! [V1s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V2i:tp__ty_2Enum_2Enum] : p(ap(V0P,ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Eoption_2Eoption(ty_2Enum_2Enum))),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Eoption_2Eoption(ty_2Enum_2Enum)),inj__ty_2Enum_2Enum(V2i)),c_2Eoption_2ENONE(ty_2Enum_2Enum))))))) & ( ! [V3s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V4i:tp__ty_2Enum_2Enum] : ( ! [V5n:tp__ty_2Enum_2Enum] : p(ap(V0P,ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Eoption_2Eoption(ty_2Enum_2Enum))),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V3s)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Eoption_2Eoption(ty_2Enum_2Enum)),inj__ty_2Enum_2Enum(V4i)),ap(c_2Eoption_2ESOME(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V5n)))))))))) => ( ! [V6v:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V7v1:tp__ty_2Enum_2Enum] : ( ! [V8v2:tp__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum] : p(ap(V0P,ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Eoption_2Eoption(ty_2Enum_2Enum))),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V6v)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Eoption_2Eoption(ty_2Enum_2Enum)),inj__ty_2Enum_2Enum(V7v1)),inj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(V8v2))))))))))))).
tff(conj_thm_2Estring_2EEXTRACT__def,lemma,(( ! [V0s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V1i:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EEXTRACT,ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Eoption_2Eoption(ty_2Enum_2Enum))),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Eoption_2Eoption(ty_2Enum_2Enum)),inj__ty_2Enum_2Enum(V1i)),c_2Eoption_2ENONE(ty_2Enum_2Enum))))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2ESUBSTRING,ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1i)),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Elist_2ELENGTH(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s))),inj__ty_2Enum_2Enum(V1i))))))) & (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EEXTRACT,ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Eoption_2Eoption(ty_2Enum_2Enum))),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Eoption_2Eoption(ty_2Enum_2Enum)),inj__ty_2Enum_2Enum(V1i)),ap(c_2Eoption_2ESOME(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V2n)))))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2ESUBSTRING,ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1i)),inj__ty_2Enum_2Enum(V2n)))))))))))).
tff(conj_thm_2Estring_2ESTRLEN__EXPLODE__THM,lemma,(( ! [V0s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s))) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(ty_2Estring_2Echar),ap(c_2Estring_2EEXPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s)))))))).
tff(ax_thm_2Estring_2EDEST__STRING__def,axiom,((surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EDEST__STRING,c_2Elist_2ENIL(ty_2Estring_2Echar))) = surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(c_2Eoption_2ENONE(ty_2Epair_2Eprod(ty_2Estring_2Echar,ty_2Elist_2Elist(ty_2Estring_2Echar))))) & ( ! [V0c:tp__ty_2Estring_2Echar] : ( ! [V1rst:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EDEST__STRING,ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V0c)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1rst)))) = surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Eoption_2ESOME(ty_2Epair_2Eprod(ty_2Estring_2Echar,ty_2Elist_2Elist(ty_2Estring_2Echar))),ap(ap(c_2Epair_2E_2C(ty_2Estring_2Echar,ty_2Elist_2Elist(ty_2Estring_2Echar)),inj__ty_2Estring_2Echar(V0c)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1rst))))))))).
tff(conj_thm_2Estring_2EDEST__STRING__LEMS,lemma,(( ! [V0c:tp__ty_2Estring_2Echar] : ( ! [V1t:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V2s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (((surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EDEST__STRING,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V2s))) = surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(c_2Eoption_2ENONE(ty_2Epair_2Eprod(ty_2Estring_2Echar,ty_2Elist_2Elist(ty_2Estring_2Echar))))) <=> (V2s = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(c_2Elist_2ENIL(ty_2Estring_2Echar)))) & ((surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EDEST__STRING,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V2s))) = surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Eoption_2ESOME(ty_2Epair_2Eprod(ty_2Estring_2Echar,ty_2Elist_2Elist(ty_2Estring_2Echar))),ap(ap(c_2Epair_2E_2C(ty_2Estring_2Echar,ty_2Elist_2Elist(ty_2Estring_2Echar)),inj__ty_2Estring_2Echar(V0c)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1t))))) <=> (V2s = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V0c)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1t))))))))))).
tff(conj_thm_2Estring_2EEXPLODE__EQNS,lemma,(((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EEXPLODE,c_2Elist_2ENIL(ty_2Estring_2Echar))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(c_2Elist_2ENIL(ty_2Estring_2Echar))) & ( ! [V0c:tp__ty_2Estring_2Echar] : ( ! [V1s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EEXPLODE,ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V0c)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s)))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V0c)),ap(c_2Estring_2EEXPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s)))))))))).
tff(conj_thm_2Estring_2EIMPLODE__EQNS,lemma,(((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EIMPLODE,c_2Elist_2ENIL(ty_2Estring_2Echar))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(c_2Elist_2ENIL(ty_2Estring_2Echar))) & ( ! [V0c:tp__ty_2Estring_2Echar] : ( ! [V1cs:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EIMPLODE,ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V0c)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1cs)))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V0c)),ap(c_2Estring_2EIMPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1cs)))))))))).
tff(conj_thm_2Estring_2EIMPLODE__EQ__EMPTYSTRING,lemma,(( ! [V0l:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EIMPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0l))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(c_2Elist_2ENIL(ty_2Estring_2Echar))) <=> (V0l = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(c_2Elist_2ENIL(ty_2Estring_2Echar)))) & ((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(c_2Elist_2ENIL(ty_2Estring_2Echar)) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EIMPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0l)))) <=> (V0l = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(c_2Elist_2ENIL(ty_2Estring_2Echar)))))))).
tff(conj_thm_2Estring_2EEXPLODE__EQ__NIL,lemma,(( ! [V0s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EEXPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(c_2Elist_2ENIL(ty_2Estring_2Echar))) <=> (V0s = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(c_2Elist_2ENIL(ty_2Estring_2Echar)))) & ((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(c_2Elist_2ENIL(ty_2Estring_2Echar)) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EEXPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s)))) <=> (V0s = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(c_2Elist_2ENIL(ty_2Estring_2Echar)))))))).
tff(conj_thm_2Estring_2EEXPLODE__EQ__THM,lemma,(( ! [V0s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V1h:tp__ty_2Estring_2Echar] : ( ! [V2t:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V1h)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V2t))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EEXPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s)))) <=> (V0s = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V1h)),ap(c_2Estring_2EIMPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V2t)))))) & ((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EEXPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V1h)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V2t)))) <=> (V0s = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V1h)),ap(c_2Estring_2EIMPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V2t)))))))))))).
tff(conj_thm_2Estring_2EIMPLODE__EQ__THM,lemma,(( ! [V0c:tp__ty_2Estring_2Echar] : ( ! [V1s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V2l:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V0c)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EIMPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V2l)))) <=> (V2l = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V0c)),ap(c_2Estring_2EEXPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s)))))) & ((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EIMPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V2l))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V0c)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s)))) <=> (V2l = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V0c)),ap(c_2Estring_2EEXPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s)))))))))))).
tff(conj_thm_2Estring_2EEXPLODE__DEST__STRING,lemma,(( ! [V0s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EEXPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(ap(c_2Eoption_2Eoption__CASE(ty_2Epair_2Eprod(ty_2Estring_2Echar,ty_2Elist_2Elist(ty_2Estring_2Echar)),ty_2Elist_2Elist(ty_2Estring_2Echar)),ap(c_2Estring_2EDEST__STRING,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s))),c_2Elist_2ENIL(ty_2Estring_2Echar)),f1142)))))).
tff(conj_thm_2Estring_2EIMPLODE__STRING,lemma,(( ! [V0clist:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EIMPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0clist))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(ap(c_2Elist_2EFOLDR(ty_2Estring_2Echar,ty_2Elist_2Elist(ty_2Estring_2Echar)),c_2Elist_2ECONS(ty_2Estring_2Echar)),c_2Elist_2ENIL(ty_2Estring_2Echar)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0clist))))))).
tff(conj_thm_2Estring_2ESTRLEN__EQ__0,lemma,(( ! [V0l:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0l))) = fo__c_2Enum_2E0) <=> (V0l = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(c_2Elist_2ENIL(ty_2Estring_2Echar))))))).
tff(conj_thm_2Estring_2ESTRLEN__THM,lemma,(((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(ty_2Estring_2Echar),c_2Elist_2ENIL(ty_2Estring_2Echar))) = fo__c_2Enum_2E0) & ( ! [V0h:tp__ty_2Estring_2Echar] : ( ! [V1t:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(ty_2Estring_2Echar),ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V0h)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1t)))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(c_2Elist_2ELENGTH(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1t)))))))))).
tff(conj_thm_2Estring_2ESTRLEN__DEF,lemma,(((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(ty_2Estring_2Echar),c_2Elist_2ENIL(ty_2Estring_2Echar))) = fo__c_2Enum_2E0) & ( ! [V0h:tp__ty_2Estring_2Echar] : ( ! [V1t:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(ty_2Estring_2Echar),ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V0h)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1t)))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(c_2Elist_2ELENGTH(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1t)))))))))).
tff(conj_thm_2Estring_2ESTRCAT__def,lemma,((( ! [V0l:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2EAPPEND(ty_2Estring_2Echar),c_2Elist_2ENIL(ty_2Estring_2Echar)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0l))) = V0l)) & ( ! [V1l1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V2l2:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V3h:tp__ty_2Estring_2Echar] : (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2EAPPEND(ty_2Estring_2Echar),ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V3h)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1l1))),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V2l2))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V3h)),ap(ap(c_2Elist_2EAPPEND(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1l1)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V2l2))))))))))).
tff(conj_thm_2Estring_2ESTRCAT,lemma,(( ! [V0s1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V1s2:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2EAPPEND(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s1)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s2))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2EAPPEND(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s1)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s2)))))))).
tff(conj_thm_2Estring_2ESTRCAT__EQNS,lemma,(( ! [V0s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V1c:tp__ty_2Estring_2Echar] : ( ! [V2s1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V3s2:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2EAPPEND(ty_2Estring_2Echar),c_2Elist_2ENIL(ty_2Estring_2Echar)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s))) = V0s) & ((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2EAPPEND(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s)),c_2Elist_2ENIL(ty_2Estring_2Echar))) = V0s) & (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2EAPPEND(ty_2Estring_2Echar),ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V1c)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V2s1))),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V3s2))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V1c)),ap(ap(c_2Elist_2EAPPEND(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V2s1)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V3s2))))))))))))).
tff(conj_thm_2Estring_2ESTRCAT__ASSOC,lemma,(( ! [V0l1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V1l2:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V2l3:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2EAPPEND(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0l1)),ap(ap(c_2Elist_2EAPPEND(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1l2)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V2l3)))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2EAPPEND(ty_2Estring_2Echar),ap(ap(c_2Elist_2EAPPEND(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0l1)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1l2))),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V2l3))))))))).
tff(conj_thm_2Estring_2ESTRCAT__11,lemma,((( ! [V0l1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V1l2:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V2l3:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2EAPPEND(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0l1)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1l2))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2EAPPEND(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0l1)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V2l3)))) <=> (V1l2 = V2l3))))) & ( ! [V3l1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V4l2:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V5l3:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2EAPPEND(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V4l2)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V3l1))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2EAPPEND(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V5l3)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V3l1)))) <=> (V4l2 = V5l3)))))))).
tff(conj_thm_2Estring_2ESTRCAT__ACYCLIC,lemma,(( ! [V0s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V1s1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (((V0s = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2EAPPEND(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s1)))) <=> (V1s1 = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(c_2Elist_2ENIL(ty_2Estring_2Echar)))) & ((V0s = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2EAPPEND(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s1)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s)))) <=> (V1s1 = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(c_2Elist_2ENIL(ty_2Estring_2Echar))))))))).
tff(conj_thm_2Estring_2ESTRCAT__EXPLODE,lemma,(( ! [V0s1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V1s2:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2EAPPEND(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s1)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s2))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(ap(c_2Elist_2EFOLDR(ty_2Estring_2Echar,ty_2Elist_2Elist(ty_2Estring_2Echar)),c_2Elist_2ECONS(ty_2Estring_2Echar)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s2)),ap(c_2Estring_2EEXPLODE,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s1))))))))).
tff(conj_thm_2Estring_2ESTRCAT__EQ__EMPTY,lemma,(( ! [V0l1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V1l2:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2EAPPEND(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0l1)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1l2))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(c_2Elist_2ENIL(ty_2Estring_2Echar))) <=> ((V0l1 = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(c_2Elist_2ENIL(ty_2Estring_2Echar))) & (V1l2 = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(c_2Elist_2ENIL(ty_2Estring_2Echar))))))))).
tff(conj_thm_2Estring_2ESTRLEN__CAT,lemma,(( ! [V0l1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V1l2:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(ty_2Estring_2Echar),ap(ap(c_2Elist_2EAPPEND(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0l1)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1l2)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Elist_2ELENGTH(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0l1))),ap(c_2Elist_2ELENGTH(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1l2))))))))).
tff(conj_thm_2Estring_2EisPREFIX__DEF,lemma,(( ! [V0s1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V1s2:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (p(ap(ap(c_2Elist_2EisPREFIX(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s1)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s2))) <=> p(ap(ap(c_2Epair_2Epair__CASE(bool,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Estring_2Echar,ty_2Elist_2Elist(ty_2Estring_2Echar))),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Estring_2Echar,ty_2Elist_2Elist(ty_2Estring_2Echar)))),ap(ap(c_2Epair_2E_2C(ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Estring_2Echar,ty_2Elist_2Elist(ty_2Estring_2Echar))),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Estring_2Echar,ty_2Elist_2Elist(ty_2Estring_2Echar)))),ap(c_2Estring_2EDEST__STRING,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s1))),ap(c_2Estring_2EDEST__STRING,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s2)))),f1150))))))).
tff(conj_thm_2Estring_2EisPREFIX__IND,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2Elist_2Elist(ty_2Estring_2Echar),arr(ty_2Elist_2Elist(ty_2Estring_2Echar),bool))) => (( ! [V1s1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V2s2:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (( ! [V3c:tp__ty_2Estring_2Echar] : ( ! [V4t1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V5t2:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (((surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EDEST__STRING,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s1))) = surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Eoption_2ESOME(ty_2Epair_2Eprod(ty_2Estring_2Echar,ty_2Elist_2Elist(ty_2Estring_2Echar))),ap(ap(c_2Epair_2E_2C(ty_2Estring_2Echar,ty_2Elist_2Elist(ty_2Estring_2Echar)),inj__ty_2Estring_2Echar(V3c)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V4t1))))) & (surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring_2EDEST__STRING,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V2s2))) = surj__c_ty_2Eoption_2Eoption_c_ty_2Epair_2Eprod_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Eoption_2ESOME(ty_2Epair_2Eprod(ty_2Estring_2Echar,ty_2Elist_2Elist(ty_2Estring_2Echar))),ap(ap(c_2Epair_2E_2C(ty_2Estring_2Echar,ty_2Elist_2Elist(ty_2Estring_2Echar)),inj__ty_2Estring_2Echar(V3c)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V5t2)))))) => p(ap(ap(V0P,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V4t1)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V5t2))))))) => p(ap(ap(V0P,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s1)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V2s2)))))) => ( ! [V6v:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V7v1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : p(ap(ap(V0P,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V6v)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V7v1)))))))))).
tff(conj_thm_2Estring_2EisPREFIX__STRCAT,lemma,(( ! [V0s1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V1s2:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (p(ap(ap(c_2Elist_2EisPREFIX(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s1)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s2))) <=> (? [V2s3:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (V1s2 = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(c_2Elist_2EAPPEND(ty_2Estring_2Echar),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s1)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V2s3)))))))))).
tff(conj_thm_2Estring_2Estring__lt__ind,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2Elist_2Elist(ty_2Estring_2Echar),arr(ty_2Elist_2Elist(ty_2Estring_2Echar),bool))) => ((( ! [V1s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : p(ap(ap(V0P,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s)),c_2Elist_2ENIL(ty_2Estring_2Echar)))) & (( ! [V2c:tp__ty_2Estring_2Echar] : ( ! [V3s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : p(ap(ap(V0P,c_2Elist_2ENIL(ty_2Estring_2Echar)),ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V2c)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V3s)))))) & ( ! [V4c1:tp__ty_2Estring_2Echar] : ( ! [V5s1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V6c2:tp__ty_2Estring_2Echar] : ( ! [V7s2:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (p(ap(ap(V0P,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V5s1)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V7s2))) => p(ap(ap(V0P,ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V4c1)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V5s1))),ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V6c2)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V7s2))))))))))) => ( ! [V8v:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V9v1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : p(ap(ap(V0P,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V8v)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V9v1)))))))))).
tff(conj_thm_2Estring_2Estring__lt__def,lemma,((( ! [V0s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (p(ap(ap(c_2Estring_2Estring__lt,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s)),c_2Elist_2ENIL(ty_2Estring_2Echar))) <=> $false)) & (( ! [V1s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V2c:tp__ty_2Estring_2Echar] : (p(ap(ap(c_2Estring_2Estring__lt,c_2Elist_2ENIL(ty_2Estring_2Echar)),ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V2c)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s)))) <=> $true))) & ( ! [V3s2:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V4s1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V5c2:tp__ty_2Estring_2Echar] : ( ! [V6c1:tp__ty_2Estring_2Echar] : (p(ap(ap(c_2Estring_2Estring__lt,ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V6c1)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V4s1))),ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V5c2)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V3s2)))) <=> (p(ap(ap(c_2Estring_2Echar__lt,inj__ty_2Estring_2Echar(V6c1)),inj__ty_2Estring_2Echar(V5c2))) | ((V6c1 = V5c2) & p(ap(ap(c_2Estring_2Estring__lt,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V4s1)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V3s2)))))))))))))).
tff(ax_thm_2Estring_2Estring__le__def,axiom,( ! [V0s1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V1s2:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (p(ap(ap(c_2Estring_2Estring__le,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s1)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s2))) <=> ((V0s1 = V1s2) | p(ap(ap(c_2Estring_2Estring__lt,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s1)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s2)))))))).
tff(ax_thm_2Estring_2Estring__gt__def,axiom,( ! [V0s1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V1s2:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (p(ap(ap(c_2Estring_2Estring__gt,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s1)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s2))) <=> p(ap(ap(c_2Estring_2Estring__lt,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s2)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s1))))))).
tff(ax_thm_2Estring_2Estring__ge__def,axiom,( ! [V0s1:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V1s2:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (p(ap(ap(c_2Estring_2Estring__ge,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s1)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s2))) <=> p(ap(ap(c_2Estring_2Estring__le,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s2)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s1))))))).
tff(conj_thm_2Estring_2Estring__lt__nonrefl,lemma,(( ! [V0s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (~~ p(ap(ap(c_2Estring_2Estring__lt,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s))))))).
tff(conj_thm_2Estring_2Estring__lt__antisym,conjecture,(( ! [V0s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ( ! [V1t:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (~~ (p(ap(ap(c_2Estring_2Estring__lt,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1t))) & p(ap(ap(c_2Estring_2Estring__lt,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1t)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s))))))))).