include('Axioms/numposrep^2.ax').
thf(tp_c_2EpatternMatches_2EAPPLY__REDUNDANT__ROWS__INFO,type,(c_2EpatternMatches_2EAPPLY__REDUNDANT__ROWS__INFO:(del>$i))).
thf(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)))))).
thf(tp_c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO,type,(c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2EpatternMatches_2EPMATCH,type,(c_2EpatternMatches_2EPMATCH:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2EpatternMatches_2EPMATCH__EQUIV__ROWS,type,(c_2EpatternMatches_2EPMATCH__EQUIV__ROWS:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2EpatternMatches_2EPMATCH__EXPAND__PRED,type,(c_2EpatternMatches_2EPMATCH__EXPAND__PRED:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2EpatternMatches_2EPMATCH__FLATTEN__FUN,type,(c_2EpatternMatches_2EPMATCH__FLATTEN__FUN:(del>(del>(del>$i))))).
thf(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)))))))))).
thf(tp_c_2EpatternMatches_2EPMATCH__INCOMPLETE,type,(c_2EpatternMatches_2EPMATCH__INCOMPLETE:(del>$i))).
thf(mem_c_2EpatternMatches_2EPMATCH__INCOMPLETE,axiom,( ! [A_27a:del] : (mem@(c_2EpatternMatches_2EPMATCH__INCOMPLETE@A_27a)@A_27a))).
thf(tp_c_2EpatternMatches_2EPMATCH__IS__EXHAUSTIVE,type,(c_2EpatternMatches_2EPMATCH__IS__EXHAUSTIVE:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2EpatternMatches_2EPMATCH__ROW,type,(c_2EpatternMatches_2EPMATCH__ROW:(del>(del>(del>$i))))).
thf(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)))))))))).
thf(tp_c_2EpatternMatches_2EPMATCH__ROW__COND,type,(c_2EpatternMatches_2EPMATCH__ROW__COND:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2EpatternMatches_2EPMATCH__ROW__COND__EX,type,(c_2EpatternMatches_2EPMATCH__ROW__COND__EX:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2EpatternMatches_2EPMATCH__ROW__COND__NOT__EX__OR__EQ,type,(c_2EpatternMatches_2EPMATCH__ROW__COND__NOT__EX__OR__EQ:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2EpatternMatches_2EPMATCH__ROW__LIFT,type,(c_2EpatternMatches_2EPMATCH__ROW__LIFT:(del>(del>(del>$i))))).
thf(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))))))))).
thf(tp_c_2EpatternMatches_2EPMATCH__ROW__REDUNDANT,type,(c_2EpatternMatches_2EPMATCH__ROW__REDUNDANT:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2EpatternMatches_2EPMATCH__ROW__magic__0,type,(c_2EpatternMatches_2EPMATCH__ROW__magic__0:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2EpatternMatches_2EPMATCH__ROW__magic__1,type,(c_2EpatternMatches_2EPMATCH__ROW__magic__1:(del>(del>(del>$i))))).
thf(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)))))))).
thf(tp_c_2EpatternMatches_2EPMATCH__ROW__magic__2,type,(c_2EpatternMatches_2EPMATCH__ROW__magic__2:(del>(del>$i)))).
thf(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))))))))).
thf(tp_c_2EpatternMatches_2EPMATCH__ROW__magic__3,type,(c_2EpatternMatches_2EPMATCH__ROW__magic__3:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2EpatternMatches_2EPMATCH__ROW__magic__4,type,(c_2EpatternMatches_2EPMATCH__ROW__magic__4:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2EpatternMatches_2EPMATCH__magic__1,type,(c_2EpatternMatches_2EPMATCH__magic__1:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2EpatternMatches_2EREDUNDANT__ROWS__INFOS__CONJ,type,(c_2EpatternMatches_2EREDUNDANT__ROWS__INFOS__CONJ:$i)).
thf(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))))).
thf(tp_c_2EpatternMatches_2EREDUNDANT__ROWS__INFOS__DISJ,type,(c_2EpatternMatches_2EREDUNDANT__ROWS__INFOS__DISJ:$i)).
thf(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))))).
thf(tp_c_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO,type,(c_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO:(del>(del>$i)))).
thf(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))))))).
thf(stp_c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o,type,(tp__c_ty_2Epair_2Eprod_o_c_ty_2Elist_2Elist_o : $tType)).
thf(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))).
thf(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))).
thf(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))).
thf(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))))).
thf(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)))))).
thf(tp_c_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO__AUX,type,(c_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO__AUX:(del>(del>$i)))).
thf(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)))))))))).
thf(stp_c_ty_2Eoption_2Eoption_o,type,(tp__c_ty_2Eoption_2Eoption_o : $tType)).
thf(stp_inj_c_ty_2Eoption_2Eoption_o,type,(inj__c_ty_2Eoption_2Eoption_o : (tp__c_ty_2Eoption_2Eoption_o > $i))).
thf(stp_surj_c_ty_2Eoption_2Eoption_o,type,(surj__c_ty_2Eoption_2Eoption_o : ($i > tp__c_ty_2Eoption_2Eoption_o))).
thf(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))).
thf(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)))).
thf(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)))))).
thf(conj_thm_2EpatternMatches_2Esome__var__bool__T,lemma,((surj__c_ty_2Eoption_2Eoption_o @ (ap@(c_2Eoption_2Esome@bool)@(lam@bool@(^ [V0x:$i] : V0x)))) = (surj__c_ty_2Eoption_2Eoption_o @ (ap@(c_2Eoption_2ESOME@bool)@c_2Ebool_2ET)))).
thf(conj_thm_2EpatternMatches_2Esome__var__bool__F,lemma,((surj__c_ty_2Eoption_2Eoption_o @ (ap@(c_2Eoption_2Esome@bool)@(lam@bool@(^ [V0x:$i] : (ap@c_2Ebool_2E_7E@V0x))))) = (surj__c_ty_2Eoption_2Eoption_o @ (ap@(c_2Eoption_2ESOME@bool)@c_2Ebool_2EF)))).
thf(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))))))))))))))).
thf(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)@(lam@A_27b@(^ [V4v:$i] : (ap@(ap@(ap@(ap@(c_2EpatternMatches_2EPMATCH__ROW__COND@A_27b@A_27c)@V0pat)@V1guard)@V3i)@V4v)))))))))))))))))).
thf(ax_thm_2EpatternMatches_2EPMATCH__INCOMPLETE__def,axiom,( ! [A_27a:del]: ((c_2EpatternMatches_2EPMATCH__INCOMPLETE@A_27a) = (c_2Ebool_2EARB@A_27a)))).
thf(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))))))))))))).
thf(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))))))))))))))))))))))).
thf(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))))))))))))))))))).
thf(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)))))))))))))))))))).
thf(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)))))))))))))))))).
thf(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)))))))))))))))))))).
thf(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)@(lam@A_27a@(^ [V6y:$i] : (ap@(ap@(ap@(ap@(c_2EpatternMatches_2EPMATCH__ROW__COND@A_27a@A_27b)@V0p)@V1g)@V2i)@V6y)))) = V5x)))))))))))))).
thf(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))))))))))))))).
thf(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)@(lam@A_27d@(^ [V5x:$i] : (ap@(ap@(ap@(ap@(c_2EpatternMatches_2EPMATCH__ROW__COND@A_27d@A_27b)@V1p)@V2g)@V0v)@V5x)))))@(ap@V3r@(ap@(c_2Emin_2E_40@A_27d)@(lam@A_27d@(^ [V6x:$i] : (ap@(ap@(ap@(ap@(c_2EpatternMatches_2EPMATCH__ROW__COND@A_27d@A_27b)@V1p)@V2g)@V0v)@V6x))))))@(ap@(ap@(c_2EpatternMatches_2EPMATCH@A_27c@A_27b)@V0v)@V4rs))))))))))))))))))).
thf(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)@(lam@A_27b@(^ [V5x:$i] : (ap@(ap@(ap@(ap@(c_2EpatternMatches_2EPMATCH__ROW__COND@A_27b@A_27c)@V0p)@V1g)@V3v)@V5x))))))))))))))))))))).
thf(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))))))))))))).
thf(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))))))))))))))))))))).
thf(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))))))))))))))).
thf(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)))))))))))))))))).
thf(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)@(lam@A_27c@(^ [V7x:$i] : (ap@V0ff@(ap@V2p@V7x)))))@V3g)@V4r)@(ap@V0ff@V1v)) = (ap@(ap@(ap@(ap@(c_2EpatternMatches_2EPMATCH__ROW@A_27d@A_27c@A_27a)@(lam@A_27c@(^ [V8x:$i] : (ap@V2p@V8x))))@V3g)@V4r)@V1v)))))))))))))))))).
thf(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)@(lam@A_27d@(^ [V13x:$i] : (ap@(ap@V5g@(ap@V2f_27@(ap@V7p_27@V13x)))@(ap@V3f@V13x)))))@(lam@A_27d@(^ [V14x:$i] : (ap@(ap@V6r@(ap@V2f_27@(ap@V7p_27@V14x)))@(ap@V3f@V14x)))))@V1v_27)))))))))))))))))))))))))).
thf(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)@(lam@A_27c@(^ [V12x:$i] : (ap@V4g@(ap@V2f@V12x)))))@(lam@A_27c@(^ [V13x:$i] : (ap@V5r@(ap@V2f@V13x)))))@V1v_27))))))))))))))))))))))).
thf(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)))))))))))))))))).
thf(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)))))))))))).
thf(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))))))))).
thf(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)))))))))))).
thf(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))))))))))))))).
thf(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)))))))))))).
thf(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)))@(lam@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b))@(^ [V3r:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(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)))@(ap@(c_2Eoption_2EIS__SOME@A_27b)@(ap@V3r@V0v)))))))@(ap@(ap@(c_2EpatternMatches_2EPMATCH@A_27b@A_27a)@V0v)@V1rows1))@(ap@(ap@(c_2EpatternMatches_2EPMATCH@A_27b@A_27a)@V0v)@V2rows2)))))))))))).
thf(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)))))))))))))))))).
thf(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)))))))))))).
thf(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)))))))))))).
thf(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)))))))))))).
thf(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))))))))))))))))))).
thf(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))))))))))))))))))))))))))))).
thf(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)))@(lam@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b))@(^ [V7row:$i] : (ap@(ap@(c_2Emin_2E_3D@(ty_2Eoption_2Eoption@A_27b))@(ap@V7row@V5v))@(c_2Eoption_2ENONE@A_27b)))))@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)))))))))))))))))))).
thf(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)))@(lam@(arr@A_27b@(ty_2Eoption_2Eoption@A_27c))@(^ [V15row:$i] : (ap@(ap@(c_2Emin_2E_3D@(ty_2Eoption_2Eoption@A_27c))@(ap@V15row@(ap@V0p@V14x)))@(c_2Eoption_2ENONE@A_27c)))))@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)))))))))))))))))))))))))))))).
thf(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))))))))))))))))).
thf(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)@(lam@A_27b@(^ [V2__0:$i] : V2__0)))@(lam@A_27b@(^ [V3__0:$i] : c_2Ebool_2ET)))@(lam@A_27b@(^ [V4__0:$i] : (c_2Ebool_2EARB@A_27a)))))@V1rows)))))))))).
thf(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)))@(lam@(arr@A_27a@(ty_2Eoption_2Eoption@A_27c))@(^ [V8row:$i] : (ap@(ap@(c_2Emin_2E_3D@(ty_2Eoption_2Eoption@A_27c))@(ap@V8row@(ap@V1p@V7x)))@(c_2Eoption_2ENONE@A_27c)))))@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)))))))))))))))))))).
thf(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)))))))))))))))).
thf(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))))))).
thf(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)))))))))))).
thf(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))))))))))))))).
thf(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))))))))))))))).
thf(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)))@(lam@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b))@(^ [V4r:$i] : (ap@(ap@(c_2Emin_2E_3D@(ty_2Eoption_2Eoption@A_27b))@(ap@V4r@V0v))@(c_2Eoption_2ENONE@A_27b)))))@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))))))))))))))))).
thf(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:$i] : ((mem@V2c@bool) => ( ! [V3infos:tp__c_ty_2Elist_2Elist_o] : ((p@(ap@(ap@(ap@(ap@(c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO@A_27a@A_27b)@V0v)@V1rows)@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)))@(lam@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b))@(^ [V5r:$i] : (ap@(ap@(c_2Emin_2E_3D@(ty_2Eoption_2Eoption@A_27b))@(ap@V5r@V0v))@(c_2Eoption_2ENONE@A_27b)))))@V1rows)) => (p@V2c))))))))))))))).
thf(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))))@c_2Ebool_2ET)@(c_2Elist_2ENIL@bool)))))))).
thf(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:$i] : ((mem@V2c@bool) => ( ! [V3infos:tp__c_ty_2Elist_2Elist_o] : ( ! [V4r:$i] : ((mem@V4r@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b))) => ( ! [V5i:$i] : ((mem@V5i@bool) => ( ! [V6c_27:$i] : ((mem@V6c_27@bool) => ((p@(ap@(ap@(ap@(ap@(c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO@A_27a@A_27b)@V0v)@V1rows)@V2c)@(inj__c_ty_2Elist_2Elist_o @ V3infos))) => ((((ap@V4r@V0v) = (c_2Eoption_2ENONE@A_27b)) => ((p@V2c) => (p@V6c_27))) => (((p@V2c) => ((p@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))@V6c_27)@(ap@(ap@(c_2Elist_2ESNOC@bool)@V5i)@(inj__c_ty_2Elist_2Elist_o @ V3infos))))))))))))))))))))))).
thf(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)))))))))))))).
thf(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:$i] : ((mem@V2c@bool) => ( ! [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:$i] : ((mem@V7c_27@bool) => ((p@(ap@(ap@(ap@(ap@(c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO@A_27a@A_27b)@V0v)@V1rows)@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@V2c) <=> (p@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))@V7c_27)@(ap@(ap@(c_2Elist_2ESNOC@bool)@(ap@(ap@c_2Emin_2E_3D_3D_3E@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))))))))))))))))))))))))).
thf(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:$i] : ((mem@V3c@bool) => ( ! [V4i:$i] : ((mem@V4i@bool) => ( ! [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))@V3c)@(ap@(ap@(c_2Elist_2ECONS@bool)@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@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)@V3c)@(inj__c_ty_2Elist_2Elist_o @ V5infos_27))))))))))))))))))))).
thf(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))@(lam@(ty_2Epair_2Eprod@bool@A_27a)@(^ [V2x:$i] : (ap@c_2Ebool_2E_7E@(ap@(c_2Epair_2EFST@bool@A_27a)@V2x)))))@(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)))))))))).
thf(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)@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)@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)))))))))))))).
thf(conj_thm_2EpatternMatches_2EPMATCH__ROWS__DROP__REDUNDANT__ROWS__INFO__EQUIV,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : ((mem@V0v@A_27a) => ( ! [V1c:$i] : ((mem@V1c@bool) => ( ! [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)@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)))))))))))))).
thf(conj_thm_2EpatternMatches_2EREDUNDANT__ROWS__INFO__TO__PMATCH__EQ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : ((mem@V0v@A_27a) => ( ! [V1c:$i] : ((mem@V1c@bool) => ( ! [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)@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)))))))))))))).
thf(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)))@(lam@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b))@(^ [V2r:$i] : (ap@(c_2Eoption_2EIS__SOME@A_27b)@(ap@V2r@V0v)))))@V1rs)))))))))).
thf(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)))))))))))))))).
thf(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:$i] : ((mem@V2c@bool) => ( ! [V3infos:tp__c_ty_2Elist_2Elist_o] : ((p@(ap@(ap@(ap@(ap@(c_2EpatternMatches_2EIS__REDUNDANT__ROWS__INFO@A_27a@A_27b)@V0v)@V1rows)@V2c)@(inj__c_ty_2Elist_2Elist_o @ V3infos))) => ((~~ (p@V2c)) => (p@(ap@(ap@(c_2EpatternMatches_2EPMATCH__IS__EXHAUSTIVE@A_27a@A_27b)@V0v)@V1rows)))))))))))))).
thf(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)@(lam@bool@(^ [V2i1:$i] : (lam@bool@(^ [V3i2:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@V2i1)@V3i2))))))@(inj__c_ty_2Elist_2Elist_o @ V0ip1))@(inj__c_ty_2Elist_2Elist_o @ V1ip2))))))).
thf(conj_thm_2EpatternMatches_2EREDUNDANT__ROWS__INFOS__CONJ__REWRITE,lemma,( ! [V0i1:$i] : ((mem@V0i1@bool) => ( ! [V1is1:tp__c_ty_2Elist_2Elist_o] : ( ! [V2i2:$i] : ((mem@V2i2@bool) => ( ! [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)@V0i1)@(inj__c_ty_2Elist_2Elist_o @ V1is1)))@(ap@(ap@(c_2Elist_2ECONS@bool)@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@V0i1)@V2i2))@(ap@(ap@c_2EpatternMatches_2EREDUNDANT__ROWS__INFOS__CONJ@(inj__c_ty_2Elist_2Elist_o @ V1is1))@(inj__c_ty_2Elist_2Elist_o @ V3is2))))))))))))).
thf(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:$i] : ((mem@V2c@bool) => ( ! [V3infos:tp__c_ty_2Elist_2Elist_o] : ( ! [V4c_27:$i] : ((mem@V4c_27@bool) => ( ! [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)@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@V2c)@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))))))))))))))))))).
thf(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)@(lam@bool@(^ [V2i1:$i] : (lam@bool@(^ [V3i2:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@V2i1)@V3i2))))))@(inj__c_ty_2Elist_2Elist_o @ V0ip1))@(inj__c_ty_2Elist_2Elist_o @ V1ip2))))))).
thf(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:$i] : ((mem@V2c@bool) => ( ! [V3infos:tp__c_ty_2Elist_2Elist_o] : ( ! [V4c_27:$i] : ((mem@V4c_27@bool) => ( ! [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)@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)@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@V2c)@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))))))))))))))))))).
thf(ax_thm_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO__AUX__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0v:$i] : ((mem@V0v@A_27a) => ( ! [V1p:$i] : ((mem@V1p@bool) => ( ! [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))))@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))@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:$i] : ((mem@V6p@bool) => ( ! [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))@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@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@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)))))))))))))))))).
thf(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)@c_2Ebool_2ET)@(c_2Elist_2ENIL@bool)))))))))))).
thf(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:$i] : ((mem@V2p@bool) => ( ! [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)@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))))))))))))))).
thf(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:$i] : ((mem@V2p@bool) => ( ! [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)@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)))))))))))))))).
thf(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:$i] : ((mem@V2p@bool) => ( ! [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)@V2p)@(inj__c_ty_2Elist_2Elist_o @ V3infos))))) <=> (((p@V2p) & (p@(ap@(ap@(c_2Elist_2EEVERY@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b)))@(lam@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b))@(^ [V5r:$i] : (ap@(ap@(c_2Emin_2E_3D@(ty_2Eoption_2Eoption@A_27b))@(ap@V5r@V0v))@(c_2Eoption_2ENONE@A_27b)))))@(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)))))))))))))))).
thf(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)))))))))).
thf(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:$i] : ((mem@V2p@bool) => ( ! [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)@V2p)@(inj__c_ty_2Elist_2Elist_o @ V3infos)))) <=> ((p@V2p) & (p@(ap@(ap@(c_2Elist_2EEVERY@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b)))@(lam@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b))@(^ [V4r:$i] : (ap@(ap@(c_2Emin_2E_3D@(ty_2Eoption_2Eoption@A_27b))@(ap@V4r@V0v))@(c_2Eoption_2ENONE@A_27b)))))@V1rows)))))))))))))).
thf(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)))@(lam@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b))@(^ [V3r:$i] : (ap@(ap@(c_2Emin_2E_3D@(ty_2Eoption_2Eoption@A_27b))@(ap@V3r@V0v))@(c_2Eoption_2ENONE@A_27b)))))@(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))))))))))))).
thf(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)))@(lam@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b))@(^ [V2r:$i] : (ap@(ap@(c_2Emin_2E_3D@(ty_2Eoption_2Eoption@A_27b))@(ap@V2r@V0v))@(c_2Eoption_2ENONE@A_27b)))))@V1rows))@(ap@(ap@(c_2EpatternMatches_2ESTRONGEST__REDUNDANT__ROWS__INFO@A_27a@A_27b)@V0v)@V1rows)))))))))).
thf(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))))))))))))))).
thf(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)@(lam@A_27a@(^ [V7x:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V5g_27@V7x))@(ap@c_2Ebool_2E_7E@(ap@V3g@(ap@V0f@V7x))))))))))))))))))))))))))).
thf(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))))))))))).
thf(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:$i] : ((mem@V5RES@bool) => ((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@V5RES))))) => ((p@(ap@(ap@(ap@(c_2EpatternMatches_2EPMATCH__ROW__COND__EX@A_27a@A_27c)@V0v)@V3p_27)@V4g_27)) <=> (p@V5RES)))))))))))))))))))).
thf(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)))@(lam@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b))@(^ [V2r:$i] : (ap@(ap@(c_2Emin_2E_3D@(ty_2Eoption_2Eoption@A_27b))@(ap@V2r@V0v))@(c_2Eoption_2ENONE@A_27b)))))@V1rs)) => $false) => (p@(ap@(ap@(c_2EpatternMatches_2EPMATCH__IS__EXHAUSTIVE@A_27a@A_27b)@V0v)@V1rs)))))))))).
thf(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)@(lam@A_27b@(^ [V4x:$i] : (ap@(ap@(ap@(ap@(c_2EpatternMatches_2EPMATCH__ROW__COND@A_27b@A_27a)@V1p)@V2g)@V0i)@V4x)))))))))))))))))))).
thf(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))))))))))))))).
thf(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)))))))))))))))))))))).
thf(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)@(lam@A_27c@(^ [V8x:$i] : c_2Ebool_2ET)))@(lam@A_27c@(^ [V9x:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@A_27b)@(ap@V4g@V9x))@(ap@V5r@V9x))@(ap@(ap@(c_2EpatternMatches_2EPMATCH@A_27b@A_27a)@(ap@V3p@V9x))@V2rs2))))))@V2rs2))))))))))))))))))))).
thf(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)@(lam@A_27b@(^ [V4x:$i] : (ap@(ap@(ap@(ap@(c_2EpatternMatches_2EPMATCH__ROW__COND@A_27b@A_27c)@V0p)@V1g)@V3v)@V4x)))))@(c_2Eoption_2ENONE@A_27a))@(lam@A_27b@(^ [V5x:$i] : (ap@(ap@V2row@V5x)@V5x))))))))))))))))).
thf(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)))@(lam@(arr@A_27b@(arr@A_27b@(ty_2Eoption_2Eoption@A_27c)))@(^ [V5r:$i] : (ap@V5r@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)@(lam@A_27b@(^ [V6x:$i] : (ap@(ap@(c_2EpatternMatches_2EPMATCH@A_27c@A_27b)@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)))@(lam@(arr@A_27b@(arr@A_27b@(ty_2Eoption_2Eoption@A_27c)))@(^ [V7r:$i] : (ap@V7r@V6x))))@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)))@(lam@(arr@A_27b@(arr@A_27b@(ty_2Eoption_2Eoption@A_27c)))@(^ [V8r:$i] : (ap@(ap@(ap@(c_2EpatternMatches_2EPMATCH__FLATTEN__FUN@A_27c@A_27b@A_27a)@V1p)@V2g)@V8r))))@V3rows)))))))))))))))).
thf(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)))@(lam@(arr@A_27b@(arr@A_27b@(ty_2Eoption_2Eoption@A_27c)))@(^ [V7r:$i] : (ap@V7r@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)@(lam@A_27b@(^ [V8x:$i] : (ap@(ap@(c_2EpatternMatches_2EPMATCH@A_27c@A_27b)@V8x)@(ap@(ap@(c_2Elist_2EMAP@(arr@A_27b@(arr@A_27b@(ty_2Eoption_2Eoption@A_27c)))@(arr@A_27b@(ty_2Eoption_2Eoption@A_27c)))@(lam@(arr@A_27b@(arr@A_27b@(ty_2Eoption_2Eoption@A_27c)))@(^ [V9r:$i] : (ap@V9r@V8x))))@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)))@(lam@(arr@A_27b@(arr@A_27b@(ty_2Eoption_2Eoption@A_27c)))@(^ [V10r:$i] : (ap@(ap@(ap@(c_2EpatternMatches_2EPMATCH__FLATTEN__FUN@A_27c@A_27b@A_27a)@V1p)@V2g)@V10r))))@V5rows)))@V4rows2)))))))))))))))))))).
thf(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)@(lam@A_27a@(^ [V7x:$i] : (ap@(ap@(ap@(c_2EpatternMatches_2EPMATCH__ROW@A_27d@A_27c@A_27a)@V4p_27)@(ap@V5g_27@V7x))@(ap@V6r_27@V7x))))) = (ap@(ap@(ap@(c_2EpatternMatches_2EPMATCH__ROW@A_27d@A_27c@A_27b)@(lam@A_27c@(^ [V8x:$i] : (ap@V0p@(ap@V4p_27@V8x)))))@(lam@A_27c@(^ [V9x:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V3g@(ap@V4p_27@V9x)))@(ap@(ap@V5g_27@(ap@V4p_27@V9x))@V9x)))))@(lam@A_27c@(^ [V10x:$i] : (ap@(ap@V6r_27@(ap@V4p_27@V10x))@V10x))))))))))))))))))))).
thf(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)))@(lam@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b))@(^ [V3row:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(c_2Emin_2E_3D@(ty_2Eoption_2Eoption@A_27b))@(ap@V3row@V0i))@(c_2Eoption_2ENONE@A_27b))))))@V2rows)) & ((ap@(c_2Eoption_2ETHE@A_27b)@(ap@V1r@V0i)) = (ap@(ap@(c_2EpatternMatches_2EPMATCH@A_27b@A_27a)@V0i)@V2rows)))))))))))))).
thf(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)))))))))))))))).
thf(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))))))))).
thf(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))))))))))))))).
thf(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))))))))))).
thf(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))))))))))))))))).
thf(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)))@(lam@(arr@A_27b@(ty_2Eoption_2Eoption@A_27a))@(^ [V8r_27:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@c_2Ebool_2E_7E@(ap@(ap@(c_2Emin_2E_3D@(ty_2Eoption_2Eoption@A_27a))@(ap@V8r_27@V4v))@(c_2Eoption_2ENONE@A_27a))))@(ap@(ap@(c_2Emin_2E_3D@(ty_2Eoption_2Eoption@A_27a))@(ap@V8r_27@V4v))@(ap@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)))))))))))))))))).
thf(conj_thm_2EpatternMatches_2EPMATCH__EXPAND__PRED__THM__GEN,conjecture,( ! [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)))@(lam@(arr@A_27b@(ty_2Eoption_2Eoption@A_27a))@(^ [V4r:$i] : (ap@(ap@(ap@(c_2EpatternMatches_2EPMATCH__ROW__COND__NOT__EX__OR__EQ@A_27b@A_27a)@V1v)@V4r)@V3rows__after))))@V2rows__before)) => (p@(ap@V0P@(ap@(ap@(c_2EpatternMatches_2EPMATCH@A_27a@A_27b)@V1v)@V3rows__after)))))))))))))))).
