include('Axioms/numposrep_2.ax').
tff(tp_c_2EpatternMatches_2EAPPLY__REDUNDANT__ROWS__INFO,type,(c_2EpatternMatches_2EAPPLY__REDUNDANT__ROWS__INFO:del > $i)).
tff(mem_c_2EpatternMatches_2EAPPLY__REDUNDANT__ROWS__INFO,axiom,( ! [A_27a:del] : mem(c_2EpatternMatches_2EAPPLY__REDUNDANT__ROWS__INFO(A_27a),arr(ty_2Elist_2Elist(bool),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))))).
tff(tp_c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO,type,(c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO:(del * del) > $i)).
tff(mem_c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO(A_27a,A_27b),arr(A_27a,arr(ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),arr(bool,arr(ty_2Elist_2Elist(bool),bool)))))))).
tff(tp_c_2EpatternMatches_2EPMATCH,type,(c_2EpatternMatches_2EPMATCH:(del * del) > $i)).
tff(mem_c_2EpatternMatches_2EPMATCH,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EpatternMatches_2EPMATCH(A_27a,A_27b),arr(A_27b,arr(ty_2Elist_2Elist(arr(A_27b,ty_2Eoption_2Eoption(A_27a))),A_27a)))))).
tff(tp_c_2EpatternMatches_2EPMATCH__EQUIV__ROWS,type,(c_2EpatternMatches_2EPMATCH__EQUIV__ROWS:(del * del) > $i)).
tff(mem_c_2EpatternMatches_2EPMATCH__EQUIV__ROWS,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EpatternMatches_2EPMATCH__EQUIV__ROWS(A_27a,A_27b),arr(A_27a,arr(ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),arr(ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),bool))))))).
tff(tp_c_2EpatternMatches_2EPMATCH__EXPAND__PRED,type,(c_2EpatternMatches_2EPMATCH__EXPAND__PRED:(del * del) > $i)).
tff(mem_c_2EpatternMatches_2EPMATCH__EXPAND__PRED,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EpatternMatches_2EPMATCH__EXPAND__PRED(A_27a,A_27b),arr(arr(A_27a,bool),arr(A_27b,arr(ty_2Elist_2Elist(arr(A_27b,ty_2Eoption_2Eoption(A_27a))),arr(ty_2Elist_2Elist(arr(A_27b,ty_2Eoption_2Eoption(A_27a))),bool)))))))).
tff(tp_c_2EpatternMatches_2EPMATCH__FLATTEN__FUN,type,(c_2EpatternMatches_2EPMATCH__FLATTEN__FUN:(del * del * del) > $i)).
tff(mem_c_2EpatternMatches_2EPMATCH__FLATTEN__FUN,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : mem(c_2EpatternMatches_2EPMATCH__FLATTEN__FUN(A_27a,A_27b,A_27c),arr(arr(A_27b,A_27c),arr(arr(A_27b,bool),arr(arr(A_27b,arr(A_27b,ty_2Eoption_2Eoption(A_27a))),arr(A_27c,ty_2Eoption_2Eoption(A_27a)))))))))).
tff(tp_c_2EpatternMatches_2EPMATCH__INCOMPLETE,type,(c_2EpatternMatches_2EPMATCH__INCOMPLETE:del > $i)).
tff(mem_c_2EpatternMatches_2EPMATCH__INCOMPLETE,axiom,( ! [A_27a:del] : mem(c_2EpatternMatches_2EPMATCH__INCOMPLETE(A_27a),A_27a))).
tff(tp_c_2EpatternMatches_2EPMATCH__IS__EXHAUSTIVE,type,(c_2EpatternMatches_2EPMATCH__IS__EXHAUSTIVE:(del * del) > $i)).
tff(mem_c_2EpatternMatches_2EPMATCH__IS__EXHAUSTIVE,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EpatternMatches_2EPMATCH__IS__EXHAUSTIVE(A_27a,A_27b),arr(A_27a,arr(ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),bool)))))).
tff(tp_c_2EpatternMatches_2EPMATCH__ROW,type,(c_2EpatternMatches_2EPMATCH__ROW:(del * del * del) > $i)).
tff(mem_c_2EpatternMatches_2EPMATCH__ROW,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : mem(c_2EpatternMatches_2EPMATCH__ROW(A_27a,A_27b,A_27c),arr(arr(A_27b,A_27c),arr(arr(A_27b,bool),arr(arr(A_27b,A_27a),arr(A_27c,ty_2Eoption_2Eoption(A_27a)))))))))).
tff(tp_c_2EpatternMatches_2EPMATCH__ROW__COND,type,(c_2EpatternMatches_2EPMATCH__ROW__COND:(del * del) > $i)).
tff(mem_c_2EpatternMatches_2EPMATCH__ROW__COND,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EpatternMatches_2EPMATCH__ROW__COND(A_27a,A_27b),arr(arr(A_27a,A_27b),arr(arr(A_27a,bool),arr(A_27b,arr(A_27a,bool)))))))).
tff(tp_c_2EpatternMatches_2EPMATCH__ROW__COND__EX,type,(c_2EpatternMatches_2EPMATCH__ROW__COND__EX:(del * del) > $i)).
tff(mem_c_2EpatternMatches_2EPMATCH__ROW__COND__EX,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EpatternMatches_2EPMATCH__ROW__COND__EX(A_27a,A_27b),arr(A_27a,arr(arr(A_27b,A_27a),arr(arr(A_27b,bool),bool))))))).
tff(tp_c_2EpatternMatches_2EPMATCH__ROW__COND__NOT__EX__OR__EQ,type,(c_2EpatternMatches_2EPMATCH__ROW__COND__NOT__EX__OR__EQ:(del * del) > $i)).
tff(mem_c_2EpatternMatches_2EPMATCH__ROW__COND__NOT__EX__OR__EQ,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EpatternMatches_2EPMATCH__ROW__COND__NOT__EX__OR__EQ(A_27a,A_27b),arr(A_27a,arr(arr(A_27a,ty_2Eoption_2Eoption(A_27b)),arr(ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),bool))))))).
tff(tp_c_2EpatternMatches_2EPMATCH__ROW__LIFT,type,(c_2EpatternMatches_2EPMATCH__ROW__LIFT:(del * del * del) > $i)).
tff(mem_c_2EpatternMatches_2EPMATCH__ROW__LIFT,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : mem(c_2EpatternMatches_2EPMATCH__ROW__LIFT(A_27a,A_27b,A_27c),arr(arr(A_27c,A_27b),arr(arr(A_27a,ty_2Eoption_2Eoption(A_27c)),arr(A_27a,ty_2Eoption_2Eoption(A_27b))))))))).
tff(tp_c_2EpatternMatches_2EPMATCH__ROW__REDUNDANT,type,(c_2EpatternMatches_2EPMATCH__ROW__REDUNDANT:(del * del) > $i)).
tff(mem_c_2EpatternMatches_2EPMATCH__ROW__REDUNDANT,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EpatternMatches_2EPMATCH__ROW__REDUNDANT(A_27a,A_27b),arr(A_27a,arr(ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),arr(ty_2Enum_2Enum,bool))))))).
tff(tp_c_2EpatternMatches_2EPMATCH__ROW__magic__0,type,(c_2EpatternMatches_2EPMATCH__ROW__magic__0:(del * del) > $i)).
tff(mem_c_2EpatternMatches_2EPMATCH__ROW__magic__0,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EpatternMatches_2EPMATCH__ROW__magic__0(A_27a,A_27b),arr(ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(bool,A_27b)),arr(A_27a,ty_2Eoption_2Eoption(A_27b))))))).
tff(tp_c_2EpatternMatches_2EPMATCH__ROW__magic__1,type,(c_2EpatternMatches_2EPMATCH__ROW__magic__1:(del * del * del) > $i)).
tff(mem_c_2EpatternMatches_2EPMATCH__ROW__magic__1,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : mem(c_2EpatternMatches_2EPMATCH__ROW__magic__1(A_27a,A_27b,A_27c),arr(arr(A_27a,ty_2Epair_2Eprod(A_27b,ty_2Epair_2Eprod(bool,A_27c))),arr(A_27b,ty_2Eoption_2Eoption(A_27c)))))))).
tff(tp_c_2EpatternMatches_2EPMATCH__ROW__magic__2,type,(c_2EpatternMatches_2EPMATCH__ROW__magic__2:(del * del) > $i)).
tff(mem_c_2EpatternMatches_2EPMATCH__ROW__magic__2,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EpatternMatches_2EPMATCH__ROW__magic__2(A_27a,A_27b),arr(A_27a,arr(bool,arr(A_27b,ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(bool,A_27b))))))))).
tff(tp_c_2EpatternMatches_2EPMATCH__ROW__magic__3,type,(c_2EpatternMatches_2EPMATCH__ROW__magic__3:(del * del) > $i)).
tff(mem_c_2EpatternMatches_2EPMATCH__ROW__magic__3,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EpatternMatches_2EPMATCH__ROW__magic__3(A_27a,A_27b),arr(A_27a,arr(A_27b,ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(bool,A_27b)))))))).
tff(tp_c_2EpatternMatches_2EPMATCH__ROW__magic__4,type,(c_2EpatternMatches_2EPMATCH__ROW__magic__4:(del * del) > $i)).
tff(mem_c_2EpatternMatches_2EPMATCH__ROW__magic__4,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EpatternMatches_2EPMATCH__ROW__magic__4(A_27a,A_27b),arr(ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(bool,A_27b)),arr(A_27a,ty_2Eoption_2Eoption(A_27b))))))).
tff(tp_c_2EpatternMatches_2EPMATCH__magic__1,type,(c_2EpatternMatches_2EPMATCH__magic__1:(del * del) > $i)).
tff(mem_c_2EpatternMatches_2EPMATCH__magic__1,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EpatternMatches_2EPMATCH__magic__1(A_27a,A_27b),arr(A_27a,arr(ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),A_27b)))))).
tff(tp_c_2EpatternMatches_2EREDUNDANT__ROWS__INFOS__CONJ,type,(c_2EpatternMatches_2EREDUNDANT__ROWS__INFOS__CONJ:$i)).
tff(mem_c_2EpatternMatches_2EREDUNDANT__ROWS__INFOS__CONJ,axiom,mem(c_2EpatternMatches_2EREDUNDANT__ROWS__INFOS__CONJ,arr(ty_2Elist_2Elist(bool),arr(ty_2Elist_2Elist(bool),ty_2Elist_2Elist(bool))))).
tff(tp_c_2EpatternMatches_2EREDUNDANT__ROWS__INFOS__DISJ,type,(c_2EpatternMatches_2EREDUNDANT__ROWS__INFOS__DISJ:$i)).
tff(mem_c_2EpatternMatches_2EREDUNDANT__ROWS__INFOS__DISJ,axiom,mem(c_2EpatternMatches_2EREDUNDANT__ROWS__INFOS__DISJ,arr(ty_2Elist_2Elist(bool),arr(ty_2Elist_2Elist(bool),ty_2Elist_2Elist(bool))))).
tff(tp_c_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO,type,(c_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO:(del * del) > $i)).
tff(mem_c_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO(A_27a,A_27b),arr(A_27a,arr(ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),ty_2Elist_2Elist(bool))))))).
tff(stp_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o,type,(tp__c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o : $tType)).
tff(stp_inj_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o,type,(inj__c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o : tp__c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o > $i)).
tff(stp_surj_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o,type,(surj__c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o : $i > tp__c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o)).
tff(stp_inj_surj_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o] : (surj__c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o(inj__c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o(X)) = X))).
tff(stp_inj_mem_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o] : (mem(inj__c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o(X),ty_2Epair_2Eprod(bool,ty_2Elist_2Elist(bool)))))).
tff(stp_iso_mem_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o,axiom,( ! [X:$i] : (mem(X,ty_2Epair_2Eprod(bool,ty_2Elist_2Elist(bool))) => (X = inj__c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o(surj__c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o(X)))))).
tff(tp_c_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO__AUX,type,(c_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO__AUX:(del * del) > $i)).
tff(mem_c_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO__AUX,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO__AUX(A_27a,A_27b),arr(A_27a,arr(ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),arr(bool,arr(ty_2Elist_2Elist(bool),ty_2Epair_2Eprod(bool,ty_2Elist_2Elist(bool)))))))))).
tff(stp_c_ty_2Eoption_2Eoption_o,type,(tp__c_ty_2Eoption_2Eoption_o : $tType)).
tff(stp_inj_c_ty_2Eoption_2Eoption_o,type,(inj__c_ty_2Eoption_2Eoption_o : tp__c_ty_2Eoption_2Eoption_o > $i)).
tff(stp_surj_c_ty_2Eoption_2Eoption_o,type,(surj__c_ty_2Eoption_2Eoption_o : $i > tp__c_ty_2Eoption_2Eoption_o)).
tff(stp_inj_surj_c_ty_2Eoption_2Eoption_o,axiom,( ! [X:tp__c_ty_2Eoption_2Eoption_o] : (surj__c_ty_2Eoption_2Eoption_o(inj__c_ty_2Eoption_2Eoption_o(X)) = X))).
tff(stp_inj_mem_c_ty_2Eoption_2Eoption_o,axiom,( ! [X:tp__c_ty_2Eoption_2Eoption_o] : (mem(inj__c_ty_2Eoption_2Eoption_o(X),ty_2Eoption_2Eoption(bool))))).
tff(stp_iso_mem_c_ty_2Eoption_2Eoption_o,axiom,( ! [X:$i] : (mem(X,ty_2Eoption_2Eoption(bool)) => (X = inj__c_ty_2Eoption_2Eoption_o(surj__c_ty_2Eoption_2Eoption_o(X)))))).
tff(conj_thm_2EpatternMatches_2Esome__var__bool__T,lemma,((surj__c_ty_2Eoption_2Eoption_o(ap(c_2Eoption_2Esome(bool),i(bool))) = surj__c_ty_2Eoption_2Eoption_o(ap(c_2Eoption_2ESOME(bool),inj__o(fo__c_2Ebool_2ET)))))).
tff(conj_thm_2EpatternMatches_2Esome__var__bool__F,lemma,((surj__c_ty_2Eoption_2Eoption_o(ap(c_2Eoption_2Esome(bool),f821)) = surj__c_ty_2Eoption_2Eoption_o(ap(c_2Eoption_2ESOME(bool),inj__o(fo__c_2Ebool_2EF)))))).
tff(ax_thm_2EpatternMatches_2EPMATCH__ROW__COND__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0pat:$i] : (mem(V0pat,arr(A_27a,A_27b)) => ( ! [V1guard:$i] : (mem(V1guard,arr(A_27a,bool)) => ( ! [V2inp:$i] : (mem(V2inp,A_27b) => ( ! [V3v:$i] : (mem(V3v,A_27a) => (p(ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND(A_27a,A_27b),V0pat),V1guard),V2inp),V3v)) <=> ((ap(V0pat,V3v) = V2inp) & p(ap(V1guard,V3v))))))))))))))).
tff(ax_thm_2EpatternMatches_2EPMATCH__ROW__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0pat:$i] : (mem(V0pat,arr(A_27b,A_27c)) => ( ! [V1guard:$i] : (mem(V1guard,arr(A_27b,bool)) => ( ! [V2rhs:$i] : (mem(V2rhs,arr(A_27b,A_27a)) => ( ! [V3i:$i] : (mem(V3i,A_27c) => (ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27a,A_27b,A_27c),V0pat),V1guard),V2rhs),V3i) = ap(ap(c_2Eoption_2EOPTION__MAP(A_27b,A_27a),V2rhs),ap(c_2Eoption_2Esome(A_27b),f822(A_27c,A_27b,V3i,V0pat,V1guard)))))))))))))))).
tff(ax_thm_2EpatternMatches_2EPMATCH__INCOMPLETE__def,axiom,( ! [A_27a:del]: (c_2EpatternMatches_2EPMATCH__INCOMPLETE(A_27a) = c_2Ebool_2EARB(A_27a)))).
tff(ax_thm_2EpatternMatches_2EPMATCH__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0v:$i] : (mem(V0v,A_27b) => (ap(ap(c_2EpatternMatches_2EPMATCH(A_27a,A_27b),V0v),c_2Elist_2ENIL(arr(A_27b,ty_2Eoption_2Eoption(A_27a)))) = c_2EpatternMatches_2EPMATCH__INCOMPLETE(A_27a)))) & ( ! [V1v:$i] : (mem(V1v,A_27b) => ( ! [V2r:$i] : (mem(V2r,arr(A_27b,ty_2Eoption_2Eoption(A_27a))) => ( ! [V3rs:$i] : (mem(V3rs,ty_2Elist_2Elist(arr(A_27b,ty_2Eoption_2Eoption(A_27a)))) => (ap(ap(c_2EpatternMatches_2EPMATCH(A_27a,A_27b),V1v),ap(ap(c_2Elist_2ECONS(arr(A_27b,ty_2Eoption_2Eoption(A_27a))),V2r),V3rs)) = ap(ap(ap(c_2Eoption_2Eoption__CASE(A_27a,A_27a),ap(V2r,V1v)),ap(ap(c_2EpatternMatches_2EPMATCH(A_27a,A_27b),V1v),V3rs)),c_2Ecombin_2EI(A_27a))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROW__CONG,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0p:$i] : (mem(V0p,arr(A_27a,A_27b)) => ( ! [V1p_27:$i] : (mem(V1p_27,arr(A_27a,A_27b)) => ( ! [V2g:$i] : (mem(V2g,arr(A_27a,bool)) => ( ! [V3g_27:$i] : (mem(V3g_27,arr(A_27a,bool)) => ( ! [V4r:$i] : (mem(V4r,arr(A_27a,A_27c)) => ( ! [V5r_27:$i] : (mem(V5r_27,arr(A_27a,A_27c)) => ( ! [V6v:$i] : (mem(V6v,A_27b) => ( ! [V7v_27:$i] : (mem(V7v_27,A_27b) => (((V0p = V1p_27) & ((V6v = V7v_27) & (( ! [V8x:$i] : (mem(V8x,A_27a) => ((V6v = ap(V0p,V8x)) => (p(ap(V2g,V8x)) <=> p(ap(V3g_27,V8x)))))) & ( ! [V9x:$i] : (mem(V9x,A_27a) => (((V6v = ap(V0p,V9x)) & p(ap(V2g,V9x))) => (ap(V4r,V9x) = ap(V5r_27,V9x)))))))) => (ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27c,A_27a,A_27b),V0p),V2g),V4r),V6v) = ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27c,A_27a,A_27b),V1p_27),V3g_27),V5r_27),V7v_27)))))))))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__CONG,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1v_27:$i] : (mem(V1v_27,A_27a) => ( ! [V2rows:$i] : (mem(V2rows,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V3rows_27:$i] : (mem(V3rows_27,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V4r:$i] : (mem(V4r,arr(A_27a,ty_2Eoption_2Eoption(A_27b))) => ( ! [V5r_27:$i] : (mem(V5r_27,arr(A_27a,ty_2Eoption_2Eoption(A_27b))) => (((V0v = V1v_27) & ((ap(V4r,V1v_27) = ap(V5r_27,V1v_27)) & (ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27a),V1v_27),V2rows) = ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27a),V1v_27),V3rows_27)))) => (ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27a),V0v),ap(ap(c_2Elist_2ECONS(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V4r),V2rows)) = ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27a),V1v_27),ap(ap(c_2Elist_2ECONS(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V5r_27),V3rows_27)))))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROW__EQ__AUX,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0p:$i] : (mem(V0p,arr(A_27b,A_27a)) => ( ! [V1g:$i] : (mem(V1g,arr(A_27b,bool)) => ( ! [V2p_27:$i] : (mem(V2p_27,arr(A_27c,A_27a)) => ( ! [V3g_27:$i] : (mem(V3g_27,arr(A_27c,bool)) => ( ! [V4r:$i] : (mem(V4r,arr(A_27b,A_27d)) => ( ! [V5r_27:$i] : (mem(V5r_27,arr(A_27c,A_27d)) => ((( ! [V6i:$i] : (mem(V6i,A_27a) => ((? [V7x:$i] : (mem(V7x,A_27b) & p(ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND(A_27b,A_27a),V0p),V1g),V6i),V7x)))) <=> (? [V8x_27:$i] : (mem(V8x_27,A_27c) & p(ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND(A_27c,A_27a),V2p_27),V3g_27),V6i),V8x_27))))))) & ( ! [V9x:$i] : (mem(V9x,A_27b) => ( ! [V10x_27:$i] : (mem(V10x_27,A_27c) => (((ap(V0p,V9x) = ap(V2p_27,V10x_27)) & (p(ap(V1g,V9x)) & p(ap(V3g_27,V10x_27)))) => (ap(V4r,V9x) = ap(V5r_27,V10x_27)))))))) => (ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27d,A_27b,A_27a),V0p),V1g),V4r) = ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27d,A_27c,A_27a),V2p_27),V3g_27),V5r_27))))))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROW__EQ__NONE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0p:$i] : (mem(V0p,arr(A_27b,A_27c)) => ( ! [V1g:$i] : (mem(V1g,arr(A_27b,bool)) => ( ! [V2r:$i] : (mem(V2r,arr(A_27b,A_27a)) => ( ! [V3i:$i] : (mem(V3i,A_27c) => ((ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27a,A_27b,A_27c),V0p),V1g),V2r),V3i) = c_2Eoption_2ENONE(A_27a)) <=> ( ! [V4x:$i] : (mem(V4x,A_27b) => (~~ p(ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND(A_27b,A_27c),V0p),V1g),V3i),V4x))))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROW__EQ__SOME,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0p:$i] : (mem(V0p,arr(A_27b,A_27c)) => ( ! [V1g:$i] : (mem(V1g,arr(A_27b,bool)) => ( ! [V2r:$i] : (mem(V2r,arr(A_27b,A_27a)) => ( ! [V3i:$i] : (mem(V3i,A_27c) => ( ! [V4y:$i] : (mem(V4y,A_27a) => ((ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27a,A_27b,A_27c),V0p),V1g),V2r),V3i) = ap(c_2Eoption_2ESOME(A_27a),V4y)) => (? [V5x:$i] : (mem(V5x,A_27b) & (p(ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND(A_27b,A_27c),V0p),V1g),V3i),V5x)) & (V4y = ap(V2r,V5x))))))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__COND__SELECT__UNIQUE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p:$i] : (mem(V0p,arr(A_27a,A_27b)) => ( ! [V1g:$i] : (mem(V1g,arr(A_27a,bool)) => ( ! [V2i:$i] : (mem(V2i,A_27b) => (( ! [V3x1:$i] : (mem(V3x1,A_27a) => ( ! [V4x2:$i] : (mem(V4x2,A_27a) => ((p(ap(V1g,V3x1)) & (p(ap(V1g,V4x2)) & (ap(V0p,V3x1) = ap(V0p,V4x2)))) => (V3x1 = V4x2)))))) => ( ! [V5x:$i] : (mem(V5x,A_27a) => (p(ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND(A_27a,A_27b),V0p),V1g),V2i),V5x)) => (ap(c_2Emin_2E_40(A_27a),f823(A_27b,A_27a,V2i,V0p,V1g)) = V5x))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROW__COND__DEF__GSYM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0pat:$i] : (mem(V0pat,arr(A_27a,A_27b)) => ( ! [V1guard:$i] : (mem(V1guard,arr(A_27a,bool)) => ( ! [V2inp:$i] : (mem(V2inp,A_27b) => ( ! [V3v:$i] : (mem(V3v,A_27a) => (p(ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND(A_27a,A_27b),V0pat),V1guard),V2inp),V3v)) <=> ((V2inp = ap(V0pat,V3v)) & p(ap(V1guard,V3v)))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__EVAL,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0v:$i] : (mem(V0v,A_27b) => ( ! [V1p:$i] : (mem(V1p,arr(A_27d,A_27b)) => ( ! [V2g:$i] : (mem(V2g,arr(A_27d,bool)) => ( ! [V3r:$i] : (mem(V3r,arr(A_27d,A_27c)) => ( ! [V4rs:$i] : (mem(V4rs,ty_2Elist_2Elist(arr(A_27b,ty_2Eoption_2Eoption(A_27c)))) => ((ap(ap(c_2EpatternMatches_2EPMATCH(A_27a,A_27b),V0v),c_2Elist_2ENIL(arr(A_27b,ty_2Eoption_2Eoption(A_27a)))) = c_2EpatternMatches_2EPMATCH__INCOMPLETE(A_27a)) & (ap(ap(c_2EpatternMatches_2EPMATCH(A_27c,A_27b),V0v),ap(ap(c_2Elist_2ECONS(arr(A_27b,ty_2Eoption_2Eoption(A_27c))),ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27c,A_27d,A_27b),V1p),V2g),V3r)),V4rs)) = ap(ap(ap(c_2Ebool_2ECOND(A_27c),ap(c_2Ebool_2E_3F(A_27d),f824(A_27b,A_27d,V0v,V1p,V2g))),ap(V3r,ap(c_2Emin_2E_40(A_27d),f825(A_27b,A_27d,V0v,V1p,V2g)))),ap(ap(c_2EpatternMatches_2EPMATCH(A_27c,A_27b),V0v),V4rs)))))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__EVAL__MATCH,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0p:$i] : (mem(V0p,arr(A_27b,A_27c)) => ( ! [V1g:$i] : (mem(V1g,arr(A_27b,bool)) => ( ! [V2r:$i] : (mem(V2r,arr(A_27b,A_27a)) => ( ! [V3v:$i] : (mem(V3v,A_27c) => ( ! [V4rs:$i] : (mem(V4rs,ty_2Elist_2Elist(arr(A_27c,ty_2Eoption_2Eoption(A_27a)))) => ((~~ (ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27a,A_27b,A_27c),V0p),V1g),V2r),V3v) = c_2Eoption_2ENONE(A_27a))) => (ap(ap(c_2EpatternMatches_2EPMATCH(A_27a,A_27c),V3v),ap(ap(c_2Elist_2ECONS(arr(A_27c,ty_2Eoption_2Eoption(A_27a))),ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27a,A_27b,A_27c),V0p),V1g),V2r)),V4rs)) = ap(V2r,ap(c_2Emin_2E_40(A_27b),f826(A_27c,A_27b,V3v,V0p,V1g)))))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__EXTEND__BASE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0v__old:$i] : (mem(V0v__old,A_27a) => ( ! [V1v__new:$i] : (mem(V1v__new,A_27b) => (ap(ap(c_2EpatternMatches_2EPMATCH(A_27c,A_27a),V0v__old),c_2Elist_2ENIL(arr(A_27a,ty_2Eoption_2Eoption(A_27c)))) = ap(ap(c_2EpatternMatches_2EPMATCH(A_27c,A_27b),V1v__new),c_2Elist_2ENIL(arr(A_27b,ty_2Eoption_2Eoption(A_27c)))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__EXTEND__BOTH,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0v__old:$i] : (mem(V0v__old,A_27a) => ( ! [V1v__new:$i] : (mem(V1v__new,A_27b) => ( ! [V2rows__old:$i] : (mem(V2rows__old,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27c)))) => ( ! [V3rows__new:$i] : (mem(V3rows__new,ty_2Elist_2Elist(arr(A_27b,ty_2Eoption_2Eoption(A_27c)))) => ( ! [V4r__old:$i] : (mem(V4r__old,arr(A_27a,ty_2Eoption_2Eoption(A_27c))) => ( ! [V5r__new:$i] : (mem(V5r__new,arr(A_27b,ty_2Eoption_2Eoption(A_27c))) => ((ap(V4r__old,V0v__old) = ap(V5r__new,V1v__new)) => ((ap(ap(c_2EpatternMatches_2EPMATCH(A_27c,A_27a),V0v__old),V2rows__old) = ap(ap(c_2EpatternMatches_2EPMATCH(A_27c,A_27b),V1v__new),V3rows__new)) => (ap(ap(c_2EpatternMatches_2EPMATCH(A_27c,A_27a),V0v__old),ap(ap(c_2Elist_2ECONS(arr(A_27a,ty_2Eoption_2Eoption(A_27c))),V4r__old),V2rows__old)) = ap(ap(c_2EpatternMatches_2EPMATCH(A_27c,A_27b),V1v__new),ap(ap(c_2Elist_2ECONS(arr(A_27b,ty_2Eoption_2Eoption(A_27c))),V5r__new),V3rows__new)))))))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__EXTEND__BOTH__ID,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rows__old:$i] : (mem(V1rows__old,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V2rows__new:$i] : (mem(V2rows__new,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V3r:$i] : (mem(V3r,arr(A_27a,ty_2Eoption_2Eoption(A_27b))) => ((ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27a),V0v),V1rows__old) = ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27a),V0v),V2rows__new)) => (ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27a),V0v),ap(ap(c_2Elist_2ECONS(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V3r),V1rows__old)) = ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27a),V0v),ap(ap(c_2Elist_2ECONS(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V3r),V2rows__new)))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__EXTEND__OLD,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0v__old:$i] : (mem(V0v__old,A_27a) => ( ! [V1v__new:$i] : (mem(V1v__new,A_27b) => ( ! [V2rows__old:$i] : (mem(V2rows__old,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27c)))) => ( ! [V3rows__new:$i] : (mem(V3rows__new,ty_2Elist_2Elist(arr(A_27b,ty_2Eoption_2Eoption(A_27c)))) => ( ! [V4r__old:$i] : (mem(V4r__old,arr(A_27a,ty_2Eoption_2Eoption(A_27c))) => ((ap(V4r__old,V0v__old) = c_2Eoption_2ENONE(A_27c)) => ((ap(ap(c_2EpatternMatches_2EPMATCH(A_27c,A_27a),V0v__old),V2rows__old) = ap(ap(c_2EpatternMatches_2EPMATCH(A_27c,A_27b),V1v__new),V3rows__new)) => (ap(ap(c_2EpatternMatches_2EPMATCH(A_27c,A_27a),V0v__old),ap(ap(c_2Elist_2ECONS(arr(A_27a,ty_2Eoption_2Eoption(A_27c))),V4r__old),V2rows__old)) = ap(ap(c_2EpatternMatches_2EPMATCH(A_27c,A_27b),V1v__new),V3rows__new))))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROW__REMOVE__FUN,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0ff:$i] : (mem(V0ff,arr(A_27a,A_27b)) => ( ! [V1v:$i] : (mem(V1v,A_27a) => ( ! [V2p:$i] : (mem(V2p,arr(A_27c,A_27a)) => ( ! [V3g:$i] : (mem(V3g,arr(A_27c,bool)) => ( ! [V4r:$i] : (mem(V4r,arr(A_27c,A_27d)) => (( ! [V5x:$i] : (mem(V5x,A_27a) => ( ! [V6y:$i] : (mem(V6y,A_27a) => ((ap(V0ff,V5x) = ap(V0ff,V6y)) => (V5x = V6y)))))) => (ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27d,A_27c,A_27b),f827(A_27b,A_27a,A_27c,V2p,V0ff)),V3g),V4r),ap(V0ff,V1v)) = ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27d,A_27c,A_27a),f828(A_27a,A_27c,V2p)),V3g),V4r),V1v))))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROW__EXTEND__INPUT,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [A_27e:del]: ( ! [A_27f:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1v_27:$i] : (mem(V1v_27,A_27b) => ( ! [V2f_27:$i] : (mem(V2f_27,arr(A_27b,A_27c)) => ( ! [V3f:$i] : (mem(V3f,arr(A_27d,A_27e)) => ( ! [V4p:$i] : (mem(V4p,arr(A_27e,A_27a)) => ( ! [V5g:$i] : (mem(V5g,arr(A_27c,arr(A_27e,bool))) => ( ! [V6r:$i] : (mem(V6r,arr(A_27c,arr(A_27e,A_27f))) => ( ! [V7p_27:$i] : (mem(V7p_27,arr(A_27d,A_27b)) => ((( ! [V8x_27:$i] : (mem(V8x_27,A_27d) => ((V1v_27 = ap(V7p_27,V8x_27)) => (ap(V4p,ap(V3f,V8x_27)) = V0v)))) & (( ! [V9x:$i] : (mem(V9x,A_27e) => ((V0v = ap(V4p,V9x)) => (? [V10x_27:$i] : (mem(V10x_27,A_27d) & (ap(V7p_27,V10x_27) = V1v_27)))))) & ( ! [V11x:$i] : (mem(V11x,A_27e) => ( ! [V12y:$i] : (mem(V12y,A_27e) => ((ap(V4p,V11x) = ap(V4p,V12y)) => (V11x = V12y)))))))) => (ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27f,A_27e,A_27a),V4p),ap(V5g,ap(V2f_27,V1v_27))),ap(V6r,ap(V2f_27,V1v_27))),V0v) = ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27f,A_27d,A_27b),V7p_27),f829(A_27c,A_27b,A_27e,A_27d,V5g,V7p_27,V2f_27,V3f)),f830(A_27b,A_27c,A_27f,A_27e,A_27d,V6r,V7p_27,V2f_27,V3f)),V1v_27))))))))))))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROW__REMOVE__FUN__VAR,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [A_27e:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1v_27:$i] : (mem(V1v_27,A_27b) => ( ! [V2f:$i] : (mem(V2f,arr(A_27c,A_27d)) => ( ! [V3p:$i] : (mem(V3p,arr(A_27d,A_27a)) => ( ! [V4g:$i] : (mem(V4g,arr(A_27d,bool)) => ( ! [V5r:$i] : (mem(V5r,arr(A_27d,A_27e)) => ( ! [V6p_27:$i] : (mem(V6p_27,arr(A_27c,A_27b)) => ((( ! [V7x_27:$i] : (mem(V7x_27,A_27c) => ((V1v_27 = ap(V6p_27,V7x_27)) <=> (ap(V3p,ap(V2f,V7x_27)) = V0v)))) & (( ! [V8x:$i] : (mem(V8x,A_27d) => ((V0v = ap(V3p,V8x)) => (? [V9x_27:$i] : (mem(V9x_27,A_27c) & (ap(V2f,V9x_27) = V8x)))))) & ( ! [V10x:$i] : (mem(V10x,A_27d) => ( ! [V11y:$i] : (mem(V11y,A_27d) => ((ap(V3p,V10x) = ap(V3p,V11y)) => (V10x = V11y)))))))) => (ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27e,A_27d,A_27a),V3p),V4g),V5r),V0v) = ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27e,A_27c,A_27b),V6p_27),f831(A_27c,A_27d,V2f,V4g)),f832(A_27e,A_27d,A_27c,V2f,V5r)),V1v_27)))))))))))))))))))))))).
tff(ax_thm_2EpatternMatches_2EPMATCH__EQUIV__ROWS__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rows1:$i] : (mem(V1rows1,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V2rows2:$i] : (mem(V2rows2,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__EQUIV__ROWS(A_27a,A_27b),V0v),V1rows1),V2rows2)) <=> ((ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27a),V0v),V1rows1) = ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27a),V0v),V2rows2)) & ((? [V3r:$i] : (mem(V3r,arr(A_27a,ty_2Eoption_2Eoption(A_27b))) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V3r),ap(c_2Elist_2ELIST__TO__SET(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1rows1))) & p(ap(c_2Eoption_2EIS__SOME(A_27b),ap(V3r,V0v)))))) <=> (? [V4r:$i] : (mem(V4r,arr(A_27a,ty_2Eoption_2Eoption(A_27b))) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V4r),ap(c_2Elist_2ELIST__TO__SET(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V2rows2))) & p(ap(c_2Eoption_2EIS__SOME(A_27b),ap(V4r,V0v)))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__EQUIV__ROWS__EQUIV__EXPAND,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rows1:$i] : (mem(V1rows1,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V2rows2:$i] : (mem(V2rows2,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__EQUIV__ROWS(A_27a,A_27b),V0v),V1rows1),V2rows2)) <=> (ap(ap(c_2EpatternMatches_2EPMATCH__EQUIV__ROWS(A_27a,A_27b),V0v),V1rows1) = ap(ap(c_2EpatternMatches_2EPMATCH__EQUIV__ROWS(A_27a,A_27b),V0v),V2rows2))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__EQUIV__ROWS__is__equiv__1,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rows:$i] : (mem(V1rows,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__EQUIV__ROWS(A_27a,A_27b),V0v),V1rows),V1rows)))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__EQUIV__ROWS__is__equiv__2,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rows1:$i] : (mem(V1rows1,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V2rows2:$i] : (mem(V2rows2,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__EQUIV__ROWS(A_27a,A_27b),V0v),V1rows1),V2rows2)) <=> p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__EQUIV__ROWS(A_27a,A_27b),V0v),V2rows2),V1rows1))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__EQUIV__ROWS__is__equiv__3,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rows1:$i] : (mem(V1rows1,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V2rows2:$i] : (mem(V2rows2,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V3rows3:$i] : (mem(V3rows3,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__EQUIV__ROWS(A_27a,A_27b),V0v),V1rows1),V2rows2)) => (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__EQUIV__ROWS(A_27a,A_27b),V0v),V2rows2),V3rows3)) => p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__EQUIV__ROWS(A_27a,A_27b),V0v),V1rows1),V3rows3)))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__EQUIV__ROWS__MATCH,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rows1:$i] : (mem(V1rows1,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V2rows2:$i] : (mem(V2rows2,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__EQUIV__ROWS(A_27a,A_27b),V0v),V1rows1),V2rows2)) => (ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27a),V0v),V1rows1) = ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27a),V0v),V2rows2))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__APPEND__SEM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rows1:$i] : (mem(V1rows1,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V2rows2:$i] : (mem(V2rows2,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => (ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27a),V0v),ap(ap(c_2Elist_2EAPPEND(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1rows1),V2rows2)) = ap(ap(ap(c_2Ebool_2ECOND(A_27b),ap(c_2Ebool_2E_3F(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),f833(A_27a,A_27b,V1rows1,V0v))),ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27a),V0v),V1rows1)),ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27a),V0v),V2rows2))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__EQUIV__APPEND,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rows1a:$i] : (mem(V1rows1a,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V2rows1b:$i] : (mem(V2rows1b,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V3rows2a:$i] : (mem(V3rows2a,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V4rows2b:$i] : (mem(V4rows2b,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__EQUIV__ROWS(A_27a,A_27b),V0v),V1rows1a),V2rows1b)) => (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__EQUIV__ROWS(A_27a,A_27b),V0v),V3rows2a),V4rows2b)) => p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__EQUIV__ROWS(A_27a,A_27b),V0v),ap(ap(c_2Elist_2EAPPEND(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1rows1a),V3rows2a)),ap(ap(c_2Elist_2EAPPEND(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V2rows1b),V4rows2b))))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__EQUIV__ROWS__CONS__NONE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0row:$i] : (mem(V0row,arr(A_27b,ty_2Eoption_2Eoption(A_27a))) => ( ! [V1v:$i] : (mem(V1v,A_27b) => ( ! [V2rows:$i] : (mem(V2rows,ty_2Elist_2Elist(arr(A_27b,ty_2Eoption_2Eoption(A_27a)))) => ((ap(V0row,V1v) = c_2Eoption_2ENONE(A_27a)) => (ap(ap(c_2EpatternMatches_2EPMATCH__EQUIV__ROWS(A_27b,A_27a),V1v),ap(ap(c_2Elist_2ECONS(arr(A_27b,ty_2Eoption_2Eoption(A_27a))),V0row),V2rows)) = ap(ap(c_2EpatternMatches_2EPMATCH__EQUIV__ROWS(A_27b,A_27a),V1v),V2rows))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROWS__DROP__REDUNDANT__TRIVIAL__SOUNDNESS__EQUIV,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rows:$i] : (mem(V1rows,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V2n:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2n)),ap(c_2Elist_2ELENGTH(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1rows))) & p(ap(c_2Eoption_2EIS__SOME(A_27b),ap(ap(ap(c_2Elist_2EEL(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),inj__ty_2Enum_2Enum(V2n)),V1rows),V0v)))) => p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__EQUIV__ROWS(A_27a,A_27b),V0v),V1rows),ap(ap(c_2Elist_2ETAKE(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2n))),V1rows))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROWS__DROP__REDUNDANT__TRIVIAL__SOUNDNESS,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rows:$i] : (mem(V1rows,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V2n:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2n)),ap(c_2Elist_2ELENGTH(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1rows))) & p(ap(c_2Eoption_2EIS__SOME(A_27b),ap(ap(ap(c_2Elist_2EEL(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),inj__ty_2Enum_2Enum(V2n)),V1rows),V0v)))) => (ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27a),V0v),V1rows) = ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27a),V0v),ap(ap(c_2Elist_2ETAKE(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2n))),V1rows))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROWS__DROP__REDUNDANT,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r1:$i] : (mem(V0r1,arr(A_27a,ty_2Eoption_2Eoption(A_27b))) => ( ! [V1r2:$i] : (mem(V1r2,arr(A_27a,ty_2Eoption_2Eoption(A_27b))) => ( ! [V2rows1:$i] : (mem(V2rows1,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V3rows2:$i] : (mem(V3rows2,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V4rows3:$i] : (mem(V4rows3,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V5v:$i] : (mem(V5v,A_27a) => ((p(ap(c_2Eoption_2EIS__SOME(A_27b),ap(V1r2,V5v))) => p(ap(c_2Eoption_2EIS__SOME(A_27b),ap(V0r1,V5v)))) => (ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27a),V5v),ap(ap(c_2Elist_2EAPPEND(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),ap(ap(c_2Elist_2EAPPEND(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V2rows1),ap(ap(c_2Elist_2ECONS(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V0r1),V3rows2))),ap(ap(c_2Elist_2ECONS(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1r2),V4rows3))) = ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27a),V5v),ap(ap(c_2Elist_2EAPPEND(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),ap(ap(c_2Elist_2EAPPEND(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V2rows1),ap(ap(c_2Elist_2ECONS(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V0r1),V3rows2))),V4rows3)))))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROWS__DROP__REDUNDANT__PMATCH__ROWS,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0p:$i] : (mem(V0p,arr(A_27a,A_27b)) => ( ! [V1g:$i] : (mem(V1g,arr(A_27a,bool)) => ( ! [V2r:$i] : (mem(V2r,arr(A_27a,A_27c)) => ( ! [V3p_27:$i] : (mem(V3p_27,arr(A_27d,A_27b)) => ( ! [V4g_27:$i] : (mem(V4g_27,arr(A_27d,bool)) => ( ! [V5r_27:$i] : (mem(V5r_27,arr(A_27d,A_27c)) => ( ! [V6rows1:$i] : (mem(V6rows1,ty_2Elist_2Elist(arr(A_27b,ty_2Eoption_2Eoption(A_27c)))) => ( ! [V7rows2:$i] : (mem(V7rows2,ty_2Elist_2Elist(arr(A_27b,ty_2Eoption_2Eoption(A_27c)))) => ( ! [V8rows3:$i] : (mem(V8rows3,ty_2Elist_2Elist(arr(A_27b,ty_2Eoption_2Eoption(A_27c)))) => ( ! [V9v:$i] : (mem(V9v,A_27b) => (( ! [V10x_27:$i] : (mem(V10x_27,A_27d) => (((V9v = ap(V3p_27,V10x_27)) & p(ap(V4g_27,V10x_27))) => (? [V11x:$i] : (mem(V11x,A_27a) & ((ap(V3p_27,V10x_27) = ap(V0p,V11x)) & p(ap(V1g,V11x)))))))) => (ap(ap(c_2EpatternMatches_2EPMATCH(A_27c,A_27b),V9v),ap(ap(c_2Elist_2EAPPEND(arr(A_27b,ty_2Eoption_2Eoption(A_27c))),ap(ap(c_2Elist_2EAPPEND(arr(A_27b,ty_2Eoption_2Eoption(A_27c))),V6rows1),ap(ap(c_2Elist_2ECONS(arr(A_27b,ty_2Eoption_2Eoption(A_27c))),ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27c,A_27a,A_27b),V0p),V1g),V2r)),V7rows2))),ap(ap(c_2Elist_2ECONS(arr(A_27b,ty_2Eoption_2Eoption(A_27c))),ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27c,A_27d,A_27b),V3p_27),V4g_27),V5r_27)),V8rows3))) = ap(ap(c_2EpatternMatches_2EPMATCH(A_27c,A_27b),V9v),ap(ap(c_2Elist_2EAPPEND(arr(A_27b,ty_2Eoption_2Eoption(A_27c))),ap(ap(c_2Elist_2EAPPEND(arr(A_27b,ty_2Eoption_2Eoption(A_27c))),V6rows1),ap(ap(c_2Elist_2ECONS(arr(A_27b,ty_2Eoption_2Eoption(A_27c))),ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27c,A_27a,A_27b),V0p),V1g),V2r)),V7rows2))),V8rows3)))))))))))))))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROWS__DROP__SUBSUMED,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r1:$i] : (mem(V0r1,arr(A_27a,ty_2Eoption_2Eoption(A_27b))) => ( ! [V1r2:$i] : (mem(V1r2,arr(A_27a,ty_2Eoption_2Eoption(A_27b))) => ( ! [V2rows1:$i] : (mem(V2rows1,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V3rows2:$i] : (mem(V3rows2,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V4rows3:$i] : (mem(V4rows3,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V5v:$i] : (mem(V5v,A_27a) => ((( ! [V6x:$i] : (mem(V6x,A_27b) => ((ap(V0r1,V5v) = ap(c_2Eoption_2ESOME(A_27b),V6x)) => (ap(V1r2,V5v) = ap(c_2Eoption_2ESOME(A_27b),V6x))))) & (p(ap(c_2Eoption_2EIS__SOME(A_27b),ap(V0r1,V5v))) => p(ap(ap(c_2Elist_2EEVERY(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),f834(A_27a,A_27b,V5v)),V3rows2)))) => (ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27a),V5v),ap(ap(c_2Elist_2EAPPEND(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V2rows1),ap(ap(c_2Elist_2ECONS(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V0r1),ap(ap(c_2Elist_2EAPPEND(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V3rows2),ap(ap(c_2Elist_2ECONS(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1r2),V4rows3))))) = ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27a),V5v),ap(ap(c_2Elist_2EAPPEND(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),ap(ap(c_2Elist_2EAPPEND(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V2rows1),V3rows2)),ap(ap(c_2Elist_2ECONS(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1r2),V4rows3))))))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROWS__DROP__SUBSUMED__PMATCH__ROWS,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0p:$i] : (mem(V0p,arr(A_27a,A_27b)) => ( ! [V1g:$i] : (mem(V1g,arr(A_27a,bool)) => ( ! [V2r:$i] : (mem(V2r,arr(A_27a,A_27c)) => ( ! [V3p_27:$i] : (mem(V3p_27,arr(A_27d,A_27b)) => ( ! [V4g_27:$i] : (mem(V4g_27,arr(A_27d,bool)) => ( ! [V5r_27:$i] : (mem(V5r_27,arr(A_27d,A_27c)) => ( ! [V6rows1:$i] : (mem(V6rows1,ty_2Elist_2Elist(arr(A_27b,ty_2Eoption_2Eoption(A_27c)))) => ( ! [V7rows2:$i] : (mem(V7rows2,ty_2Elist_2Elist(arr(A_27b,ty_2Eoption_2Eoption(A_27c)))) => ( ! [V8rows3:$i] : (mem(V8rows3,ty_2Elist_2Elist(arr(A_27b,ty_2Eoption_2Eoption(A_27c)))) => ( ! [V9v:$i] : (mem(V9v,A_27b) => ((( ! [V10x:$i] : (mem(V10x,A_27a) => (((V9v = ap(V0p,V10x)) & p(ap(V1g,V10x))) => (? [V11x_27:$i] : (mem(V11x_27,A_27d) & ((ap(V0p,V10x) = ap(V3p_27,V11x_27)) & p(ap(V4g_27,V11x_27)))))))) & (( ! [V12x:$i] : (mem(V12x,A_27a) => ( ! [V13x_27:$i] : (mem(V13x_27,A_27d) => (((V9v = ap(V0p,V12x)) & ((ap(V0p,V12x) = ap(V3p_27,V13x_27)) & (p(ap(V1g,V12x)) & p(ap(V4g_27,V13x_27))))) => (ap(V2r,V12x) = ap(V5r_27,V13x_27))))))) & ( ! [V14x:$i] : (mem(V14x,A_27a) => (((V9v = ap(V0p,V14x)) & p(ap(V1g,V14x))) => p(ap(ap(c_2Elist_2EEVERY(arr(A_27b,ty_2Eoption_2Eoption(A_27c))),f835(A_27b,A_27a,A_27c,V14x,V0p)),V7rows2))))))) => (ap(ap(c_2EpatternMatches_2EPMATCH(A_27c,A_27b),V9v),ap(ap(c_2Elist_2EAPPEND(arr(A_27b,ty_2Eoption_2Eoption(A_27c))),V6rows1),ap(ap(c_2Elist_2ECONS(arr(A_27b,ty_2Eoption_2Eoption(A_27c))),ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27c,A_27a,A_27b),V0p),V1g),V2r)),ap(ap(c_2Elist_2EAPPEND(arr(A_27b,ty_2Eoption_2Eoption(A_27c))),V7rows2),ap(ap(c_2Elist_2ECONS(arr(A_27b,ty_2Eoption_2Eoption(A_27c))),ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27c,A_27d,A_27b),V3p_27),V4g_27),V5r_27)),V8rows3))))) = ap(ap(c_2EpatternMatches_2EPMATCH(A_27c,A_27b),V9v),ap(ap(c_2Elist_2EAPPEND(arr(A_27b,ty_2Eoption_2Eoption(A_27c))),ap(ap(c_2Elist_2EAPPEND(arr(A_27b,ty_2Eoption_2Eoption(A_27c))),V6rows1),V7rows2)),ap(ap(c_2Elist_2ECONS(arr(A_27b,ty_2Eoption_2Eoption(A_27c))),ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27c,A_27d,A_27b),V3p_27),V4g_27),V5r_27)),V8rows3))))))))))))))))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__REMOVE__ARB,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0p:$i] : (mem(V0p,arr(A_27a,A_27b)) => ( ! [V1g:$i] : (mem(V1g,arr(A_27a,bool)) => ( ! [V2r:$i] : (mem(V2r,arr(A_27a,A_27c)) => ( ! [V3v:$i] : (mem(V3v,A_27b) => ( ! [V4rows:$i] : (mem(V4rows,ty_2Elist_2Elist(arr(A_27b,ty_2Eoption_2Eoption(A_27c)))) => (( ! [V5x:$i] : (mem(V5x,A_27a) => (ap(V2r,V5x) = c_2Ebool_2EARB(A_27c)))) => (ap(ap(c_2EpatternMatches_2EPMATCH(A_27c,A_27b),V3v),ap(ap(c_2Elist_2ESNOC(arr(A_27b,ty_2Eoption_2Eoption(A_27c))),ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27c,A_27a,A_27b),V0p),V1g),V2r)),V4rows)) = ap(ap(c_2EpatternMatches_2EPMATCH(A_27c,A_27b),V3v),V4rows)))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__INTRO__CATCHALL,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27b) => ( ! [V1rows:$i] : (mem(V1rows,ty_2Elist_2Elist(arr(A_27b,ty_2Eoption_2Eoption(A_27a)))) => (ap(ap(c_2EpatternMatches_2EPMATCH(A_27a,A_27b),V0v),V1rows) = ap(ap(c_2EpatternMatches_2EPMATCH(A_27a,A_27b),V0v),ap(ap(c_2Elist_2ESNOC(arr(A_27b,ty_2Eoption_2Eoption(A_27a))),ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27a,A_27b,A_27b),i(A_27b)),k(A_27b,c_2Ebool_2ET)),k(A_27b,c_2Ebool_2EARB(A_27a)))),V1rows))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__REMOVE__ARB__NO__OVERLAP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1p:$i] : (mem(V1p,arr(A_27b,A_27a)) => ( ! [V2g:$i] : (mem(V2g,arr(A_27b,bool)) => ( ! [V3r:$i] : (mem(V3r,arr(A_27b,A_27c)) => ( ! [V4rows1:$i] : (mem(V4rows1,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27c)))) => ( ! [V5rows2:$i] : (mem(V5rows2,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27c)))) => ((( ! [V6x:$i] : (mem(V6x,A_27b) => (ap(V3r,V6x) = c_2Ebool_2EARB(A_27c)))) & ( ! [V7x:$i] : (mem(V7x,A_27b) => (((V0v = ap(V1p,V7x)) & p(ap(V2g,V7x))) => p(ap(ap(c_2Elist_2EEVERY(arr(A_27a,ty_2Eoption_2Eoption(A_27c))),f836(A_27a,A_27b,A_27c,V7x,V1p)),V5rows2)))))) => (ap(ap(c_2EpatternMatches_2EPMATCH(A_27c,A_27a),V0v),ap(ap(c_2Elist_2EAPPEND(arr(A_27a,ty_2Eoption_2Eoption(A_27c))),V4rows1),ap(ap(c_2Elist_2ECONS(arr(A_27a,ty_2Eoption_2Eoption(A_27c))),ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27c,A_27b,A_27a),V1p),V2g),V3r)),V5rows2))) = ap(ap(c_2EpatternMatches_2EPMATCH(A_27c,A_27a),V0v),ap(ap(c_2Elist_2EAPPEND(arr(A_27a,ty_2Eoption_2Eoption(A_27c))),V4rows1),V5rows2))))))))))))))))))))).
tff(ax_thm_2EpatternMatches_2EPMATCH__ROW__REDUNDANT__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rs:$i] : (mem(V1rs,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V2i:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__REDUNDANT(A_27a,A_27b),V0v),V1rs),inj__ty_2Enum_2Enum(V2i))) <=> (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2i)),ap(c_2Elist_2ELENGTH(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1rs))) & (p(ap(c_2Eoption_2EIS__SOME(A_27b),ap(ap(ap(c_2Elist_2EEL(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),inj__ty_2Enum_2Enum(V2i)),V1rs),V0v))) => (? [V3j:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V3j)),inj__ty_2Enum_2Enum(V2i))) & p(ap(c_2Eoption_2EIS__SOME(A_27b),ap(ap(ap(c_2Elist_2EEL(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),inj__ty_2Enum_2Enum(V3j)),V1rs),V0v)))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROW__REDUNDANT__NIL,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1i:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__REDUNDANT(A_27a,A_27b),V0v),c_2Elist_2ENIL(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))),inj__ty_2Enum_2Enum(V1i))) <=> $false)))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROW__REDUNDANT__0,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1r:$i] : (mem(V1r,arr(A_27a,ty_2Eoption_2Eoption(A_27b))) => ( ! [V2rs:$i] : (mem(V2rs,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__REDUNDANT(A_27a,A_27b),V0v),ap(ap(c_2Elist_2ECONS(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1r),V2rs)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> (ap(V1r,V0v) = c_2Eoption_2ENONE(A_27b))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROW__REDUNDANT__SUC,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1r:$i] : (mem(V1r,arr(A_27a,ty_2Eoption_2Eoption(A_27b))) => ( ! [V2rs:$i] : (mem(V2rs,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V3i:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__REDUNDANT(A_27a,A_27b),V0v),ap(ap(c_2Elist_2ECONS(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1r),V2rs)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V3i)))) <=> (((~~ (ap(V1r,V0v) = c_2Eoption_2ENONE(A_27b))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V3i)),ap(c_2Elist_2ELENGTH(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V2rs)))) | p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__REDUNDANT(A_27a,A_27b),V0v),V2rs),inj__ty_2Enum_2Enum(V3i)))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROW__REDUNDANT__APPEND__LT,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rs1:$i] : (mem(V1rs1,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V2rs2:$i] : (mem(V2rs2,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V3i:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V3i)),ap(c_2Elist_2ELENGTH(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1rs1))) => (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__REDUNDANT(A_27a,A_27b),V0v),ap(ap(c_2Elist_2EAPPEND(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1rs1),V2rs2)),inj__ty_2Enum_2Enum(V3i))) <=> p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__REDUNDANT(A_27a,A_27b),V0v),V1rs1),inj__ty_2Enum_2Enum(V3i)))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROW__REDUNDANT__APPEND__GE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rs1:$i] : (mem(V1rs1,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V2rs2:$i] : (mem(V2rs2,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V3i:tp__ty_2Enum_2Enum] : ((~~ p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V3i)),ap(c_2Elist_2ELENGTH(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1rs1)))) => (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__REDUNDANT(A_27a,A_27b),V0v),ap(ap(c_2Elist_2EAPPEND(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1rs1),V2rs2)),inj__ty_2Enum_2Enum(V3i))) <=> (((~~ p(ap(ap(c_2Elist_2EEVERY(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),f837(A_27a,A_27b,V0v)),V1rs1))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V3i)),ap(ap(c_2Earithmetic_2E_2B,ap(c_2Elist_2ELENGTH(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1rs1)),ap(c_2Elist_2ELENGTH(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V2rs2))))) | p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__REDUNDANT(A_27a,A_27b),V0v),V2rs2),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V3i)),ap(c_2Elist_2ELENGTH(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1rs1)))))))))))))))))).
tff(ax_thm_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rows:$i] : (mem(V1rows,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V2c:tp__o] : ( ! [V3infos:tp__c_ty_2Elist_2Elist_o] : (p(ap(ap(ap(ap(c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO(A_27a,A_27b),V0v),V1rows),inj__o(V2c)),inj__c_ty_2Elist_2Elist_o(V3infos))) <=> ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1rows)) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(bool),inj__c_ty_2Elist_2Elist_o(V3infos)))) & (( ! [V4i:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V4i)),ap(c_2Elist_2ELENGTH(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1rows))) => (p(ap(ap(c_2Elist_2EEL(bool),inj__ty_2Enum_2Enum(V4i)),inj__c_ty_2Elist_2Elist_o(V3infos))) => p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__REDUNDANT(A_27a,A_27b),V0v),V1rows),inj__ty_2Enum_2Enum(V4i)))))) & (p(ap(ap(c_2Elist_2EEVERY(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),f838(A_27a,A_27b,V0v)),V1rows)) => p(inj__o(V2c))))))))))))))).
tff(conj_thm_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO__NIL,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => p(ap(ap(ap(ap(c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO(A_27a,A_27b),V0v),c_2Elist_2ENIL(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))),inj__o(fo__c_2Ebool_2ET)),c_2Elist_2ENIL(bool))))))))).
tff(conj_thm_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO__SNOC,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rows:$i] : (mem(V1rows,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V2c:tp__o] : ( ! [V3infos:tp__c_ty_2Elist_2Elist_o] : ( ! [V4r:$i] : (mem(V4r,arr(A_27a,ty_2Eoption_2Eoption(A_27b))) => ( ! [V5i:tp__o] : ( ! [V6c_27:tp__o] : (p(ap(ap(ap(ap(c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO(A_27a,A_27b),V0v),V1rows),inj__o(V2c)),inj__c_ty_2Elist_2Elist_o(V3infos))) => (((ap(V4r,V0v) = c_2Eoption_2ENONE(A_27b)) => (p(inj__o(V2c)) => p(inj__o(V6c_27)))) => ((p(inj__o(V2c)) => (p(inj__o(V5i)) => (ap(V4r,V0v) = c_2Eoption_2ENONE(A_27b)))) => p(ap(ap(ap(ap(c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO(A_27a,A_27b),V0v),ap(ap(c_2Elist_2ESNOC(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V4r),V1rows)),inj__o(V6c_27)),ap(ap(c_2Elist_2ESNOC(bool),inj__o(V5i)),inj__c_ty_2Elist_2Elist_o(V3infos))))))))))))))))))))).
tff(ax_thm_2EpatternMatches_2EPMATCH__ROW__COND__EX__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,A_27a) => ( ! [V1p:$i] : (mem(V1p,arr(A_27b,A_27a)) => ( ! [V2g:$i] : (mem(V2g,arr(A_27b,bool)) => (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND__EX(A_27a,A_27b),V0i),V1p),V2g)) <=> (? [V3x:$i] : (mem(V3x,A_27b) & p(ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND(A_27b,A_27a),V1p),V2g),V0i),V3x)))))))))))))).
tff(conj_thm_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO__SNOC__PMATCH__ROW,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rows:$i] : (mem(V1rows,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V2c:tp__o] : ( ! [V3infos:tp__c_ty_2Elist_2Elist_o] : ( ! [V4p:$i] : (mem(V4p,arr(A_27c,A_27a)) => ( ! [V5g:$i] : (mem(V5g,arr(A_27c,bool)) => ( ! [V6r:$i] : (mem(V6r,arr(A_27c,A_27b)) => ( ! [V7c_27:tp__o] : (p(ap(ap(ap(ap(c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO(A_27a,A_27b),V0v),V1rows),inj__o(V2c)),inj__c_ty_2Elist_2Elist_o(V3infos))) => (((~~ p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND__EX(A_27a,A_27c),V0v),V4p),V5g))) => (p(inj__o(V2c)) <=> p(inj__o(V7c_27)))) => p(ap(ap(ap(ap(c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO(A_27a,A_27b),V0v),ap(ap(c_2Elist_2ESNOC(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27b,A_27c,A_27a),V4p),V5g),V6r)),V1rows)),inj__o(V7c_27)),ap(ap(c_2Elist_2ESNOC(bool),ap(ap(c_2Emin_2E_3D_3D_3E,inj__o(V2c)),ap(c_2Ebool_2E_7E,ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND__EX(A_27a,A_27c),V0v),V4p),V5g)))),inj__c_ty_2Elist_2Elist_o(V3infos)))))))))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO__CONS,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1row:$i] : (mem(V1row,arr(A_27a,ty_2Eoption_2Eoption(A_27b))) => ( ! [V2rows:$i] : (mem(V2rows,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V3c:tp__o] : ( ! [V4i:tp__o] : ( ! [V5infos_27:tp__c_ty_2Elist_2Elist_o] : (p(ap(ap(ap(ap(c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO(A_27a,A_27b),V0v),ap(ap(c_2Elist_2ECONS(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1row),V2rows)),inj__o(V3c)),ap(ap(c_2Elist_2ECONS(bool),inj__o(V4i)),inj__c_ty_2Elist_2Elist_o(V5infos_27)))) <=> ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V2rows)) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(bool),inj__c_ty_2Elist_2Elist_o(V5infos_27)))) & ((p(inj__o(V4i)) => (ap(V1row,V0v) = c_2Eoption_2ENONE(A_27b))) & ((ap(V1row,V0v) = c_2Eoption_2ENONE(A_27b)) => p(ap(ap(ap(ap(c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO(A_27a,A_27b),V0v),V2rows),inj__o(V3c)),inj__c_ty_2Elist_2Elist_o(V5infos_27)))))))))))))))))))).
tff(ax_thm_2EpatternMatches_2EAPPLY__REDUNDANT__ROWS__INFO__def,axiom,( ! [A_27a:del]: ( ! [V0is:tp__c_ty_2Elist_2Elist_o] : ( ! [V1xs:$i] : (mem(V1xs,ty_2Elist_2Elist(A_27a)) => (ap(ap(c_2EpatternMatches_2EAPPLY__REDUNDANT__ROWS__INFO(A_27a),inj__c_ty_2Elist_2Elist_o(V0is)),V1xs) = ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(bool,A_27a),A_27a),c_2Epair_2ESND(bool,A_27a)),ap(ap(c_2Elist_2EFILTER(ty_2Epair_2Eprod(bool,A_27a)),f839(A_27a)),ap(c_2Elist_2EZIP(bool,A_27a),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(bool),ty_2Elist_2Elist(A_27a)),inj__c_ty_2Elist_2Elist_o(V0is)),V1xs)))))))))).
tff(conj_thm_2EpatternMatches_2EAPPLY__REDUNDANT__ROWS__INFO__THMS,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ((ap(ap(c_2EpatternMatches_2EAPPLY__REDUNDANT__ROWS__INFO(A_27a),c_2Elist_2ENIL(bool)),c_2Elist_2ENIL(A_27a)) = c_2Elist_2ENIL(A_27a)) & (( ! [V0is:tp__c_ty_2Elist_2Elist_o] : ( ! [V1x:$i] : (mem(V1x,A_27b) => ( ! [V2xs:$i] : (mem(V2xs,ty_2Elist_2Elist(A_27b)) => (ap(ap(c_2EpatternMatches_2EAPPLY__REDUNDANT__ROWS__INFO(A_27b),ap(ap(c_2Elist_2ECONS(bool),inj__o(fo__c_2Ebool_2ET)),inj__c_ty_2Elist_2Elist_o(V0is))),ap(ap(c_2Elist_2ECONS(A_27b),V1x),V2xs)) = ap(ap(c_2EpatternMatches_2EAPPLY__REDUNDANT__ROWS__INFO(A_27b),inj__c_ty_2Elist_2Elist_o(V0is)),V2xs))))))) & ( ! [V3is:tp__c_ty_2Elist_2Elist_o] : ( ! [V4x:$i] : (mem(V4x,A_27c) => ( ! [V5xs:$i] : (mem(V5xs,ty_2Elist_2Elist(A_27c)) => (ap(ap(c_2EpatternMatches_2EAPPLY__REDUNDANT__ROWS__INFO(A_27c),ap(ap(c_2Elist_2ECONS(bool),inj__o(fo__c_2Ebool_2EF)),inj__c_ty_2Elist_2Elist_o(V3is))),ap(ap(c_2Elist_2ECONS(A_27c),V4x),V5xs)) = ap(ap(c_2Elist_2ECONS(A_27c),V4x),ap(ap(c_2EpatternMatches_2EAPPLY__REDUNDANT__ROWS__INFO(A_27c),inj__c_ty_2Elist_2Elist_o(V3is)),V5xs))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROWS__DROP__REDUNDANT__ROWS__INFO__EQUIV,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1c:tp__o] : ( ! [V2rows:$i] : (mem(V2rows,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V3infos:tp__c_ty_2Elist_2Elist_o] : (p(ap(ap(ap(ap(c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO(A_27a,A_27b),V0v),V2rows),inj__o(V1c)),inj__c_ty_2Elist_2Elist_o(V3infos))) => p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__EQUIV__ROWS(A_27a,A_27b),V0v),V2rows),ap(ap(c_2EpatternMatches_2EAPPLY__REDUNDANT__ROWS__INFO(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),inj__c_ty_2Elist_2Elist_o(V3infos)),V2rows)))))))))))))).
tff(conj_thm_2EpatternMatches_2EREDUNDANT__ROWS__INFO__TO__PMATCH__EQ,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1c:tp__o] : ( ! [V2rows:$i] : (mem(V2rows,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V3infos:tp__c_ty_2Elist_2Elist_o] : (p(ap(ap(ap(ap(c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO(A_27a,A_27b),V0v),V2rows),inj__o(V1c)),inj__c_ty_2Elist_2Elist_o(V3infos))) => (ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27a),V0v),V2rows) = ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27a),V0v),ap(ap(c_2EpatternMatches_2EAPPLY__REDUNDANT__ROWS__INFO(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),inj__c_ty_2Elist_2Elist_o(V3infos)),V2rows)))))))))))))).
tff(ax_thm_2EpatternMatches_2EPMATCH__IS__EXHAUSTIVE__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rs:$i] : (mem(V1rs,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => (p(ap(ap(c_2EpatternMatches_2EPMATCH__IS__EXHAUSTIVE(A_27a,A_27b),V0v),V1rs)) <=> p(ap(ap(c_2Elist_2EEXISTS(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),f840(A_27a,A_27b,V0v)),V1rs)))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__IS__EXHAUSTIVE__REWRITES,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: (( ! [V0v:$i] : (mem(V0v,A_27a) => (p(ap(ap(c_2EpatternMatches_2EPMATCH__IS__EXHAUSTIVE(A_27a,A_27b),V0v),c_2Elist_2ENIL(arr(A_27a,ty_2Eoption_2Eoption(A_27b))))) <=> $false))) & ( ! [V1v:$i] : (mem(V1v,A_27c) => ( ! [V2r:$i] : (mem(V2r,arr(A_27c,ty_2Eoption_2Eoption(A_27d))) => ( ! [V3rs:$i] : (mem(V3rs,ty_2Elist_2Elist(arr(A_27c,ty_2Eoption_2Eoption(A_27d)))) => (p(ap(ap(c_2EpatternMatches_2EPMATCH__IS__EXHAUSTIVE(A_27c,A_27d),V1v),ap(ap(c_2Elist_2ECONS(arr(A_27c,ty_2Eoption_2Eoption(A_27d))),V2r),V3rs))) <=> ((~~ (ap(V2r,V1v) = c_2Eoption_2ENONE(A_27d))) | p(ap(ap(c_2EpatternMatches_2EPMATCH__IS__EXHAUSTIVE(A_27c,A_27d),V1v),V3rs))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO__EXTRACT__IS__EXHAUSTIVE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rows:$i] : (mem(V1rows,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V2c:tp__o] : ( ! [V3infos:tp__c_ty_2Elist_2Elist_o] : (p(ap(ap(ap(ap(c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO(A_27a,A_27b),V0v),V1rows),inj__o(V2c)),inj__c_ty_2Elist_2Elist_o(V3infos))) => ((~~ p(inj__o(V2c))) => p(ap(ap(c_2EpatternMatches_2EPMATCH__IS__EXHAUSTIVE(A_27a,A_27b),V0v),V1rows)))))))))))))).
tff(ax_thm_2EpatternMatches_2EREDUNDANT__ROWS__INFOS__CONJ__def,axiom,( ! [V0ip1:tp__c_ty_2Elist_2Elist_o] : ( ! [V1ip2:tp__c_ty_2Elist_2Elist_o] : (surj__c_ty_2Elist_2Elist_o(ap(ap(c_2EpatternMatches_2EREDUNDANT__ROWS__INFOS__CONJ,inj__c_ty_2Elist_2Elist_o(V0ip1)),inj__c_ty_2Elist_2Elist_o(V1ip2))) = surj__c_ty_2Elist_2Elist_o(ap(ap(ap(c_2Elist_2EMAP2(bool,bool,bool),f842),inj__c_ty_2Elist_2Elist_o(V0ip1)),inj__c_ty_2Elist_2Elist_o(V1ip2))))))).
tff(conj_thm_2EpatternMatches_2EREDUNDANT__ROWS__INFOS__CONJ__REWRITE,lemma,(( ! [V0i1:tp__o] : ( ! [V1is1:tp__c_ty_2Elist_2Elist_o] : ( ! [V2i2:tp__o] : ( ! [V3is2:tp__c_ty_2Elist_2Elist_o] : ((surj__c_ty_2Elist_2Elist_o(ap(ap(c_2EpatternMatches_2EREDUNDANT__ROWS__INFOS__CONJ,c_2Elist_2ENIL(bool)),c_2Elist_2ENIL(bool))) = surj__c_ty_2Elist_2Elist_o(c_2Elist_2ENIL(bool))) & (surj__c_ty_2Elist_2Elist_o(ap(ap(c_2EpatternMatches_2EREDUNDANT__ROWS__INFOS__CONJ,ap(ap(c_2Elist_2ECONS(bool),inj__o(V0i1)),inj__c_ty_2Elist_2Elist_o(V1is1))),ap(ap(c_2Elist_2ECONS(bool),inj__o(V2i2)),inj__c_ty_2Elist_2Elist_o(V3is2)))) = surj__c_ty_2Elist_2Elist_o(ap(ap(c_2Elist_2ECONS(bool),ap(ap(c_2Ebool_2E_2F_5C,inj__o(V0i1)),inj__o(V2i2))),ap(ap(c_2EpatternMatches_2EREDUNDANT__ROWS__INFOS__CONJ,inj__c_ty_2Elist_2Elist_o(V1is1)),inj__c_ty_2Elist_2Elist_o(V3is2)))))))))))).
tff(conj_thm_2EpatternMatches_2EREDUNDANT__ROWS__INFOS__CONJ__THM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rows:$i] : (mem(V1rows,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V2c:tp__o] : ( ! [V3infos:tp__c_ty_2Elist_2Elist_o] : ( ! [V4c_27:tp__o] : ( ! [V5infos_27:tp__c_ty_2Elist_2Elist_o] : (p(ap(ap(ap(ap(c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO(A_27a,A_27b),V0v),V1rows),inj__o(V2c)),inj__c_ty_2Elist_2Elist_o(V3infos))) => ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(bool),inj__c_ty_2Elist_2Elist_o(V5infos_27))) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(bool),inj__c_ty_2Elist_2Elist_o(V3infos)))) => p(ap(ap(ap(ap(c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO(A_27a,A_27b),V0v),V1rows),ap(ap(c_2Ebool_2E_5C_2F,inj__o(V2c)),inj__o(V4c_27))),ap(ap(c_2EpatternMatches_2EREDUNDANT__ROWS__INFOS__CONJ,inj__c_ty_2Elist_2Elist_o(V3infos)),inj__c_ty_2Elist_2Elist_o(V5infos_27)))))))))))))))))).
tff(ax_thm_2EpatternMatches_2EREDUNDANT__ROWS__INFOS__DISJ__def,axiom,( ! [V0ip1:tp__c_ty_2Elist_2Elist_o] : ( ! [V1ip2:tp__c_ty_2Elist_2Elist_o] : (surj__c_ty_2Elist_2Elist_o(ap(ap(c_2EpatternMatches_2EREDUNDANT__ROWS__INFOS__DISJ,inj__c_ty_2Elist_2Elist_o(V0ip1)),inj__c_ty_2Elist_2Elist_o(V1ip2))) = surj__c_ty_2Elist_2Elist_o(ap(ap(ap(c_2Elist_2EMAP2(bool,bool,bool),f844),inj__c_ty_2Elist_2Elist_o(V0ip1)),inj__c_ty_2Elist_2Elist_o(V1ip2))))))).
tff(conj_thm_2EpatternMatches_2EREDUNDANT__ROWS__INFOS__DISJ__THM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rows:$i] : (mem(V1rows,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V2c:tp__o] : ( ! [V3infos:tp__c_ty_2Elist_2Elist_o] : ( ! [V4c_27:tp__o] : ( ! [V5infos_27:tp__c_ty_2Elist_2Elist_o] : (p(ap(ap(ap(ap(c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO(A_27a,A_27b),V0v),V1rows),inj__o(V2c)),inj__c_ty_2Elist_2Elist_o(V3infos))) => (p(ap(ap(ap(ap(c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO(A_27a,A_27b),V0v),V1rows),inj__o(V4c_27)),inj__c_ty_2Elist_2Elist_o(V5infos_27))) => p(ap(ap(ap(ap(c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO(A_27a,A_27b),V0v),V1rows),ap(ap(c_2Ebool_2E_2F_5C,inj__o(V2c)),inj__o(V4c_27))),ap(ap(c_2EpatternMatches_2EREDUNDANT__ROWS__INFOS__DISJ,inj__c_ty_2Elist_2Elist_o(V3infos)),inj__c_ty_2Elist_2Elist_o(V5infos_27)))))))))))))))))).
tff(ax_thm_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO__AUX__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1p:tp__o] : ( ! [V2infos:tp__c_ty_2Elist_2Elist_o] : (surj__c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o(ap(ap(ap(ap(c_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO__AUX(A_27a,A_27b),V0v),c_2Elist_2ENIL(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))),inj__o(V1p)),inj__c_ty_2Elist_2Elist_o(V2infos))) = surj__c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o(ap(ap(c_2Epair_2E_2C(bool,ty_2Elist_2Elist(bool)),inj__o(V1p)),inj__c_ty_2Elist_2Elist_o(V2infos)))))))) & ( ! [V3v:$i] : (mem(V3v,A_27a) => ( ! [V4r:$i] : (mem(V4r,arr(A_27a,ty_2Eoption_2Eoption(A_27b))) => ( ! [V5rows:$i] : (mem(V5rows,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V6p:tp__o] : ( ! [V7infos:tp__c_ty_2Elist_2Elist_o] : (surj__c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o(ap(ap(ap(ap(c_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO__AUX(A_27a,A_27b),V3v),ap(ap(c_2Elist_2ECONS(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V4r),V5rows)),inj__o(V6p)),inj__c_ty_2Elist_2Elist_o(V7infos))) = surj__c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o(ap(ap(ap(ap(c_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO__AUX(A_27a,A_27b),V3v),V5rows),ap(ap(c_2Ebool_2E_2F_5C,inj__o(V6p)),ap(ap(c_2Emin_2E_3D(ty_2Eoption_2Eoption(A_27b)),ap(V4r,V3v)),c_2Eoption_2ENONE(A_27b)))),ap(ap(c_2Elist_2ESNOC(bool),ap(ap(c_2Emin_2E_3D_3D_3E,inj__o(V6p)),ap(ap(c_2Emin_2E_3D(ty_2Eoption_2Eoption(A_27b)),ap(V4r,V3v)),c_2Eoption_2ENONE(A_27b)))),inj__c_ty_2Elist_2Elist_o(V7infos))))))))))))))))).
tff(ax_thm_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rows:$i] : (mem(V1rows,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => (surj__c_ty_2Elist_2Elist_o(ap(ap(c_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO(A_27a,A_27b),V0v),V1rows)) = surj__c_ty_2Elist_2Elist_o(ap(c_2Epair_2ESND(bool,ty_2Elist_2Elist(bool)),ap(ap(ap(ap(c_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO__AUX(A_27a,A_27b),V0v),V1rows),inj__o(fo__c_2Ebool_2ET)),c_2Elist_2ENIL(bool)))))))))))).
tff(conj_thm_2EpatternMatches_2ELENGTH__STRONGEST__REDUNDANT__ROWS__INFO__AUX,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rows:$i] : (mem(V1rows,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V2p:tp__o] : ( ! [V3infos:tp__c_ty_2Elist_2Elist_o] : (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(bool),ap(c_2Epair_2ESND(bool,ty_2Elist_2Elist(bool)),ap(ap(ap(ap(c_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO__AUX(A_27a,A_27b),V0v),V1rows),inj__o(V2p)),inj__c_ty_2Elist_2Elist_o(V3infos))))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Elist_2ELENGTH(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1rows)),ap(c_2Elist_2ELENGTH(bool),inj__c_ty_2Elist_2Elist_o(V3infos))))))))))))))).
tff(conj_thm_2EpatternMatches_2EEL1__STRONGEST__REDUNDANT__ROWS__INFO__AUX,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rows:$i] : (mem(V1rows,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V2p:tp__o] : ( ! [V3infos:tp__c_ty_2Elist_2Elist_o] : ( ! [V4i:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V4i)),ap(c_2Elist_2ELENGTH(bool),inj__c_ty_2Elist_2Elist_o(V3infos)))) => (p(ap(ap(c_2Elist_2EEL(bool),inj__ty_2Enum_2Enum(V4i)),ap(c_2Epair_2ESND(bool,ty_2Elist_2Elist(bool)),ap(ap(ap(ap(c_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO__AUX(A_27a,A_27b),V0v),V1rows),inj__o(V2p)),inj__c_ty_2Elist_2Elist_o(V3infos))))) <=> p(ap(ap(c_2Elist_2EEL(bool),inj__ty_2Enum_2Enum(V4i)),inj__c_ty_2Elist_2Elist_o(V3infos)))))))))))))))).
tff(conj_thm_2EpatternMatches_2EEL2__STRONGEST__REDUNDANT__ROWS__INFO__AUX,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rows:$i] : (mem(V1rows,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V2p:tp__o] : ( ! [V3infos:tp__c_ty_2Elist_2Elist_o] : ( ! [V4i:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3E_3D,inj__ty_2Enum_2Enum(V4i)),ap(c_2Elist_2ELENGTH(bool),inj__c_ty_2Elist_2Elist_o(V3infos)))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V4i)),ap(ap(c_2Earithmetic_2E_2B,ap(c_2Elist_2ELENGTH(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1rows)),ap(c_2Elist_2ELENGTH(bool),inj__c_ty_2Elist_2Elist_o(V3infos)))))) => (p(ap(ap(c_2Elist_2EEL(bool),inj__ty_2Enum_2Enum(V4i)),ap(c_2Epair_2ESND(bool,ty_2Elist_2Elist(bool)),ap(ap(ap(ap(c_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO__AUX(A_27a,A_27b),V0v),V1rows),inj__o(V2p)),inj__c_ty_2Elist_2Elist_o(V3infos))))) <=> ((p(inj__o(V2p)) & p(ap(ap(c_2Elist_2EEVERY(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),f838(A_27a,A_27b,V0v)),ap(ap(c_2Elist_2ETAKE(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V4i)),ap(c_2Elist_2ELENGTH(bool),inj__c_ty_2Elist_2Elist_o(V3infos)))),V1rows)))) => (ap(ap(ap(c_2Elist_2EEL(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V4i)),ap(c_2Elist_2ELENGTH(bool),inj__c_ty_2Elist_2Elist_o(V3infos)))),V1rows),V0v) = c_2Eoption_2ENONE(A_27b)))))))))))))))).
tff(conj_thm_2EpatternMatches_2ELENGTH__STRONGEST__REDUNDANT__ROWS__INFO,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rows:$i] : (mem(V1rows,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(bool),ap(ap(c_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO(A_27a,A_27b),V0v),V1rows))) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1rows))))))))))).
tff(conj_thm_2EpatternMatches_2EFST__STRONGEST__REDUNDANT__ROWS__INFO__AUX,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rows:$i] : (mem(V1rows,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V2p:tp__o] : ( ! [V3infos:tp__c_ty_2Elist_2Elist_o] : (p(ap(c_2Epair_2EFST(bool,ty_2Elist_2Elist(bool)),ap(ap(ap(ap(c_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO__AUX(A_27a,A_27b),V0v),V1rows),inj__o(V2p)),inj__c_ty_2Elist_2Elist_o(V3infos)))) <=> (p(inj__o(V2p)) & p(ap(ap(c_2Elist_2EEVERY(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),f837(A_27a,A_27b,V0v)),V1rows)))))))))))))).
tff(conj_thm_2EpatternMatches_2EEL__STRONGEST__REDUNDANT__ROWS__INFO,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rows:$i] : (mem(V1rows,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V2i:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2i)),ap(c_2Elist_2ELENGTH(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1rows))) => (p(ap(ap(c_2Elist_2EEL(bool),inj__ty_2Enum_2Enum(V2i)),ap(ap(c_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO(A_27a,A_27b),V0v),V1rows))) <=> (p(ap(ap(c_2Elist_2EEVERY(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),f845(A_27a,A_27b,V0v)),ap(ap(c_2Elist_2ETAKE(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),inj__ty_2Enum_2Enum(V2i)),V1rows))) => (ap(ap(ap(c_2Elist_2EEL(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),inj__ty_2Enum_2Enum(V2i)),V1rows),V0v) = c_2Eoption_2ENONE(A_27b)))))))))))))).
tff(conj_thm_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO__OK,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rows:$i] : (mem(V1rows,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => p(ap(ap(ap(ap(c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO(A_27a,A_27b),V0v),V1rows),ap(ap(c_2Elist_2EEVERY(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),f846(A_27a,A_27b,V0v)),V1rows)),ap(ap(c_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO(A_27a,A_27b),V0v),V1rows))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROW__COND__EX__FULL__DEF,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,A_27a) => ( ! [V1p:$i] : (mem(V1p,arr(A_27b,A_27a)) => ( ! [V2g:$i] : (mem(V2g,arr(A_27b,bool)) => (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND__EX(A_27a,A_27b),V0i),V1p),V2g)) <=> (? [V3x:$i] : (mem(V3x,A_27b) & ((V0i = ap(V1p,V3x)) & p(ap(V2g,V3x)))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROW__COND__EX__WEAKEN,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1v:$i] : (mem(V1v,A_27c) => ( ! [V2p:$i] : (mem(V2p,arr(A_27b,A_27c)) => ( ! [V3g:$i] : (mem(V3g,arr(A_27b,bool)) => ( ! [V4p_27:$i] : (mem(V4p_27,arr(A_27a,A_27c)) => ( ! [V5g_27:$i] : (mem(V5g_27,arr(A_27a,bool)) => ((~~ p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND__EX(A_27c,A_27b),V1v),V2p),V3g))) => (( ! [V6x:$i] : (mem(V6x,A_27a) => (ap(V4p_27,V6x) = ap(V2p,ap(V0f,V6x))))) => (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND__EX(A_27c,A_27a),V1v),V4p_27),V5g_27)) <=> p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND__EX(A_27c,A_27a),V1v),V4p_27),f847(A_27b,A_27a,V0f,V3g,V5g_27))))))))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROW__COND__EX__FALSE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1p:$i] : (mem(V1p,arr(A_27b,A_27a)) => ( ! [V2g:$i] : (mem(V2g,arr(A_27b,bool)) => (( ! [V3x:$i] : (mem(V3x,A_27b) => (~~ p(ap(V2g,V3x))))) => (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND__EX(A_27a,A_27b),V0v),V1p),V2g)) <=> $false)))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROW__COND__EX__IMP__REWRITE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1p:$i] : (mem(V1p,arr(A_27b,A_27a)) => ( ! [V2g:$i] : (mem(V2g,arr(A_27b,bool)) => ( ! [V3p_27:$i] : (mem(V3p_27,arr(A_27c,A_27a)) => ( ! [V4g_27:$i] : (mem(V4g_27,arr(A_27c,bool)) => ( ! [V5RES:tp__o] : (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND__EX(A_27a,A_27b),V0v),V1p),V2g)) => (( ! [V6x:$i] : (mem(V6x,A_27b) => (p(ap(V2g,V6x)) => ((? [V7x_27:$i] : (mem(V7x_27,A_27c) & ((ap(V3p_27,V7x_27) = ap(V1p,V6x)) & p(ap(V4g_27,V7x_27))))) <=> p(inj__o(V5RES)))))) => (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND__EX(A_27a,A_27c),V0v),V3p_27),V4g_27)) <=> p(inj__o(V5RES))))))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__IS__EXHAUSTIVE__CONTRADICT,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rs:$i] : (mem(V1rs,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ((p(ap(ap(c_2Elist_2EEVERY(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),f846(A_27a,A_27b,V0v)),V1rs)) => $false) => p(ap(ap(c_2EpatternMatches_2EPMATCH__IS__EXHAUSTIVE(A_27a,A_27b),V0v),V1rs))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROW__EVAL__COND__EX,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0i:$i] : (mem(V0i,A_27a) => ( ! [V1p:$i] : (mem(V1p,arr(A_27b,A_27a)) => ( ! [V2g:$i] : (mem(V2g,arr(A_27b,bool)) => ( ! [V3r:$i] : (mem(V3r,arr(A_27b,A_27c)) => (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND__EX(A_27a,A_27b),V0i),V1p),V2g)) => (ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27c,A_27b,A_27a),V1p),V2g),V3r),V0i) = ap(c_2Eoption_2ESOME(A_27c),ap(V3r,ap(c_2Emin_2E_40(A_27b),f848(A_27a,A_27b,V0i,V1p,V2g))))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROW__NEQ__NONE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0p:$i] : (mem(V0p,arr(A_27b,A_27c)) => ( ! [V1g:$i] : (mem(V1g,arr(A_27b,bool)) => ( ! [V2r:$i] : (mem(V2r,arr(A_27b,A_27a)) => ( ! [V3i:$i] : (mem(V3i,A_27c) => ((~~ (ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27a,A_27b,A_27c),V0p),V1g),V2r),V3i) = c_2Eoption_2ENONE(A_27a))) <=> p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND__EX(A_27c,A_27b),V3i),V0p),V1g)))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROW__REMOVE__DOUBLE__BINDS__THM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0g:$i] : (mem(V0g,arr(A_27a,A_27b)) => ( ! [V1p1:$i] : (mem(V1p1,arr(A_27a,A_27c)) => ( ! [V2g1:$i] : (mem(V2g1,arr(A_27a,bool)) => ( ! [V3r1:$i] : (mem(V3r1,arr(A_27a,A_27d)) => ( ! [V4p2:$i] : (mem(V4p2,arr(A_27b,A_27c)) => ( ! [V5g2:$i] : (mem(V5g2,arr(A_27b,bool)) => ( ! [V6r2:$i] : (mem(V6r2,arr(A_27b,A_27d)) => ((( ! [V7x:$i] : (mem(V7x,A_27a) => ( ! [V8y:$i] : (mem(V8y,A_27a) => ((ap(V1p1,V7x) = ap(V1p1,V8y)) => (V7x = V8y)))))) & (( ! [V9x:$i] : (mem(V9x,A_27a) => (ap(V4p2,ap(V0g,V9x)) = ap(V1p1,V9x)))) & (( ! [V10x_27:$i] : (mem(V10x_27,A_27b) => (p(ap(V5g2,V10x_27)) <=> (? [V11x:$i] : (mem(V11x,A_27a) & ((V10x_27 = ap(V0g,V11x)) & p(ap(V2g1,V11x)))))))) & ( ! [V12x:$i] : (mem(V12x,A_27a) => (ap(V6r2,ap(V0g,V12x)) = ap(V3r1,V12x))))))) => (ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27d,A_27a,A_27c),V1p1),V2g1),V3r1) = ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27d,A_27b,A_27c),V4p2),V5g2),V6r2))))))))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EGUARDS__ELIM__THM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1rs1:$i] : (mem(V1rs1,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V2rs2:$i] : (mem(V2rs2,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V3p:$i] : (mem(V3p,arr(A_27c,A_27a)) => ( ! [V4g:$i] : (mem(V4g,arr(A_27c,bool)) => ( ! [V5r:$i] : (mem(V5r,arr(A_27c,A_27b)) => (( ! [V6x1:$i] : (mem(V6x1,A_27c) => ( ! [V7x2:$i] : (mem(V7x2,A_27c) => ((ap(V3p,V6x1) = ap(V3p,V7x2)) => (V6x1 = V7x2)))))) => (ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27a),V0v),ap(ap(c_2Elist_2EAPPEND(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1rs1),ap(ap(c_2Elist_2ECONS(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27b,A_27c,A_27a),V3p),V4g),V5r)),V2rs2))) = ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27a),V0v),ap(ap(c_2Elist_2EAPPEND(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1rs1),ap(ap(c_2Elist_2ECONS(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27b,A_27c,A_27a),V3p),k(A_27c,c_2Ebool_2ET)),f849(A_27a,A_27b,A_27c,V5r,V4g,V3p,V2rs2))),V2rs2)))))))))))))))))))))).
tff(ax_thm_2EpatternMatches_2EPMATCH__FLATTEN__FUN__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0p:$i] : (mem(V0p,arr(A_27b,A_27c)) => ( ! [V1g:$i] : (mem(V1g,arr(A_27b,bool)) => ( ! [V2row:$i] : (mem(V2row,arr(A_27b,arr(A_27b,ty_2Eoption_2Eoption(A_27a)))) => ( ! [V3v:$i] : (mem(V3v,A_27c) => (ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__FLATTEN__FUN(A_27a,A_27b,A_27c),V0p),V1g),V2row),V3v) = ap(ap(ap(c_2Eoption_2Eoption__CASE(A_27b,ty_2Eoption_2Eoption(A_27a)),ap(c_2Eoption_2Esome(A_27b),f850(A_27c,A_27b,V3v,V0p,V1g))),c_2Eoption_2ENONE(A_27a)),f851(A_27a,A_27b,V2row))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__FLATTEN__THM__SINGLE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1p:$i] : (mem(V1p,arr(A_27b,A_27a)) => ( ! [V2g:$i] : (mem(V2g,arr(A_27b,bool)) => ( ! [V3rows:$i] : (mem(V3rows,ty_2Elist_2Elist(arr(A_27b,arr(A_27b,ty_2Eoption_2Eoption(A_27c))))) => (( ! [V4x:$i] : (mem(V4x,A_27b) => p(ap(ap(c_2EpatternMatches_2EPMATCH__IS__EXHAUSTIVE(A_27b,A_27c),V4x),ap(ap(c_2Elist_2EMAP(arr(A_27b,arr(A_27b,ty_2Eoption_2Eoption(A_27c))),arr(A_27b,ty_2Eoption_2Eoption(A_27c))),f852(A_27c,A_27b,V4x)),V3rows))))) => p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__EQUIV__ROWS(A_27a,A_27c),V0v),ap(ap(c_2Elist_2ECONS(arr(A_27a,ty_2Eoption_2Eoption(A_27c))),ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27c,A_27b,A_27a),V1p),V2g),f854(A_27b,A_27c,V3rows))),c_2Elist_2ENIL(arr(A_27a,ty_2Eoption_2Eoption(A_27c))))),ap(ap(c_2Elist_2EMAP(arr(A_27b,arr(A_27b,ty_2Eoption_2Eoption(A_27c))),arr(A_27a,ty_2Eoption_2Eoption(A_27c))),f855(A_27a,A_27c,A_27b,V2g,V1p)),V3rows))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__FLATTEN__THM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1p:$i] : (mem(V1p,arr(A_27b,A_27a)) => ( ! [V2g:$i] : (mem(V2g,arr(A_27b,bool)) => ( ! [V3rows1:$i] : (mem(V3rows1,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27c)))) => ( ! [V4rows2:$i] : (mem(V4rows2,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27c)))) => ( ! [V5rows:$i] : (mem(V5rows,ty_2Elist_2Elist(arr(A_27b,arr(A_27b,ty_2Eoption_2Eoption(A_27c))))) => (( ! [V6x:$i] : (mem(V6x,A_27b) => p(ap(ap(c_2EpatternMatches_2EPMATCH__IS__EXHAUSTIVE(A_27b,A_27c),V6x),ap(ap(c_2Elist_2EMAP(arr(A_27b,arr(A_27b,ty_2Eoption_2Eoption(A_27c))),arr(A_27b,ty_2Eoption_2Eoption(A_27c))),f853(A_27c,A_27b,V6x)),V5rows))))) => (ap(ap(c_2EpatternMatches_2EPMATCH(A_27c,A_27a),V0v),ap(ap(c_2Elist_2EAPPEND(arr(A_27a,ty_2Eoption_2Eoption(A_27c))),V3rows1),ap(ap(c_2Elist_2ECONS(arr(A_27a,ty_2Eoption_2Eoption(A_27c))),ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27c,A_27b,A_27a),V1p),V2g),f857(A_27b,A_27c,V5rows))),V4rows2))) = ap(ap(c_2EpatternMatches_2EPMATCH(A_27c,A_27a),V0v),ap(ap(c_2Elist_2EAPPEND(arr(A_27a,ty_2Eoption_2Eoption(A_27c))),ap(ap(c_2Elist_2EAPPEND(arr(A_27a,ty_2Eoption_2Eoption(A_27c))),V3rows1),ap(ap(c_2Elist_2EMAP(arr(A_27b,arr(A_27b,ty_2Eoption_2Eoption(A_27c))),arr(A_27a,ty_2Eoption_2Eoption(A_27c))),f858(A_27a,A_27c,A_27b,V2g,V1p)),V5rows))),V4rows2))))))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__FLATTEN__FUN__PMATCH__ROW,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0p:$i] : (mem(V0p,arr(A_27a,A_27b)) => (( ! [V1x1:$i] : (mem(V1x1,A_27a) => ( ! [V2x2:$i] : (mem(V2x2,A_27a) => ((ap(V0p,V1x1) = ap(V0p,V2x2)) => (V1x1 = V2x2)))))) => ( ! [V3g:$i] : (mem(V3g,arr(A_27a,bool)) => ( ! [V4p_27:$i] : (mem(V4p_27,arr(A_27c,A_27a)) => ( ! [V5g_27:$i] : (mem(V5g_27,arr(A_27a,arr(A_27c,bool))) => ( ! [V6r_27:$i] : (mem(V6r_27,arr(A_27a,arr(A_27c,A_27d))) => (ap(ap(ap(c_2EpatternMatches_2EPMATCH__FLATTEN__FUN(A_27d,A_27a,A_27b),V0p),V3g),f859(A_27c,A_27d,A_27a,V4p_27,V5g_27,V6r_27)) = ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW(A_27d,A_27c,A_27b),f860(A_27b,A_27a,A_27c,V4p_27,V0p)),f861(A_27a,A_27c,V3g,V5g_27,V4p_27)),f862(A_27a,A_27d,A_27c,V6r_27,V4p_27)))))))))))))))))))).
tff(ax_thm_2EpatternMatches_2EPMATCH__ROW__COND__NOT__EX__OR__EQ__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,A_27a) => ( ! [V1r:$i] : (mem(V1r,arr(A_27a,ty_2Eoption_2Eoption(A_27b))) => ( ! [V2rows:$i] : (mem(V2rows,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND__NOT__EX__OR__EQ(A_27a,A_27b),V0i),V1r),V2rows)) <=> ((~~ (~~ (ap(V1r,V0i) = c_2Eoption_2ENONE(A_27b)))) | (p(ap(ap(c_2Elist_2EEXISTS(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),f863(A_27b,A_27a,V0i)),V2rows)) & (ap(c_2Eoption_2ETHE(A_27b),ap(V1r,V0i)) = ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27a),V0i),V2rows)))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROW__COND__NOT__EX__OR__EQ__FIRST__ROW,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,A_27a) => ( ! [V1r:$i] : (mem(V1r,arr(A_27a,ty_2Eoption_2Eoption(A_27b))) => ( ! [V2r_27:$i] : (mem(V2r_27,arr(A_27a,ty_2Eoption_2Eoption(A_27b))) => ( ! [V3rows:$i] : (mem(V3rows,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ((~~ (ap(V2r_27,V0i) = c_2Eoption_2ENONE(A_27b))) => (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND__NOT__EX__OR__EQ(A_27a,A_27b),V0i),V1r),ap(ap(c_2Elist_2ECONS(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V2r_27),V3rows))) <=> ((~~ (ap(V1r,V0i) = c_2Eoption_2ENONE(A_27b))) => (ap(V1r,V0i) = ap(V2r_27,V0i))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROW__COND__NOT__EX__OR__EQ__NIL,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,A_27a) => ( ! [V1r:$i] : (mem(V1r,arr(A_27a,ty_2Eoption_2Eoption(A_27b))) => (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND__NOT__EX__OR__EQ(A_27a,A_27b),V0i),V1r),c_2Elist_2ENIL(arr(A_27a,ty_2Eoption_2Eoption(A_27b))))) <=> ((~~ (ap(V1r,V0i) = c_2Eoption_2ENONE(A_27b))) => $false)))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__ROW__COND__NOT__EX__OR__EQ__NOT__FIRST__ROW,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,A_27a) => ( ! [V1r_27:$i] : (mem(V1r_27,arr(A_27a,ty_2Eoption_2Eoption(A_27b))) => ( ! [V2rows:$i] : (mem(V2rows,ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(A_27b)))) => ( ! [V3r:$i] : (mem(V3r,arr(A_27a,ty_2Eoption_2Eoption(A_27b))) => (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND__NOT__EX__OR__EQ(A_27a,A_27b),V0i),V1r_27),V2rows)) => (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND__NOT__EX__OR__EQ(A_27a,A_27b),V0i),V3r),ap(ap(c_2Elist_2ECONS(arr(A_27a,ty_2Eoption_2Eoption(A_27b))),V1r_27),V2rows))) <=> p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND__NOT__EX__OR__EQ(A_27a,A_27b),V0i),V3r),V2rows)))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__PRED__UNROLL__NIL,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,A_27b)) => ( ! [V1v:$i] : (mem(V1v,A_27c) => (ap(V0P,ap(ap(c_2EpatternMatches_2EPMATCH(A_27a,A_27c),V1v),c_2Elist_2ENIL(arr(A_27c,ty_2Eoption_2Eoption(A_27a))))) = ap(V0P,c_2Ebool_2EARB(A_27a)))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__PRED__UNROLL__CONS,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1v:$i] : (mem(V1v,A_27b) => ( ! [V2r:$i] : (mem(V2r,arr(A_27b,ty_2Eoption_2Eoption(A_27a))) => ( ! [V3rows:$i] : (mem(V3rows,ty_2Elist_2Elist(arr(A_27b,ty_2Eoption_2Eoption(A_27a)))) => (p(ap(V0P,ap(ap(c_2EpatternMatches_2EPMATCH(A_27a,A_27b),V1v),ap(ap(c_2Elist_2ECONS(arr(A_27b,ty_2Eoption_2Eoption(A_27a))),V2r),V3rows)))) <=> (((~~ (ap(V2r,V1v) = c_2Eoption_2ENONE(A_27a))) => p(ap(V0P,ap(c_2Eoption_2ETHE(A_27a),ap(V2r,V1v))))) & (p(ap(ap(ap(c_2EpatternMatches_2EPMATCH__ROW__COND__NOT__EX__OR__EQ(A_27b,A_27a),V1v),V2r),V3rows)) => p(ap(V0P,ap(ap(c_2EpatternMatches_2EPMATCH(A_27a,A_27b),V1v),V3rows)))))))))))))))))).
tff(ax_thm_2EpatternMatches_2EPMATCH__EXPAND__PRED__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1v:$i] : (mem(V1v,A_27b) => ( ! [V2rows__before:$i] : (mem(V2rows__before,ty_2Elist_2Elist(arr(A_27b,ty_2Eoption_2Eoption(A_27a)))) => (p(ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__EXPAND__PRED(A_27a,A_27b),V0P),V1v),V2rows__before),c_2Elist_2ENIL(arr(A_27b,ty_2Eoption_2Eoption(A_27a))))) <=> ((~~ p(ap(ap(c_2EpatternMatches_2EPMATCH__IS__EXHAUSTIVE(A_27b,A_27a),V1v),ap(c_2Elist_2EREVERSE(arr(A_27b,ty_2Eoption_2Eoption(A_27a))),V2rows__before)))) => p(ap(V0P,c_2Ebool_2EARB(A_27a))))))))))) & ( ! [V3P:$i] : (mem(V3P,arr(A_27a,bool)) => ( ! [V4v:$i] : (mem(V4v,A_27b) => ( ! [V5rows__before:$i] : (mem(V5rows__before,ty_2Elist_2Elist(arr(A_27b,ty_2Eoption_2Eoption(A_27a)))) => ( ! [V6r:$i] : (mem(V6r,arr(A_27b,ty_2Eoption_2Eoption(A_27a))) => ( ! [V7rows__after:$i] : (mem(V7rows__after,ty_2Elist_2Elist(arr(A_27b,ty_2Eoption_2Eoption(A_27a)))) => (p(ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__EXPAND__PRED(A_27a,A_27b),V3P),V4v),V5rows__before),ap(ap(c_2Elist_2ECONS(arr(A_27b,ty_2Eoption_2Eoption(A_27a))),V6r),V7rows__after))) <=> (((~~ (ap(V6r,V4v) = c_2Eoption_2ENONE(A_27a))) => (p(ap(ap(c_2Elist_2EEVERY(arr(A_27b,ty_2Eoption_2Eoption(A_27a))),f864(A_27a,A_27b,V6r,V4v)),V5rows__before)) => p(ap(V3P,ap(c_2Eoption_2ETHE(A_27a),ap(V6r,V4v)))))) & p(ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__EXPAND__PRED(A_27a,A_27b),V3P),V4v),ap(ap(c_2Elist_2ECONS(arr(A_27b,ty_2Eoption_2Eoption(A_27a))),V6r),V5rows__before)),V7rows__after)))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__EXPAND__PRED__THM__GEN,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1v:$i] : (mem(V1v,A_27b) => ( ! [V2rows__before:$i] : (mem(V2rows__before,ty_2Elist_2Elist(arr(A_27b,ty_2Eoption_2Eoption(A_27a)))) => ( ! [V3rows__after:$i] : (mem(V3rows__after,ty_2Elist_2Elist(arr(A_27b,ty_2Eoption_2Eoption(A_27a)))) => (p(ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__EXPAND__PRED(A_27a,A_27b),V0P),V1v),V2rows__before),V3rows__after)) <=> (p(ap(ap(c_2Elist_2EEVERY(arr(A_27b,ty_2Eoption_2Eoption(A_27a))),f865(A_27a,A_27b,V1v,V3rows__after)),V2rows__before)) => p(ap(V0P,ap(ap(c_2EpatternMatches_2EPMATCH(A_27a,A_27b),V1v),V3rows__after))))))))))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__EXPAND__PRED__THM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1v:$i] : (mem(V1v,A_27b) => ( ! [V2rows:$i] : (mem(V2rows,ty_2Elist_2Elist(arr(A_27b,ty_2Eoption_2Eoption(A_27a)))) => (p(ap(V0P,ap(ap(c_2EpatternMatches_2EPMATCH(A_27a,A_27b),V1v),V2rows))) <=> p(ap(ap(ap(ap(c_2EpatternMatches_2EPMATCH__EXPAND__PRED(A_27a,A_27b),V0P),V1v),c_2Elist_2ENIL(arr(A_27b,ty_2Eoption_2Eoption(A_27a)))),V2rows))))))))))))).
tff(ax_thm_2EpatternMatches_2EPMATCH__ROW__LIFT__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27c,A_27b)) => ( ! [V1r:$i] : (mem(V1r,arr(A_27a,ty_2Eoption_2Eoption(A_27c))) => (ap(ap(c_2EpatternMatches_2EPMATCH__ROW__LIFT(A_27a,A_27b,A_27c),V0f),V1r) = f866(A_27b,A_27c,A_27a,V1r,V0f)))))))))).
tff(conj_thm_2EpatternMatches_2EPMATCH__LIFT__THM,conjecture,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1v:$i] : (mem(V1v,A_27c) => ( ! [V2rows:$i] : (mem(V2rows,ty_2Elist_2Elist(arr(A_27c,ty_2Eoption_2Eoption(A_27a)))) => (p(ap(ap(c_2EpatternMatches_2EPMATCH__IS__EXHAUSTIVE(A_27c,A_27a),V1v),V2rows)) => (ap(V0f,ap(ap(c_2EpatternMatches_2EPMATCH(A_27a,A_27c),V1v),V2rows)) = ap(ap(c_2EpatternMatches_2EPMATCH(A_27b,A_27c),V1v),ap(ap(c_2Elist_2EMAP(arr(A_27c,ty_2Eoption_2Eoption(A_27a)),arr(A_27c,ty_2Eoption_2Eoption(A_27b))),ap(c_2EpatternMatches_2EPMATCH__ROW__LIFT(A_27c,A_27b,A_27a),V0f)),V2rows))))))))))))))).
