include('Axioms/errorStateMonad_2.ax').
tff(tp_c_2EquantHeuristics_2EGUESS__EXISTS,type,(c_2EquantHeuristics_2EGUESS__EXISTS:(del * del) > $i)).
tff(mem_c_2EquantHeuristics_2EGUESS__EXISTS,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),arr(arr(A_27a,A_27b),arr(arr(A_27b,bool),bool)))))).
tff(tp_c_2EquantHeuristics_2EGUESS__EXISTS__GAP,type,(c_2EquantHeuristics_2EGUESS__EXISTS__GAP:(del * del) > $i)).
tff(mem_c_2EquantHeuristics_2EGUESS__EXISTS__GAP,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),arr(arr(A_27a,A_27b),arr(arr(A_27b,bool),bool)))))).
tff(tp_c_2EquantHeuristics_2EGUESS__EXISTS__POINT,type,(c_2EquantHeuristics_2EGUESS__EXISTS__POINT:(del * del) > $i)).
tff(mem_c_2EquantHeuristics_2EGUESS__EXISTS__POINT,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),arr(arr(A_27a,A_27b),arr(arr(A_27b,bool),bool)))))).
tff(tp_c_2EquantHeuristics_2EGUESS__FORALL,type,(c_2EquantHeuristics_2EGUESS__FORALL:(del * del) > $i)).
tff(mem_c_2EquantHeuristics_2EGUESS__FORALL,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),arr(arr(A_27a,A_27b),arr(arr(A_27b,bool),bool)))))).
tff(tp_c_2EquantHeuristics_2EGUESS__FORALL__GAP,type,(c_2EquantHeuristics_2EGUESS__FORALL__GAP:(del * del) > $i)).
tff(mem_c_2EquantHeuristics_2EGUESS__FORALL__GAP,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),arr(arr(A_27a,A_27b),arr(arr(A_27b,bool),bool)))))).
tff(tp_c_2EquantHeuristics_2EGUESS__FORALL__POINT,type,(c_2EquantHeuristics_2EGUESS__FORALL__POINT:(del * del) > $i)).
tff(mem_c_2EquantHeuristics_2EGUESS__FORALL__POINT,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),arr(arr(A_27a,A_27b),arr(arr(A_27b,bool),bool)))))).
tff(tp_c_2EquantHeuristics_2EIS__REMOVABLE__QUANT__FUN,type,(c_2EquantHeuristics_2EIS__REMOVABLE__QUANT__FUN:(del * del) > $i)).
tff(mem_c_2EquantHeuristics_2EIS__REMOVABLE__QUANT__FUN,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EquantHeuristics_2EIS__REMOVABLE__QUANT__FUN(A_27a,A_27b),arr(arr(A_27a,A_27b),bool))))).
tff(tp_c_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS,type,(c_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS:del > $i)).
tff(mem_c_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS,axiom,( ! [A_27a:del] : mem(c_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS(A_27a),arr(A_27a,arr(A_27a,arr(bool,bool)))))).
tff(tp_c_2EquantHeuristics_2ESIMPLE__GUESS__FORALL,type,(c_2EquantHeuristics_2ESIMPLE__GUESS__FORALL:del > $i)).
tff(mem_c_2EquantHeuristics_2ESIMPLE__GUESS__FORALL,axiom,( ! [A_27a:del] : mem(c_2EquantHeuristics_2ESIMPLE__GUESS__FORALL(A_27a),arr(A_27a,arr(A_27a,arr(bool,bool)))))).
tff(ax_thm_2EquantHeuristics_2EGUESS__EXISTS__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27b)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27b,bool)) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),V1P)) <=> ((? [V2v:$i] : (mem(V2v,A_27b) & p(ap(V1P,V2v)))) <=> (? [V3fv:$i] : (mem(V3fv,A_27a) & p(ap(V1P,ap(V0i,V3fv)))))))))))))).
tff(ax_thm_2EquantHeuristics_2EGUESS__FORALL__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27b)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27b,bool)) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),V1P)) <=> (( ! [V2v:$i] : (mem(V2v,A_27b) => p(ap(V1P,V2v)))) <=> ( ! [V3fv:$i] : (mem(V3fv,A_27a) => p(ap(V1P,ap(V0i,V3fv)))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__EXISTS__FORALL__REWRITES,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27b)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27b,bool)) => ((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),V1P)) <=> ( ! [V2v:$i] : (mem(V2v,A_27b) => (p(ap(V1P,V2v)) => (? [V3fv:$i] : (mem(V3fv,A_27a) & p(ap(V1P,ap(V0i,V3fv))))))))) & (p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),V1P)) <=> ( ! [V4v:$i] : (mem(V4v,A_27b) => ((~~ p(ap(V1P,V4v))) => (? [V5fv:$i] : (mem(V5fv,A_27a) & (~~ p(ap(V1P,ap(V0i,V5fv))))))))))))))))))).
tff(ax_thm_2EquantHeuristics_2EGUESS__EXISTS__POINT__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27b)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27b,bool)) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),V1P)) <=> ( ! [V2fv:$i] : (mem(V2fv,A_27a) => p(ap(V1P,ap(V0i,V2fv))))))))))))).
tff(ax_thm_2EquantHeuristics_2EGUESS__FORALL__POINT__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27b)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27b,bool)) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),V1P)) <=> ( ! [V2fv:$i] : (mem(V2fv,A_27a) => (~~ p(ap(V1P,ap(V0i,V2fv)))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__POINT__THM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27b)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27b,bool)) => ((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),V1P)) => ((? [V2v:$i] : (mem(V2v,A_27b) & p(ap(V1P,V2v)))) <=> $true)) & (p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),V1P)) => (( ! [V3v:$i] : (mem(V3v,A_27b) => p(ap(V1P,V3v)))) <=> $false))))))))))).
tff(ax_thm_2EquantHeuristics_2EGUESS__EXISTS__GAP__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27b)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27b,bool)) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),V1P)) <=> ( ! [V2v:$i] : (mem(V2v,A_27b) => (p(ap(V1P,V2v)) => (? [V3fv:$i] : (mem(V3fv,A_27a) & (V2v = ap(V0i,V3fv))))))))))))))).
tff(ax_thm_2EquantHeuristics_2EGUESS__FORALL__GAP__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27b)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27b,bool)) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),V1P)) <=> ( ! [V2v:$i] : (mem(V2v,A_27b) => ((~~ p(ap(V1P,V2v))) => (? [V3fv:$i] : (mem(V3fv,A_27a) & (V2v = ap(V0i,V3fv))))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__REWRITES,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27b)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27b,bool)) => (((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),V1P)) <=> ( ! [V2v:$i] : (mem(V2v,A_27b) => (p(ap(V1P,V2v)) => (? [V3fv:$i] : (mem(V3fv,A_27a) & p(ap(V1P,ap(V0i,V3fv))))))))) & (p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),V1P)) <=> ( ! [V4v:$i] : (mem(V4v,A_27b) => ((~~ p(ap(V1P,V4v))) => (? [V5fv:$i] : (mem(V5fv,A_27a) & (~~ p(ap(V1P,ap(V0i,V5fv))))))))))) & (( ! [V6i:$i] : (mem(V6i,arr(A_27a,A_27b)) => ( ! [V7P:$i] : (mem(V7P,arr(A_27b,bool)) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V6i),V7P)) <=> ( ! [V8fv:$i] : (mem(V8fv,A_27a) => p(ap(V7P,ap(V6i,V8fv)))))))))) & (( ! [V9i:$i] : (mem(V9i,arr(A_27a,A_27b)) => ( ! [V10P:$i] : (mem(V10P,arr(A_27b,bool)) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V9i),V10P)) <=> ( ! [V11fv:$i] : (mem(V11fv,A_27a) => (~~ p(ap(V10P,ap(V9i,V11fv))))))))))) & (( ! [V12i:$i] : (mem(V12i,arr(A_27a,A_27b)) => ( ! [V13P:$i] : (mem(V13P,arr(A_27b,bool)) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V12i),V13P)) <=> ( ! [V14v:$i] : (mem(V14v,A_27b) => (p(ap(V13P,V14v)) => (? [V15fv:$i] : (mem(V15fv,A_27a) & (V14v = ap(V12i,V15fv)))))))))))) & ( ! [V16i:$i] : (mem(V16i,arr(A_27a,A_27b)) => ( ! [V17P:$i] : (mem(V17P,arr(A_27b,bool)) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V16i),V17P)) <=> ( ! [V18v:$i] : (mem(V18v,A_27b) => ((~~ p(ap(V17P,V18v))) => (? [V19fv:$i] : (mem(V19fv,A_27a) & (V18v = ap(V16i,V19fv)))))))))))))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__EXISTS__POINT__THM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27b)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27b,bool)) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),V1P)) => (p(ap(c_2Ebool_2E_3F(A_27b),V1P)) <=> $true)))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__FORALL__POINT__THM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27b)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27b,bool)) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),V1P)) => (p(ap(c_2Ebool_2E_21(A_27b),V1P)) <=> $false)))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__EXISTS__THM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27b)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27b,bool)) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),V1P)) => (p(ap(c_2Ebool_2E_3F(A_27b),V1P)) <=> (? [V2fv:$i] : (mem(V2fv,A_27a) & p(ap(V1P,ap(V0i,V2fv))))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__FORALL__THM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27b)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27b,bool)) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),V1P)) => (p(ap(c_2Ebool_2E_21(A_27b),V1P)) <=> ( ! [V2fv:$i] : (mem(V2fv,A_27a) => p(ap(V1P,ap(V0i,V2fv))))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESSES__UEXISTS__THM1,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,A_27a) => ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27b,A_27a),k(A_27b,V0i)),V1P)) => (p(ap(c_2Ebool_2E_3F_21(A_27a),V1P)) <=> (p(ap(V1P,V0i)) & ( ! [V3v:$i] : (mem(V3v,A_27a) => (p(ap(V1P,V3v)) => (V3v = V0i))))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESSES__UEXISTS__THM2,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,A_27a) => ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27b,A_27a),k(A_27b,V0i)),V1P)) => (p(ap(c_2Ebool_2E_3F_21(A_27a),V1P)) <=> p(ap(V1P,V0i)))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESSES__UEXISTS__THM3,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,A_27a) => ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27b,A_27a),k(A_27b,V0i)),V1P)) => (p(ap(c_2Ebool_2E_3F_21(A_27a),V1P)) <=> ( ! [V3v:$i] : (mem(V3v,A_27a) => (p(ap(V1P,V3v)) => (V3v = V0i)))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESSES__UEXISTS__THM4,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0i:$i] : (mem(V0i,A_27a) => ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27b,A_27a),k(A_27b,V0i)),V1P)) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27c,A_27a),k(A_27c,V0i)),V1P)) => (p(ap(c_2Ebool_2E_3F_21(A_27a),V1P)) <=> $true)))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESSES__NEG__DUALITY,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27b)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27b,bool)) => ((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),ap(ap(c_2Ecombin_2Eo(A_27b,bool,bool),c_2Ebool_2E_7E),V1P))) <=> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),V1P))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),ap(ap(c_2Ecombin_2Eo(A_27b,bool,bool),c_2Ebool_2E_7E),V1P))) <=> p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),V1P))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),ap(ap(c_2Ecombin_2Eo(A_27b,bool,bool),c_2Ebool_2E_7E),V1P))) <=> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),V1P))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),ap(ap(c_2Ecombin_2Eo(A_27b,bool,bool),c_2Ebool_2E_7E),V1P))) <=> p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),V1P))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),ap(ap(c_2Ecombin_2Eo(A_27b,bool,bool),c_2Ebool_2E_7E),V1P))) <=> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),V1P))) & (p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),ap(ap(c_2Ecombin_2Eo(A_27b,bool,bool),c_2Ebool_2E_7E),V1P))) <=> p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),V1P)))))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESSES__NEG__REWRITE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27b)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27b,bool)) => ((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),f581(A_27b,V1P))) <=> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),f582(A_27b,V1P)))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),f583(A_27b,V1P))) <=> p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),f584(A_27b,V1P)))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f585(A_27b,V1P))) <=> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f586(A_27b,V1P)))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f587(A_27b,V1P))) <=> p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f588(A_27b,V1P)))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f589(A_27b,V1P))) <=> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f590(A_27b,V1P)))) & (p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f591(A_27b,V1P))) <=> p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f592(A_27b,V1P))))))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESSES__WEAKEN__THM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27b)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27b,bool)) => ((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),V1P)) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),V1P))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),V1P)) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),V1P))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),V1P)) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),V1P))) & (p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),V1P)) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),V1P)))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__EQUATION__EXISTS__POINT,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,A_27a) => ( ! [V1P:$i] : (mem(V1P,arr(A_27a,A_27b)) => ( ! [V2Q:$i] : (mem(V2Q,arr(A_27a,A_27b)) => ((ap(V1P,V0i) = ap(V2Q,V0i)) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(ty_2Eone_2Eone,A_27a),k(ty_2Eone_2Eone,V0i)),f593(A_27b,A_27a,V1P,V2Q)))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__EQUATION__FORALL__POINT,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27b)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27b,A_27c)) => ( ! [V2Q:$i] : (mem(V2Q,arr(A_27b,A_27c)) => (( ! [V3fv:$i] : (mem(V3fv,A_27a) => (~~ (ap(V1P,ap(V0i,V3fv)) = ap(V2Q,ap(V0i,V3fv)))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f594(A_27c,A_27b,V1P,V2Q))))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__EQUATION__EXISTS__GAP,lemma,(( ! [A_27a:del]: ( ! [V0i:$i] : (mem(V0i,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(ty_2Eone_2Eone,A_27a),k(ty_2Eone_2Eone,V0i)),f595(A_27a,V0i)))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__TRIVIAL__EXISTS__POINT,lemma,(( ! [A_27a:del]: ( ! [V0i:$i] : (mem(V0i,A_27a) => ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => (p(ap(V1P,V0i)) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(ty_2Eone_2Eone,A_27a),k(ty_2Eone_2Eone,V0i)),V1P)))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__TRIVIAL__FORALL__POINT,lemma,(( ! [A_27a:del]: ( ! [V0i:$i] : (mem(V0i,A_27a) => ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => ((~~ p(ap(V1P,V0i))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(ty_2Eone_2Eone,A_27a),k(ty_2Eone_2Eone,V0i)),V1P)))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__BOOL,lemma,((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(ty_2Eone_2Eone,bool),k(ty_2Eone_2Eone,c_2Ebool_2ET)),i(bool))) & (p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(ty_2Eone_2Eone,bool),k(ty_2Eone_2Eone,c_2Ebool_2EF)),i(bool))) & (p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(ty_2Eone_2Eone,bool),k(ty_2Eone_2Eone,c_2Ebool_2ET)),i(bool))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(ty_2Eone_2Eone,bool),k(ty_2Eone_2Eone,c_2Ebool_2EF)),i(bool)))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__TWO__CASES,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0y:$i] : (mem(V0y,A_27a) => ( ! [V1Q:$i] : (mem(V1Q,arr(A_27b,A_27a)) => (( ! [V2x:$i] : (mem(V2x,A_27a) => ((V2x = V0y) | (? [V3fv:$i] : (mem(V3fv,A_27b) & (V2x = ap(V1Q,V3fv))))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27b,A_27a),V1Q),f596(A_27a,V0y)))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__ONE__CASE______FORALL__GAP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1Q:$i] : (mem(V1Q,arr(A_27b,A_27a)) => (( ! [V2x:$i] : (mem(V2x,A_27a) => (? [V3fv:$i] : (mem(V3fv,A_27b) & (V2x = ap(V1Q,V3fv)))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27b,A_27a),V1Q),V0P))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__ONE__CASE______EXISTS__GAP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1Q:$i] : (mem(V1Q,arr(A_27b,A_27a)) => (( ! [V2x:$i] : (mem(V2x,A_27a) => (? [V3fv:$i] : (mem(V3fv,A_27b) & (V2x = ap(V1Q,V3fv)))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27b,A_27a),V1Q),V0P))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__NEG,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27b)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27b,bool)) => ((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),f597(A_27b,V1P))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),f598(A_27b,V1P)))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f599(A_27b,V1P))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f600(A_27b,V1P)))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f601(A_27b,V1P))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f602(A_27b,V1P)))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),f603(A_27b,V1P))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),f604(A_27b,V1P)))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f605(A_27b,V1P))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f606(A_27b,V1P)))) & (p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f607(A_27b,V1P))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f608(A_27b,V1P))))))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__CONSTANT__EXISTS,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27b)) => ( ! [V1p:tp__o] : (p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),k(A_27b,inj__o(V1p)))) <=> $true)))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__CONSTANT__FORALL,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27b)) => ( ! [V1p:tp__o] : (p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),k(A_27b,inj__o(V1p)))) <=> $true)))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__DISJ,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27b)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27b,bool)) => ( ! [V2Q:$i] : (mem(V2Q,arr(A_27b,bool)) => ( ! [V3iK:$i] : (mem(V3iK,A_27b) => ( ! [V4q:tp__o] : ( ! [V5p:tp__o] : ((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f601(A_27b,V1P))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f609(A_27b,V1P,V2Q)))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f610(A_27b,V2Q))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f611(A_27b,V1P,V2Q)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),f605(A_27b,V1P))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),f612(A_27b,V2Q)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),f613(A_27b,V1P,V2Q)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f592(A_27b,V1P))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f614(A_27b,V2Q)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f615(A_27b,V1P,V2Q)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(ty_2Eone_2Eone,A_27b),k(ty_2Eone_2Eone,V3iK)),f616(A_27b,V1P))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(ty_2Eone_2Eone,A_27b),k(ty_2Eone_2Eone,V3iK)),f617(A_27b,V2Q)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(ty_2Eone_2Eone,A_27b),k(ty_2Eone_2Eone,V3iK)),f618(A_27b,V1P,V2Q)))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),f619(A_27b,V1P))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),f620(A_27b,V1P,V4q)))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),f621(A_27b,V2Q))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),f622(A_27b,V2Q,V5p)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f623(A_27b,V1P))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f624(A_27b,V2Q)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f625(A_27b,V1P,V2Q)))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f626(A_27b,V1P))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f627(A_27b,V1P,V2Q)))) & (p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f628(A_27b,V2Q))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f629(A_27b,V1P,V2Q))))))))))))))))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__CONJ,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27b)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27b,bool)) => ( ! [V2Q:$i] : (mem(V2Q,arr(A_27b,bool)) => ( ! [V3iK:$i] : (mem(V3iK,A_27b) => ( ! [V4q:tp__o] : ( ! [V5p:tp__o] : ((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f601(A_27b,V1P))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f630(A_27b,V1P,V2Q)))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f610(A_27b,V2Q))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f631(A_27b,V1P,V2Q)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),f605(A_27b,V1P))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),f612(A_27b,V2Q)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),f632(A_27b,V1P,V2Q)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f592(A_27b,V1P))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f614(A_27b,V2Q)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f633(A_27b,V1P,V2Q)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(ty_2Eone_2Eone,A_27b),k(ty_2Eone_2Eone,V3iK)),f616(A_27b,V1P))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(ty_2Eone_2Eone,A_27b),k(ty_2Eone_2Eone,V3iK)),f617(A_27b,V2Q)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(ty_2Eone_2Eone,A_27b),k(ty_2Eone_2Eone,V3iK)),f634(A_27b,V1P,V2Q)))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),f619(A_27b,V1P))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),f635(A_27b,V1P,V4q)))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),f621(A_27b,V2Q))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),f636(A_27b,V2Q,V5p)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f623(A_27b,V1P))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f624(A_27b,V2Q)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f637(A_27b,V1P,V2Q)))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f626(A_27b,V1P))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f638(A_27b,V1P,V2Q)))) & (p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f628(A_27b,V2Q))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f639(A_27b,V1P,V2Q))))))))))))))))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__IMP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27b)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27b,bool)) => ( ! [V2Q:$i] : (mem(V2Q,arr(A_27b,bool)) => ( ! [V3iK:$i] : (mem(V3iK,A_27b) => ( ! [V4q:tp__o] : ( ! [V5p:tp__o] : ((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f601(A_27b,V1P))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f640(A_27b,V1P,V2Q)))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f610(A_27b,V2Q))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f641(A_27b,V1P,V2Q)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),f605(A_27b,V1P))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),f612(A_27b,V2Q)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),f642(A_27b,V1P,V2Q)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f592(A_27b,V1P))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f614(A_27b,V2Q)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f643(A_27b,V1P,V2Q)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(ty_2Eone_2Eone,A_27b),k(ty_2Eone_2Eone,V3iK)),f616(A_27b,V1P))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(ty_2Eone_2Eone,A_27b),k(ty_2Eone_2Eone,V3iK)),f617(A_27b,V2Q)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(ty_2Eone_2Eone,A_27b),k(ty_2Eone_2Eone,V3iK)),f644(A_27b,V1P,V2Q)))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),f619(A_27b,V1P))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),f645(A_27b,V1P,V4q)))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),f621(A_27b,V2Q))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),f646(A_27b,V2Q,V5p)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f623(A_27b,V1P))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f624(A_27b,V2Q)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f647(A_27b,V1P,V2Q)))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f626(A_27b,V1P))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f648(A_27b,V1P,V2Q)))) & (p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f628(A_27b,V2Q))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f649(A_27b,V1P,V2Q))))))))))))))))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__EQUIV,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27b)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27b,bool)) => ( ! [V2Q:$i] : (mem(V2Q,arr(A_27b,bool)) => ( ! [V3P1:$i] : (mem(V3P1,arr(A_27b,bool)) => ( ! [V4P2:$i] : (mem(V4P2,arr(A_27b,bool)) => (((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f584(A_27b,V1P))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f650(A_27b,V2Q)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f651(A_27b,V1P,V2Q)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f603(A_27b,V1P))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f652(A_27b,V2Q)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f653(A_27b,V1P,V2Q)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f590(A_27b,V1P))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f654(A_27b,V2Q)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f655(A_27b,V1P,V2Q)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f656(A_27b,V1P))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f657(A_27b,V2Q)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f658(A_27b,V1P,V2Q)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f659(A_27b,V3P1))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f660(A_27b,V4P2)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f661(A_27b,V3P1,V4P2)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f662(A_27b,V3P1))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f663(A_27b,V4P2)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f664(A_27b,V3P1,V4P2)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f665(A_27b,V3P1))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f666(A_27b,V4P2)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f667(A_27b,V3P1,V4P2)))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f668(A_27b,V3P1))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f669(A_27b,V4P2)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f670(A_27b,V3P1,V4P2))))))))))))))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__COND,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27b)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27b,bool)) => ( ! [V2Q:$i] : (mem(V2Q,arr(A_27b,bool)) => ( ! [V3b:$i] : (mem(V3b,arr(A_27b,bool)) => ( ! [V4bc:tp__o] : (((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f584(A_27b,V1P))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f650(A_27b,V2Q)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f671(A_27b,V1P,V3b,V2Q)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f603(A_27b,V1P))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f652(A_27b,V2Q)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f672(A_27b,V1P,V3b,V2Q)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),f590(A_27b,V1P))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),f654(A_27b,V2Q)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),V0i),f673(A_27b,V4bc,V1P,V2Q)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),f656(A_27b,V1P))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),f657(A_27b,V2Q)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),V0i),f674(A_27b,V4bc,V1P,V2Q)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f616(A_27b,V1P))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f675(A_27b,V2Q)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f676(A_27b,V1P,V3b,V2Q)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f677(A_27b,V1P))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f678(A_27b,V2Q)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f679(A_27b,V1P,V3b,V2Q)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f680(A_27b,V3b))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f621(A_27b,V2Q)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f681(A_27b,V1P,V3b,V2Q)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f682(A_27b,V3b))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f624(A_27b,V2Q)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f683(A_27b,V1P,V3b,V2Q)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f684(A_27b,V3b))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f685(A_27b,V1P)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),V0i),f686(A_27b,V1P,V3b,V2Q)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f687(A_27b,V3b))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f688(A_27b,V1P)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),V0i),f689(A_27b,V1P,V3b,V2Q)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f690(A_27b,V3b))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f691(A_27b,V1P)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f692(A_27b,V1P,V3b,V2Q)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f693(A_27b,V3b))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f694(A_27b,V2Q)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f695(A_27b,V1P,V3b,V2Q)))) & (((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),V0i),f696(A_27b,V3b))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f697(A_27b,V2Q)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f698(A_27b,V1P,V3b,V2Q)))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f699(A_27b,V3b))) & p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f700(A_27b,V1P)))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),V0i),f701(A_27b,V1P,V3b,V2Q)))))))))))))))))))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__FORALL______NEW__FV,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0iy:$i] : (mem(V0iy,arr(A_27a,arr(A_27b,A_27c))) => ( ! [V1P:$i] : (mem(V1P,arr(A_27c,arr(A_27a,bool))) => ((( ! [V2y:$i] : (mem(V2y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27b,A_27c),ap(V0iy,V2y)),f702(A_27c,A_27a,V1P,V2y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(ty_2Epair_2Eprod(A_27a,A_27b),A_27c),f703(A_27c,A_27a,A_27b,V0iy)),f705(A_27c,A_27a,V1P)))) & ((( ! [V7y:$i] : (mem(V7y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27b,A_27c),ap(V0iy,V7y)),f706(A_27c,A_27a,V1P,V7y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(ty_2Epair_2Eprod(A_27a,A_27b),A_27c),f707(A_27c,A_27a,A_27b,V0iy)),f709(A_27c,A_27a,V1P)))) & ((( ! [V12y:$i] : (mem(V12y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27b,A_27c),ap(V0iy,V12y)),f710(A_27c,A_27a,V1P,V12y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27c),f711(A_27c,A_27a,A_27b,V0iy)),f713(A_27c,A_27a,V1P)))) & (( ! [V17y:$i] : (mem(V17y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27b,A_27c),ap(V0iy,V17y)),f714(A_27c,A_27a,V1P,V17y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27c),f715(A_27c,A_27a,A_27b,V0iy)),f717(A_27c,A_27a,V1P)))))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__FORALL______NEW__FV__1,lemma,(( ! [A_27a:del]: ( ! [A_27c:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27c)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27c,arr(A_27a,bool))) => ((( ! [V2y:$i] : (mem(V2y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(ty_2Eone_2Eone,A_27c),k(ty_2Eone_2Eone,ap(V0i,V2y))),f718(A_27c,A_27a,V1P,V2y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27c),V0i),f705(A_27c,A_27a,V1P)))) & ((( ! [V7y:$i] : (mem(V7y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(ty_2Eone_2Eone,A_27c),k(ty_2Eone_2Eone,ap(V0i,V7y))),f719(A_27c,A_27a,V1P,V7y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27c),V0i),f709(A_27c,A_27a,V1P)))) & ((( ! [V12y:$i] : (mem(V12y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(ty_2Eone_2Eone,A_27c),k(ty_2Eone_2Eone,ap(V0i,V12y))),f720(A_27c,A_27a,V1P,V12y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27c),V0i),f713(A_27c,A_27a,V1P)))) & (( ! [V17y:$i] : (mem(V17y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(ty_2Eone_2Eone,A_27c),k(ty_2Eone_2Eone,ap(V0i,V17y))),f721(A_27c,A_27a,V1P,V17y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27c),V0i),f717(A_27c,A_27a,V1P))))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__FORALL,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27b,A_27c)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27c,arr(A_27a,bool))) => ( ! [V2iK:$i] : (mem(V2iK,A_27c) => ((( ! [V3y:$i] : (mem(V3y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27b,A_27c),V0i),f722(A_27c,A_27a,V1P,V3y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27b,A_27c),V0i),f705(A_27c,A_27a,V1P)))) & ((( ! [V7y:$i] : (mem(V7y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27b,A_27c),V0i),f706(A_27c,A_27a,V1P,V7y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27b,A_27c),V0i),f724(A_27c,A_27a,V1P)))) & ((( ! [V11y:$i] : (mem(V11y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27b,A_27c),V0i),f725(A_27c,A_27a,V1P,V11y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27b,A_27c),V0i),f727(A_27c,A_27a,V1P)))) & ((( ! [V15y:$i] : (mem(V15y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27b,A_27c),V0i),f728(A_27c,A_27a,V1P,V15y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27b,A_27c),V0i),f730(A_27c,A_27a,V1P)))) & ((( ! [V19y:$i] : (mem(V19y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(ty_2Eone_2Eone,A_27c),k(ty_2Eone_2Eone,V2iK)),f731(A_27c,A_27a,V1P,V19y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(ty_2Eone_2Eone,A_27c),k(ty_2Eone_2Eone,V2iK)),f733(A_27c,A_27a,V1P)))) & (( ! [V25y:$i] : (mem(V25y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27b,A_27c),V0i),f734(A_27c,A_27a,V1P,V25y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27b,A_27c),V0i),f736(A_27c,A_27a,V1P)))))))))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__EXISTS______NEW__FV,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0iy:$i] : (mem(V0iy,arr(A_27a,arr(A_27b,A_27c))) => ( ! [V1P:$i] : (mem(V1P,arr(A_27c,arr(A_27a,bool))) => ((( ! [V2y:$i] : (mem(V2y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27b,A_27c),ap(V0iy,V2y)),f702(A_27c,A_27a,V1P,V2y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(ty_2Epair_2Eprod(A_27a,A_27b),A_27c),f703(A_27c,A_27a,A_27b,V0iy)),f737(A_27c,A_27a,V1P)))) & ((( ! [V7y:$i] : (mem(V7y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27b,A_27c),ap(V0iy,V7y)),f706(A_27c,A_27a,V1P,V7y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(ty_2Epair_2Eprod(A_27a,A_27b),A_27c),f707(A_27c,A_27a,A_27b,V0iy)),f738(A_27c,A_27a,V1P)))) & ((( ! [V12y:$i] : (mem(V12y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27b,A_27c),ap(V0iy,V12y)),f710(A_27c,A_27a,V1P,V12y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27c),f711(A_27c,A_27a,A_27b,V0iy)),f739(A_27c,A_27a,V1P)))) & (( ! [V17y:$i] : (mem(V17y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27b,A_27c),ap(V0iy,V17y)),f714(A_27c,A_27a,V1P,V17y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27c),f715(A_27c,A_27a,A_27b,V0iy)),f740(A_27c,A_27a,V1P)))))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__EXISTS______NEW__FV__1,lemma,(( ! [A_27a:del]: ( ! [A_27c:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27a,A_27c)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27c,arr(A_27a,bool))) => ((( ! [V2y:$i] : (mem(V2y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(ty_2Eone_2Eone,A_27c),k(ty_2Eone_2Eone,ap(V0i,V2y))),f718(A_27c,A_27a,V1P,V2y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27c),V0i),f737(A_27c,A_27a,V1P)))) & ((( ! [V7y:$i] : (mem(V7y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(ty_2Eone_2Eone,A_27c),k(ty_2Eone_2Eone,ap(V0i,V7y))),f719(A_27c,A_27a,V1P,V7y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27c),V0i),f738(A_27c,A_27a,V1P)))) & ((( ! [V12y:$i] : (mem(V12y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(ty_2Eone_2Eone,A_27c),k(ty_2Eone_2Eone,ap(V0i,V12y))),f720(A_27c,A_27a,V1P,V12y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27c),V0i),f739(A_27c,A_27a,V1P)))) & (( ! [V17y:$i] : (mem(V17y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(ty_2Eone_2Eone,A_27c),k(ty_2Eone_2Eone,ap(V0i,V17y))),f721(A_27c,A_27a,V1P,V17y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27c),V0i),f740(A_27c,A_27a,V1P))))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__EXISTS,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27b,A_27c)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27c,arr(A_27a,bool))) => ( ! [V2iK:$i] : (mem(V2iK,A_27c) => ((( ! [V3y:$i] : (mem(V3y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27b,A_27c),V0i),f722(A_27c,A_27a,V1P,V3y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27b,A_27c),V0i),f737(A_27c,A_27a,V1P)))) & ((( ! [V7y:$i] : (mem(V7y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27b,A_27c),V0i),f706(A_27c,A_27a,V1P,V7y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27b,A_27c),V0i),f741(A_27c,A_27a,V1P)))) & ((( ! [V11y:$i] : (mem(V11y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27b,A_27c),V0i),f725(A_27c,A_27a,V1P,V11y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27b,A_27c),V0i),f742(A_27c,A_27a,V1P)))) & ((( ! [V15y:$i] : (mem(V15y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27b,A_27c),V0i),f728(A_27c,A_27a,V1P,V15y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27b,A_27c),V0i),f743(A_27c,A_27a,V1P)))) & ((( ! [V19y:$i] : (mem(V19y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(ty_2Eone_2Eone,A_27c),k(ty_2Eone_2Eone,V2iK)),f731(A_27c,A_27a,V1P,V19y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(ty_2Eone_2Eone,A_27c),k(ty_2Eone_2Eone,V2iK)),f744(A_27c,A_27a,V1P)))) & (( ! [V25y:$i] : (mem(V25y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27b,A_27c),V0i),f734(A_27c,A_27a,V1P,V25y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27b,A_27c),V0i),f745(A_27c,A_27a,V1P)))))))))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__EXISTS__UNIQUE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27b,A_27c)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27c,arr(A_27a,bool))) => ((( ! [V2y:$i] : (mem(V2y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27b,A_27c),V0i),f702(A_27c,A_27a,V1P,V2y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27b,A_27c),V0i),f747(A_27c,A_27a,V1P)))) & (( ! [V6y:$i] : (mem(V6y,A_27a) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27b,A_27c),V0i),f748(A_27c,A_27a,V1P,V6y))))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27b,A_27c),V0i),f750(A_27c,A_27a,V1P)))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__ELIM__UNIT,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(ty_2Epair_2Eprod(A_27a,ty_2Eone_2Eone),A_27b)) => ( ! [V1vt:$i] : (mem(V1vt,arr(A_27b,bool)) => ((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(ty_2Epair_2Eprod(A_27a,ty_2Eone_2Eone),A_27b),V0i),V1vt)) <=> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27a,A_27b),f751(A_27b,A_27a,V0i)),V1vt))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(ty_2Epair_2Eprod(A_27a,ty_2Eone_2Eone),A_27b),V0i),V1vt)) <=> p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27a,A_27b),f752(A_27b,A_27a,V0i)),V1vt))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(ty_2Epair_2Eprod(A_27a,ty_2Eone_2Eone),A_27b),V0i),V1vt)) <=> p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(A_27a,A_27b),f753(A_27b,A_27a,V0i)),V1vt))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(ty_2Epair_2Eprod(A_27a,ty_2Eone_2Eone),A_27b),V0i),V1vt)) <=> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(A_27a,A_27b),f754(A_27b,A_27a,V0i)),V1vt))) & ((p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(ty_2Epair_2Eprod(A_27a,ty_2Eone_2Eone),A_27b),V0i),V1vt)) <=> p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27a,A_27b),f755(A_27b,A_27a,V0i)),V1vt))) & (p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(ty_2Epair_2Eprod(A_27a,ty_2Eone_2Eone),A_27b),V0i),V1vt)) <=> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27a,A_27b),f756(A_27b,A_27a,V0i)),V1vt)))))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__STRENGTHEN__EXISTS__POINT,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27b,A_27a)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => ( ! [V2Q:$i] : (mem(V2Q,arr(A_27a,bool)) => (( ! [V3x:$i] : (mem(V3x,A_27a) => (p(ap(V1P,V3x)) => p(ap(V2Q,V3x))))) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27b,A_27a),V0i),V1P)) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(A_27b,A_27a),V0i),V2Q)))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__STRENGTHEN__FORALL__GAP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27b,A_27a)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => ( ! [V2Q:$i] : (mem(V2Q,arr(A_27a,bool)) => (( ! [V3x:$i] : (mem(V3x,A_27a) => (p(ap(V1P,V3x)) => p(ap(V2Q,V3x))))) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27b,A_27a),V0i),V1P)) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(A_27b,A_27a),V0i),V2Q)))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27b,A_27a)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => ( ! [V2Q:$i] : (mem(V2Q,arr(A_27a,bool)) => (( ! [V3x:$i] : (mem(V3x,A_27a) => (p(ap(V2Q,V3x)) => p(ap(V1P,V3x))))) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27b,A_27a),V0i),V1P)) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(A_27b,A_27a),V0i),V2Q)))))))))))))).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__EXISTS__GAP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:$i] : (mem(V0i,arr(A_27b,A_27a)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => ( ! [V2Q:$i] : (mem(V2Q,arr(A_27a,bool)) => (( ! [V3x:$i] : (mem(V3x,A_27a) => (p(ap(V2Q,V3x)) => p(ap(V1P,V3x))))) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27b,A_27a),V0i),V1P)) => p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(A_27b,A_27a),V0i),V2Q)))))))))))))).
tff(conj_thm_2EquantHeuristics_2ECONJ__NOT__OR__THM,lemma,(( ! [V0A:tp__o] : ( ! [V1B:tp__o] : ((p(inj__o(V0A)) & p(inj__o(V1B))) <=> (~~ ((~~ p(inj__o(V0A))) | (~~ p(inj__o(V1B)))))))))).
tff(conj_thm_2EquantHeuristics_2EEXISTS__NOT__FORALL__THM,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ((? [V1x:$i] : (mem(V1x,A_27a) & p(ap(V0P,V1x)))) <=> (~~ ( ! [V2x:$i] : (mem(V2x,A_27a) => (~~ p(ap(V0P,V2x)))))))))))).
tff(conj_thm_2EquantHeuristics_2EMOVE__EXISTS__IMP__THM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,arr(A_27b,bool))) => ( ! [V1R:$i] : (mem(V1R,arr(A_27b,bool)) => ( ! [V2Q:$i] : (mem(V2Q,arr(A_27a,bool)) => ((? [V3x:$i] : (mem(V3x,A_27a) & (( ! [V4y:$i] : (mem(V4y,A_27b) => ((~~ p(ap(ap(V0P,V3x),V4y))) => p(ap(V1R,V4y))))) => p(ap(V2Q,V3x))))) <=> (( ! [V5y:$i] : (mem(V5y,A_27b) => ((~~ ( ! [V6x:$i] : (mem(V6x,A_27a) => p(ap(ap(V0P,V6x),V5y))))) => p(ap(V1R,V5y))))) => (? [V7x:$i] : (mem(V7x,A_27a) & p(ap(V2Q,V7x)))))))))))))))).
tff(conj_thm_2EquantHeuristics_2EUNWIND__EXISTS__THM,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,A_27a) => ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => ((? [V2x:$i] : (mem(V2x,A_27a) & p(ap(V1P,V2x)))) <=> (( ! [V3x:$i] : (mem(V3x,A_27a) => ((~~ (V3x = V0a)) => (~~ p(ap(V1P,V3x)))))) => p(ap(V1P,V0a))))))))))).
tff(conj_thm_2EquantHeuristics_2ELEFT__IMP__AND__INTRO,lemma,(( ! [V0x:tp__o] : ( ! [V1t1:tp__o] : ( ! [V2t2:tp__o] : ((p(inj__o(V1t1)) => p(inj__o(V2t2))) => ((p(inj__o(V0x)) & p(inj__o(V1t1))) => (p(inj__o(V0x)) & p(inj__o(V2t2)))))))))).
tff(conj_thm_2EquantHeuristics_2ERIGHT__IMP__AND__INTRO,lemma,(( ! [V0x:tp__o] : ( ! [V1t1:tp__o] : ( ! [V2t2:tp__o] : ((p(inj__o(V1t1)) => p(inj__o(V2t2))) => ((p(inj__o(V1t1)) & p(inj__o(V0x))) => (p(inj__o(V2t2)) & p(inj__o(V0x)))))))))).
tff(conj_thm_2EquantHeuristics_2ELEFT__IMP__OR__INTRO,lemma,(( ! [V0x:tp__o] : ( ! [V1t1:tp__o] : ( ! [V2t2:tp__o] : ((p(inj__o(V1t1)) => p(inj__o(V2t2))) => ((p(inj__o(V0x)) | p(inj__o(V1t1))) => (p(inj__o(V0x)) | p(inj__o(V2t2)))))))))).
tff(conj_thm_2EquantHeuristics_2ERIGHT__IMP__OR__INTRO,lemma,(( ! [V0x:tp__o] : ( ! [V1t1:tp__o] : ( ! [V2t2:tp__o] : ((p(inj__o(V1t1)) => p(inj__o(V2t2))) => ((p(inj__o(V1t1)) | p(inj__o(V0x))) => (p(inj__o(V2t2)) | p(inj__o(V0x)))))))))).
tff(conj_thm_2EquantHeuristics_2EIMP__NEG__CONTRA,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1i:$i] : (mem(V1i,A_27a) => ( ! [V2x:$i] : (mem(V2x,A_27a) => ((~~ p(ap(V0P,V1i))) => (p(ap(V0P,V2x)) => (~~ (V2x = V1i))))))))))))).
tff(conj_thm_2EquantHeuristics_2EDISJ__IMP__INTRO,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1Q:$i] : (mem(V1Q,arr(A_27a,bool)) => ( ! [V2y:$i] : (mem(V2y,A_27a) => (( ! [V3x:$i] : (mem(V3x,A_27a) => (p(ap(V0P,V3x)) | p(ap(V1Q,V3x))))) => (((~~ p(ap(V0P,V2y))) => p(ap(V1Q,V2y))) & ((~~ p(ap(V1Q,V2y))) => p(ap(V0P,V2y)))))))))))))).
tff(ax_thm_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS__def,axiom,( ! [A_27a:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1i:$i] : (mem(V1i,A_27a) => ( ! [V2P:tp__o] : (p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS(A_27a),V0v),V1i),inj__o(V2P))) <=> (p(inj__o(V2P)) => (V0v = V1i)))))))))).
tff(conj_thm_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS__ALT__DEF,lemma,(( ! [A_27a:del]: ( ! [V0i:$i] : (mem(V0i,A_27a) => ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => (( ! [V2v:$i] : (mem(V2v,A_27a) => p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS(A_27a),V2v),V0i),ap(V1P,V2v))))) <=> p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(ty_2Eone_2Eone,A_27a),ap(c_2Ecombin_2EK(A_27a,ty_2Eone_2Eone),V0i)),f757(A_27a,V1P))))))))))).
tff(ax_thm_2EquantHeuristics_2ESIMPLE__GUESS__FORALL__def,axiom,( ! [A_27a:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1i:$i] : (mem(V1i,A_27a) => ( ! [V2P:tp__o] : (p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__FORALL(A_27a),V0v),V1i),inj__o(V2P))) <=> ((~~ p(inj__o(V2P))) => (V0v = V1i)))))))))).
tff(conj_thm_2EquantHeuristics_2ESIMPLE__GUESS__FORALL__ALT__DEF,lemma,(( ! [A_27a:del]: ( ! [V0i:$i] : (mem(V0i,A_27a) => ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => (( ! [V2v:$i] : (mem(V2v,A_27a) => p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__FORALL(A_27a),V2v),V0i),ap(V1P,V2v))))) <=> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(ty_2Eone_2Eone,A_27a),ap(c_2Ecombin_2EK(A_27a,ty_2Eone_2Eone),V0i)),f757(A_27a,V1P))))))))))).
tff(conj_thm_2EquantHeuristics_2ESIMPLE__GUESS__FORALL__THM,lemma,(( ! [A_27a:del]: ( ! [V0i:$i] : (mem(V0i,A_27a) => ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => (( ! [V2v:$i] : (mem(V2v,A_27a) => p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__FORALL(A_27a),V2v),V0i),ap(V1P,V2v))))) => (( ! [V3v:$i] : (mem(V3v,A_27a) => p(ap(V1P,V3v)))) <=> p(ap(V1P,V0i))))))))))).
tff(conj_thm_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS__THM,lemma,(( ! [A_27a:del]: ( ! [V0i:$i] : (mem(V0i,A_27a) => ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => (( ! [V2v:$i] : (mem(V2v,A_27a) => p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS(A_27a),V2v),V0i),ap(V1P,V2v))))) => ((? [V3v:$i] : (mem(V3v,A_27a) & p(ap(V1P,V3v)))) <=> p(ap(V1P,V0i))))))))))).
tff(conj_thm_2EquantHeuristics_2ESIMPLE__GUESS__UEXISTS__THM,lemma,(( ! [A_27a:del]: ( ! [V0i:$i] : (mem(V0i,A_27a) => ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => (( ! [V2v:$i] : (mem(V2v,A_27a) => p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS(A_27a),V2v),V0i),ap(V1P,V2v))))) => (p(ap(c_2Ebool_2E_3F_21(A_27a),f757(A_27a,V1P))) <=> p(ap(V1P,V0i))))))))))).
tff(conj_thm_2EquantHeuristics_2ESIMPLE__GUESS__SELECT__THM,lemma,(( ! [A_27a:del]: ( ! [V0i:$i] : (mem(V0i,A_27a) => ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => (( ! [V2v:$i] : (mem(V2v,A_27a) => p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS(A_27a),V2v),V0i),ap(V1P,V2v))))) => (ap(c_2Emin_2E_40(A_27a),f757(A_27a,V1P)) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),ap(V1P,V0i)),V0i),ap(c_2Emin_2E_40(A_27a),k(A_27a,c_2Ebool_2EF)))))))))))).
tff(conj_thm_2EquantHeuristics_2ESIMPLE__GUESS__SOME__THM,lemma,(( ! [A_27a:del]: ( ! [V0i:$i] : (mem(V0i,A_27a) => ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => (( ! [V2v:$i] : (mem(V2v,A_27a) => p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS(A_27a),V2v),V0i),ap(V1P,V2v))))) => (ap(c_2Eoption_2Esome(A_27a),f757(A_27a,V1P)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(A_27a)),ap(V1P,V0i)),ap(c_2Eoption_2ESOME(A_27a),V0i)),c_2Eoption_2ENONE(A_27a))))))))))).
tff(conj_thm_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS__EQ__1,lemma,(( ! [A_27a:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1i:$i] : (mem(V1i,A_27a) => p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS(A_27a),V0v),V1i),ap(ap(c_2Emin_2E_3D(A_27a),V0v),V1i)))))))))).
tff(conj_thm_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS__EQ__2,lemma,(( ! [A_27a:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1i:$i] : (mem(V1i,A_27a) => p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS(A_27a),V0v),V1i),ap(ap(c_2Emin_2E_3D(A_27a),V1i),V0v)))))))))).
tff(conj_thm_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS__EQ__T,lemma,(( ! [V0v:tp__o] : p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS(bool),inj__o(V0v)),inj__o(fo__c_2Ebool_2ET)),inj__o(V0v)))))).
tff(conj_thm_2EquantHeuristics_2ESIMPLE__GUESS__FORALL__NEG,lemma,(( ! [A_27a:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1i:$i] : (mem(V1i,A_27a) => ( ! [V2P:tp__o] : (p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS(A_27a),V0v),V1i),inj__o(V2P))) => p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__FORALL(A_27a),V0v),V1i),ap(c_2Ebool_2E_7E,inj__o(V2P))))))))))))).
tff(conj_thm_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS__NEG,lemma,(( ! [A_27a:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1i:$i] : (mem(V1i,A_27a) => ( ! [V2P:tp__o] : (p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__FORALL(A_27a),V0v),V1i),inj__o(V2P))) => p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS(A_27a),V0v),V1i),ap(c_2Ebool_2E_7E,inj__o(V2P))))))))))))).
tff(conj_thm_2EquantHeuristics_2ESIMPLE__GUESS__FORALL__OR__1,lemma,(( ! [A_27a:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1i:$i] : (mem(V1i,A_27a) => ( ! [V2P1:tp__o] : ( ! [V3P2:tp__o] : (p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__FORALL(A_27a),V0v),V1i),inj__o(V2P1))) => p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__FORALL(A_27a),V0v),V1i),ap(ap(c_2Ebool_2E_5C_2F,inj__o(V2P1)),inj__o(V3P2)))))))))))))).
tff(conj_thm_2EquantHeuristics_2ESIMPLE__GUESS__FORALL__OR__2,lemma,(( ! [A_27a:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1i:$i] : (mem(V1i,A_27a) => ( ! [V2P1:tp__o] : ( ! [V3P2:tp__o] : (p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__FORALL(A_27a),V0v),V1i),inj__o(V3P2))) => p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__FORALL(A_27a),V0v),V1i),ap(ap(c_2Ebool_2E_5C_2F,inj__o(V2P1)),inj__o(V3P2)))))))))))))).
tff(conj_thm_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS__AND__1,lemma,(( ! [A_27a:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1i:$i] : (mem(V1i,A_27a) => ( ! [V2P1:tp__o] : ( ! [V3P2:tp__o] : (p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS(A_27a),V0v),V1i),inj__o(V2P1))) => p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS(A_27a),V0v),V1i),ap(ap(c_2Ebool_2E_2F_5C,inj__o(V2P1)),inj__o(V3P2)))))))))))))).
tff(conj_thm_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS__AND__2,lemma,(( ! [A_27a:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1i:$i] : (mem(V1i,A_27a) => ( ! [V2P1:tp__o] : ( ! [V3P2:tp__o] : (p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS(A_27a),V0v),V1i),inj__o(V3P2))) => p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS(A_27a),V0v),V1i),ap(ap(c_2Ebool_2E_2F_5C,inj__o(V2P1)),inj__o(V3P2)))))))))))))).
tff(conj_thm_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS__EXISTS,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1i:$i] : (mem(V1i,A_27a) => ( ! [V2P:$i] : (mem(V2P,arr(A_27b,bool)) => (( ! [V3v2:$i] : (mem(V3v2,A_27b) => p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS(A_27a),V0v),V1i),ap(V2P,V3v2))))) => p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS(A_27a),V0v),V1i),ap(c_2Ebool_2E_3F(A_27b),f758(A_27b,V2P))))))))))))))).
tff(conj_thm_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS__FORALL,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1i:$i] : (mem(V1i,A_27a) => ( ! [V2P:$i] : (mem(V2P,arr(A_27b,bool)) => (( ! [V3v2:$i] : (mem(V3v2,A_27b) => p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS(A_27a),V0v),V1i),ap(V2P,V3v2))))) => p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS(A_27a),V0v),V1i),ap(c_2Ebool_2E_21(A_27b),f758(A_27b,V2P))))))))))))))).
tff(conj_thm_2EquantHeuristics_2ESIMPLE__GUESS__FORALL__EXISTS,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1i:$i] : (mem(V1i,A_27a) => ( ! [V2P:$i] : (mem(V2P,arr(A_27b,bool)) => (( ! [V3v2:$i] : (mem(V3v2,A_27b) => p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__FORALL(A_27a),V0v),V1i),ap(V2P,V3v2))))) => p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__FORALL(A_27a),V0v),V1i),ap(c_2Ebool_2E_3F(A_27b),f758(A_27b,V2P))))))))))))))).
tff(conj_thm_2EquantHeuristics_2ESIMPLE__GUESS__FORALL__FORALL,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1i:$i] : (mem(V1i,A_27a) => ( ! [V2P:$i] : (mem(V2P,arr(A_27b,bool)) => (( ! [V3v2:$i] : (mem(V3v2,A_27b) => p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__FORALL(A_27a),V0v),V1i),ap(V2P,V3v2))))) => p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__FORALL(A_27a),V0v),V1i),ap(c_2Ebool_2E_21(A_27b),f758(A_27b,V2P))))))))))))))).
tff(conj_thm_2EquantHeuristics_2ESIMPLE__GUESS__FORALL__IMP__1,lemma,(( ! [A_27a:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1i:$i] : (mem(V1i,A_27a) => ( ! [V2P1:tp__o] : ( ! [V3P2:tp__o] : (p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS(A_27a),V0v),V1i),inj__o(V2P1))) => p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__FORALL(A_27a),V0v),V1i),ap(ap(c_2Emin_2E_3D_3D_3E,inj__o(V2P1)),inj__o(V3P2)))))))))))))).
tff(conj_thm_2EquantHeuristics_2ESIMPLE__GUESS__FORALL__IMP__2,lemma,(( ! [A_27a:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1i:$i] : (mem(V1i,A_27a) => ( ! [V2P1:tp__o] : ( ! [V3P2:tp__o] : (p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__FORALL(A_27a),V0v),V1i),inj__o(V3P2))) => p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__FORALL(A_27a),V0v),V1i),ap(ap(c_2Emin_2E_3D_3D_3E,inj__o(V2P1)),inj__o(V3P2)))))))))))))).
tff(conj_thm_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS__EQ__FUN,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1i:$i] : (mem(V1i,A_27a) => ( ! [V2t1:$i] : (mem(V2t1,A_27b) => ( ! [V3t2:$i] : (mem(V3t2,A_27b) => ( ! [V4f:$i] : (mem(V4f,arr(A_27b,A_27c)) => (p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS(A_27a),V0v),V1i),ap(ap(c_2Emin_2E_3D(A_27c),ap(V4f,V2t1)),ap(V4f,V3t2)))) => p(ap(ap(ap(c_2EquantHeuristics_2ESIMPLE__GUESS__EXISTS(A_27a),V0v),V1i),ap(ap(c_2Emin_2E_3D(A_27b),V2t1),V3t2))))))))))))))))))).
tff(ax_thm_2EquantHeuristics_2EIS__REMOVABLE__QUANT__FUN__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => (p(ap(c_2EquantHeuristics_2EIS__REMOVABLE__QUANT__FUN(A_27a,A_27b),V0f)) <=> ( ! [V1v:$i] : (mem(V1v,A_27b) => (? [V2x:$i] : (mem(V2x,A_27a) & (ap(V0f,V2x) = V1v))))))))))).
tff(conj_thm_2EquantHeuristics_2EIS__REMOVABLE__QUANT__FUN______EXISTS__THM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27b,bool)) => (p(ap(c_2EquantHeuristics_2EIS__REMOVABLE__QUANT__FUN(A_27a,A_27b),V0f)) => ((? [V2x:$i] : (mem(V2x,A_27a) & p(ap(V1P,ap(V0f,V2x))))) <=> (? [V3x_27:$i] : (mem(V3x_27,A_27b) & p(ap(V1P,V3x_27)))))))))))))).
tff(conj_thm_2EquantHeuristics_2EIS__REMOVABLE__QUANT__FUN______FORALL__THM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27b,bool)) => (p(ap(c_2EquantHeuristics_2EIS__REMOVABLE__QUANT__FUN(A_27a,A_27b),V0f)) => (( ! [V2x:$i] : (mem(V2x,A_27a) => p(ap(V1P,ap(V0f,V2x))))) <=> ( ! [V3x_27:$i] : (mem(V3x_27,A_27b) => p(ap(V1P,V3x_27)))))))))))))).
tff(conj_thm_2EquantHeuristics_2EPAIR__EQ__EXPAND,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1y:$i] : (mem(V1y,A_27b) => ( ! [V2X:$i] : (mem(V2X,ty_2Epair_2Eprod(A_27a,A_27b)) => (((ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V0x),V1y) = V2X) <=> ((V0x = ap(c_2Epair_2EFST(A_27a,A_27b),V2X)) & (V1y = ap(c_2Epair_2ESND(A_27a,A_27b),V2X)))) & ((V2X = ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V0x),V1y)) <=> ((ap(c_2Epair_2EFST(A_27a,A_27b),V2X) = V0x) & (ap(c_2Epair_2ESND(A_27a,A_27b),V2X) = V1y)))))))))))))).
tff(conj_thm_2EquantHeuristics_2EPAIR__EQ__SIMPLE__EXPAND,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1y:$i] : (mem(V1y,A_27b) => ( ! [V2y_27:$i] : (mem(V2y_27,A_27b) => ( ! [V3X:$i] : (mem(V3X,ty_2Epair_2Eprod(A_27a,A_27b)) => (((ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V0x),V1y) = ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V0x),V2y_27)) <=> (V1y = V2y_27)) & (((ap(ap(c_2Epair_2E_2C(A_27b,A_27a),V1y),V0x) = ap(ap(c_2Epair_2E_2C(A_27b,A_27a),V2y_27),V0x)) <=> (V1y = V2y_27)) & (((ap(ap(c_2Epair_2E_2C(A_27a,A_27b),ap(c_2Epair_2EFST(A_27a,A_27b),V3X)),V1y) = V3X) <=> (V1y = ap(c_2Epair_2ESND(A_27a,A_27b),V3X))) & (((ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V0x),ap(c_2Epair_2ESND(A_27a,A_27b),V3X)) = V3X) <=> (V0x = ap(c_2Epair_2EFST(A_27a,A_27b),V3X))) & (((V3X = ap(ap(c_2Epair_2E_2C(A_27a,A_27b),ap(c_2Epair_2EFST(A_27a,A_27b),V3X)),V1y)) <=> (ap(c_2Epair_2ESND(A_27a,A_27b),V3X) = V1y)) & ((V3X = ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V0x),ap(c_2Epair_2ESND(A_27a,A_27b),V3X))) <=> (ap(c_2Epair_2EFST(A_27a,A_27b),V3X) = V0x))))))))))))))))))).
tff(conj_thm_2EquantHeuristics_2EIS__SOME__EQ__NOT__NONE,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,ty_2Eoption_2Eoption(A_27a)) => (p(ap(c_2Eoption_2EIS__SOME(A_27a),V0x)) <=> (~~ (V0x = c_2Eoption_2ENONE(A_27a))))))))).
tff(conj_thm_2EquantHeuristics_2EISL__exists,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,ty_2Esum_2Esum(A_27a,A_27b)) => (p(ap(c_2Esum_2EISL(A_27a,A_27b),V0x)) <=> (? [V1l:$i] : (mem(V1l,A_27a) & (V0x = ap(c_2Esum_2EINL(A_27a,A_27b),V1l))))))))))).
tff(conj_thm_2EquantHeuristics_2EISR__exists,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,ty_2Esum_2Esum(A_27a,A_27b)) => (p(ap(c_2Esum_2EISR(A_27a,A_27b),V0x)) <=> (? [V1r:$i] : (mem(V1r,A_27b) & (V0x = ap(c_2Esum_2EINR(A_27a,A_27b),V1r))))))))))).
tff(conj_thm_2EquantHeuristics_2EINL__NEQ__ELIM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,ty_2Esum_2Esum(A_27a,A_27b)) => ((( ! [V1l:$i] : (mem(V1l,A_27a) => (~~ (V0x = ap(c_2Esum_2EINL(A_27a,A_27b),V1l))))) <=> p(ap(c_2Esum_2EISR(A_27a,A_27b),V0x))) & (( ! [V2l:$i] : (mem(V2l,A_27a) => (~~ (ap(c_2Esum_2EINL(A_27a,A_27b),V2l) = V0x)))) <=> p(ap(c_2Esum_2EISR(A_27a,A_27b),V0x)))))))))).
tff(conj_thm_2EquantHeuristics_2EINR__NEQ__ELIM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,ty_2Esum_2Esum(A_27b,A_27a)) => ((( ! [V1r:$i] : (mem(V1r,A_27a) => (~~ (V0x = ap(c_2Esum_2EINR(A_27b,A_27a),V1r))))) <=> p(ap(c_2Esum_2EISL(A_27b,A_27a),V0x))) & (( ! [V2r:$i] : (mem(V2r,A_27a) => (~~ (ap(c_2Esum_2EINR(A_27b,A_27a),V2r) = V0x)))) <=> p(ap(c_2Esum_2EISL(A_27b,A_27a),V0x)))))))))).
tff(conj_thm_2EquantHeuristics_2ELENGTH__LE__PLUS,lemma,(( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2l:$i] : (mem(V2l,ty_2Elist_2Elist(A_27a)) => (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m))),ap(c_2Elist_2ELENGTH(A_27a),V2l))) <=> (? [V3l1:$i] : (mem(V3l1,ty_2Elist_2Elist(A_27a)) & (? [V4l2:$i] : (mem(V4l2,ty_2Elist_2Elist(A_27a)) & ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V3l1)) = V0n) & (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1m)),ap(c_2Elist_2ELENGTH(A_27a),V4l2))) & (V2l = ap(ap(c_2Elist_2EAPPEND(A_27a),V3l1),V4l2)))))))))))))))).
tff(conj_thm_2EquantHeuristics_2ELENGTH__LE__NUM,lemma,(( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0n)),ap(c_2Elist_2ELENGTH(A_27a),V1l))) <=> (? [V2l1:$i] : (mem(V2l1,ty_2Elist_2Elist(A_27a)) & (? [V3l2:$i] : (mem(V3l2,ty_2Elist_2Elist(A_27a)) & ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V2l1)) = V0n) & (V1l = ap(ap(c_2Elist_2EAPPEND(A_27a),V2l1),V3l2)))))))))))))).
tff(conj_thm_2EquantHeuristics_2ELENGTH__NIL__SYM,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ((fo__c_2Enum_2E0 = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (V0l = c_2Elist_2ENIL(A_27a)))))))).
tff(conj_thm_2EquantHeuristics_2ELIST__LENGTH__COMPARE__1,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ((p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Elist_2ELENGTH(A_27a),V0l)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) <=> (V0l = c_2Elist_2ENIL(A_27a))) & ((p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (V0l = c_2Elist_2ENIL(A_27a))) & ((p(ap(ap(c_2Earithmetic_2E_3E_3D,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (V0l = c_2Elist_2ENIL(A_27a))) & (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Elist_2ELENGTH(A_27a),V0l)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> (V0l = c_2Elist_2ENIL(A_27a))))))))))).
tff(conj_thm_2EquantHeuristics_2ELIST__LENGTH__0,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => (((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l)) = fo__c_2Enum_2E0) <=> (V0l = c_2Elist_2ENIL(A_27a))) & (((fo__c_2Enum_2E0 = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (V0l = c_2Elist_2ENIL(A_27a))) & ((p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Elist_2ELENGTH(A_27a),V0l)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) <=> (V0l = c_2Elist_2ENIL(A_27a))) & ((p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (V0l = c_2Elist_2ENIL(A_27a))) & ((p(ap(ap(c_2Earithmetic_2E_3E_3D,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (V0l = c_2Elist_2ENIL(A_27a))) & (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Elist_2ELENGTH(A_27a),V0l)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> (V0l = c_2Elist_2ENIL(A_27a))))))))))))).
tff(conj_thm_2EquantHeuristics_2ELIST__LENGTH__1,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ! [V1x:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l)) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) <=> (? [V2e1:$i] : (mem(V2e1,A_27a) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V2e1),c_2Elist_2ENIL(A_27a)))))) & (((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (? [V3e1:$i] : (mem(V3e1,A_27a) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V3e1),c_2Elist_2ENIL(A_27a)))))) & ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (? [V4l_27:$i] : (mem(V4l_27,ty_2Elist_2Elist(A_27a)) & (? [V5e1:$i] : (mem(V5e1,A_27a) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V5e1),V4l_27))))))) & ((p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Elist_2ELENGTH(A_27a),V0l)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> (? [V6l_27:$i] : (mem(V6l_27,ty_2Elist_2Elist(A_27a)) & (? [V7e1:$i] : (mem(V7e1,A_27a) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V7e1),V6l_27))))))) & ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (? [V8l_27:$i] : (mem(V8l_27,ty_2Elist_2Elist(A_27a)) & (? [V9e1:$i] : (mem(V9e1,A_27a) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V9e1),V8l_27))))))) & ((p(ap(ap(c_2Earithmetic_2E_3E_3D,ap(c_2Elist_2ELENGTH(A_27a),V0l)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) <=> (? [V10l_27:$i] : (mem(V10l_27,ty_2Elist_2Elist(A_27a)) & (? [V11e1:$i] : (mem(V11e1,A_27a) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V11e1),V10l_27))))))) & ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V1x))),ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (? [V12l_27:$i] : (mem(V12l_27,ty_2Elist_2Elist(A_27a)) & (? [V13e1:$i] : (mem(V13e1,A_27a) & (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1x)),ap(c_2Elist_2ELENGTH(A_27a),V12l_27))) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V13e1),V12l_27)))))))) & ((p(ap(ap(c_2Earithmetic_2E_3E_3D,ap(c_2Elist_2ELENGTH(A_27a),V0l)),ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V1x)))) <=> (? [V14l_27:$i] : (mem(V14l_27,ty_2Elist_2Elist(A_27a)) & (? [V15e1:$i] : (mem(V15e1,A_27a) & (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1x)),ap(c_2Elist_2ELENGTH(A_27a),V14l_27))) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V15e1),V14l_27)))))))) & ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (? [V16l_27:$i] : (mem(V16l_27,ty_2Elist_2Elist(A_27a)) & (? [V17e1:$i] : (mem(V17e1,A_27a) & (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1x)),ap(c_2Elist_2ELENGTH(A_27a),V16l_27))) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V17e1),V16l_27)))))))) & ((p(ap(ap(c_2Earithmetic_2E_3E_3D,ap(c_2Elist_2ELENGTH(A_27a),V0l)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) <=> (? [V18l_27:$i] : (mem(V18l_27,ty_2Elist_2Elist(A_27a)) & (? [V19e1:$i] : (mem(V19e1,A_27a) & (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1x)),ap(c_2Elist_2ELENGTH(A_27a),V18l_27))) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V19e1),V18l_27)))))))) & (((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l)) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V1x)))) <=> (? [V20l_27:$i] : (mem(V20l_27,ty_2Elist_2Elist(A_27a)) & (? [V21e1:$i] : (mem(V21e1,A_27a) & ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V20l_27)) = V1x) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V21e1),V20l_27)))))))) & (((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V1x))) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (? [V22l_27:$i] : (mem(V22l_27,ty_2Elist_2Elist(A_27a)) & (? [V23e1:$i] : (mem(V23e1,A_27a) & ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V22l_27)) = V1x) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V23e1),V22l_27)))))))) & (((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l)) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) <=> (? [V24l_27:$i] : (mem(V24l_27,ty_2Elist_2Elist(A_27a)) & (? [V25e1:$i] : (mem(V25e1,A_27a) & ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V24l_27)) = V1x) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V25e1),V24l_27)))))))) & (((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (? [V26l_27:$i] : (mem(V26l_27,ty_2Elist_2Elist(A_27a)) & (? [V27e1:$i] : (mem(V27e1,A_27a) & ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V26l_27)) = V1x) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V27e1),V26l_27)))))))) & (((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l)) = fo__c_2Enum_2E0) <=> (V0l = c_2Elist_2ENIL(A_27a))) & (((fo__c_2Enum_2E0 = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (V0l = c_2Elist_2ENIL(A_27a))) & ((p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Elist_2ELENGTH(A_27a),V0l)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) <=> (V0l = c_2Elist_2ENIL(A_27a))) & ((p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (V0l = c_2Elist_2ENIL(A_27a))) & ((p(ap(ap(c_2Earithmetic_2E_3E_3D,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (V0l = c_2Elist_2ENIL(A_27a))) & (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Elist_2ELENGTH(A_27a),V0l)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> (V0l = c_2Elist_2ENIL(A_27a)))))))))))))))))))))))))))).
tff(conj_thm_2EquantHeuristics_2ELIST__LENGTH__2,conjecture,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ! [V1x:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l)) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) <=> (? [V2e1:$i] : (mem(V2e1,A_27a) & (? [V3e2:$i] : (mem(V3e2,A_27a) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V2e1),ap(ap(c_2Elist_2ECONS(A_27a),V3e2),c_2Elist_2ENIL(A_27a))))))))) & (((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (? [V4e1:$i] : (mem(V4e1,A_27a) & (? [V5e2:$i] : (mem(V5e2,A_27a) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V4e1),ap(ap(c_2Elist_2ECONS(A_27a),V5e2),c_2Elist_2ENIL(A_27a))))))))) & ((p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (? [V6l_27:$i] : (mem(V6l_27,ty_2Elist_2Elist(A_27a)) & (? [V7e1:$i] : (mem(V7e1,A_27a) & (? [V8e2:$i] : (mem(V8e2,A_27a) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V7e1),ap(ap(c_2Elist_2ECONS(A_27a),V8e2),V6l_27)))))))))) & ((p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Elist_2ELENGTH(A_27a),V0l)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) <=> (? [V9l_27:$i] : (mem(V9l_27,ty_2Elist_2Elist(A_27a)) & (? [V10e1:$i] : (mem(V10e1,A_27a) & (? [V11e2:$i] : (mem(V11e2,A_27a) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V10e1),ap(ap(c_2Elist_2ECONS(A_27a),V11e2),V9l_27)))))))))) & ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (? [V12l_27:$i] : (mem(V12l_27,ty_2Elist_2Elist(A_27a)) & (? [V13e1:$i] : (mem(V13e1,A_27a) & (? [V14e2:$i] : (mem(V14e2,A_27a) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V13e1),ap(ap(c_2Elist_2ECONS(A_27a),V14e2),V12l_27)))))))))) & ((p(ap(ap(c_2Earithmetic_2E_3E_3D,ap(c_2Elist_2ELENGTH(A_27a),V0l)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) <=> (? [V15l_27:$i] : (mem(V15l_27,ty_2Elist_2Elist(A_27a)) & (? [V16e1:$i] : (mem(V16e1,A_27a) & (? [V17e2:$i] : (mem(V17e2,A_27a) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V16e1),ap(ap(c_2Elist_2ECONS(A_27a),V17e2),V15l_27)))))))))) & ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V1x))),ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (? [V18l_27:$i] : (mem(V18l_27,ty_2Elist_2Elist(A_27a)) & (? [V19e1:$i] : (mem(V19e1,A_27a) & (? [V20e2:$i] : (mem(V20e2,A_27a) & (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1x)),ap(c_2Elist_2ELENGTH(A_27a),V18l_27))) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V19e1),ap(ap(c_2Elist_2ECONS(A_27a),V20e2),V18l_27))))))))))) & ((p(ap(ap(c_2Earithmetic_2E_3E_3D,ap(c_2Elist_2ELENGTH(A_27a),V0l)),ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V1x)))) <=> (? [V21l_27:$i] : (mem(V21l_27,ty_2Elist_2Elist(A_27a)) & (? [V22e1:$i] : (mem(V22e1,A_27a) & (? [V23e2:$i] : (mem(V23e2,A_27a) & (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1x)),ap(c_2Elist_2ELENGTH(A_27a),V21l_27))) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V22e1),ap(ap(c_2Elist_2ECONS(A_27a),V23e2),V21l_27))))))))))) & ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (? [V24l_27:$i] : (mem(V24l_27,ty_2Elist_2Elist(A_27a)) & (? [V25e1:$i] : (mem(V25e1,A_27a) & (? [V26e2:$i] : (mem(V26e2,A_27a) & (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1x)),ap(c_2Elist_2ELENGTH(A_27a),V24l_27))) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V25e1),ap(ap(c_2Elist_2ECONS(A_27a),V26e2),V24l_27))))))))))) & ((p(ap(ap(c_2Earithmetic_2E_3E_3D,ap(c_2Elist_2ELENGTH(A_27a),V0l)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) <=> (? [V27l_27:$i] : (mem(V27l_27,ty_2Elist_2Elist(A_27a)) & (? [V28e1:$i] : (mem(V28e1,A_27a) & (? [V29e2:$i] : (mem(V29e2,A_27a) & (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1x)),ap(c_2Elist_2ELENGTH(A_27a),V27l_27))) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V28e1),ap(ap(c_2Elist_2ECONS(A_27a),V29e2),V27l_27))))))))))) & (((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l)) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V1x)))) <=> (? [V30l_27:$i] : (mem(V30l_27,ty_2Elist_2Elist(A_27a)) & (? [V31e1:$i] : (mem(V31e1,A_27a) & (? [V32e2:$i] : (mem(V32e2,A_27a) & ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V30l_27)) = V1x) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V31e1),ap(ap(c_2Elist_2ECONS(A_27a),V32e2),V30l_27))))))))))) & (((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V1x))) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (? [V33l_27:$i] : (mem(V33l_27,ty_2Elist_2Elist(A_27a)) & (? [V34e1:$i] : (mem(V34e1,A_27a) & (? [V35e2:$i] : (mem(V35e2,A_27a) & ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V33l_27)) = V1x) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V34e1),ap(ap(c_2Elist_2ECONS(A_27a),V35e2),V33l_27))))))))))) & (((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l)) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) <=> (? [V36l_27:$i] : (mem(V36l_27,ty_2Elist_2Elist(A_27a)) & (? [V37e1:$i] : (mem(V37e1,A_27a) & (? [V38e2:$i] : (mem(V38e2,A_27a) & ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V36l_27)) = V1x) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V37e1),ap(ap(c_2Elist_2ECONS(A_27a),V38e2),V36l_27))))))))))) & (((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (? [V39l_27:$i] : (mem(V39l_27,ty_2Elist_2Elist(A_27a)) & (? [V40e1:$i] : (mem(V40e1,A_27a) & (? [V41e2:$i] : (mem(V41e2,A_27a) & ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V39l_27)) = V1x) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V40e1),ap(ap(c_2Elist_2ECONS(A_27a),V41e2),V39l_27))))))))))) & (((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l)) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) <=> (? [V42e1:$i] : (mem(V42e1,A_27a) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V42e1),c_2Elist_2ENIL(A_27a)))))) & (((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (? [V43e1:$i] : (mem(V43e1,A_27a) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V43e1),c_2Elist_2ENIL(A_27a)))))) & ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (? [V44l_27:$i] : (mem(V44l_27,ty_2Elist_2Elist(A_27a)) & (? [V45e1:$i] : (mem(V45e1,A_27a) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V45e1),V44l_27))))))) & ((p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Elist_2ELENGTH(A_27a),V0l)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> (? [V46l_27:$i] : (mem(V46l_27,ty_2Elist_2Elist(A_27a)) & (? [V47e1:$i] : (mem(V47e1,A_27a) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V47e1),V46l_27))))))) & ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (? [V48l_27:$i] : (mem(V48l_27,ty_2Elist_2Elist(A_27a)) & (? [V49e1:$i] : (mem(V49e1,A_27a) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V49e1),V48l_27))))))) & ((p(ap(ap(c_2Earithmetic_2E_3E_3D,ap(c_2Elist_2ELENGTH(A_27a),V0l)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) <=> (? [V50l_27:$i] : (mem(V50l_27,ty_2Elist_2Elist(A_27a)) & (? [V51e1:$i] : (mem(V51e1,A_27a) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V51e1),V50l_27))))))) & ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V1x))),ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (? [V52l_27:$i] : (mem(V52l_27,ty_2Elist_2Elist(A_27a)) & (? [V53e1:$i] : (mem(V53e1,A_27a) & (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1x)),ap(c_2Elist_2ELENGTH(A_27a),V52l_27))) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V53e1),V52l_27)))))))) & ((p(ap(ap(c_2Earithmetic_2E_3E_3D,ap(c_2Elist_2ELENGTH(A_27a),V0l)),ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V1x)))) <=> (? [V54l_27:$i] : (mem(V54l_27,ty_2Elist_2Elist(A_27a)) & (? [V55e1:$i] : (mem(V55e1,A_27a) & (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1x)),ap(c_2Elist_2ELENGTH(A_27a),V54l_27))) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V55e1),V54l_27)))))))) & ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (? [V56l_27:$i] : (mem(V56l_27,ty_2Elist_2Elist(A_27a)) & (? [V57e1:$i] : (mem(V57e1,A_27a) & (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1x)),ap(c_2Elist_2ELENGTH(A_27a),V56l_27))) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V57e1),V56l_27)))))))) & ((p(ap(ap(c_2Earithmetic_2E_3E_3D,ap(c_2Elist_2ELENGTH(A_27a),V0l)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) <=> (? [V58l_27:$i] : (mem(V58l_27,ty_2Elist_2Elist(A_27a)) & (? [V59e1:$i] : (mem(V59e1,A_27a) & (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1x)),ap(c_2Elist_2ELENGTH(A_27a),V58l_27))) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V59e1),V58l_27)))))))) & (((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l)) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V1x)))) <=> (? [V60l_27:$i] : (mem(V60l_27,ty_2Elist_2Elist(A_27a)) & (? [V61e1:$i] : (mem(V61e1,A_27a) & ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V60l_27)) = V1x) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V61e1),V60l_27)))))))) & (((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V1x))) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (? [V62l_27:$i] : (mem(V62l_27,ty_2Elist_2Elist(A_27a)) & (? [V63e1:$i] : (mem(V63e1,A_27a) & ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V62l_27)) = V1x) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V63e1),V62l_27)))))))) & (((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l)) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) <=> (? [V64l_27:$i] : (mem(V64l_27,ty_2Elist_2Elist(A_27a)) & (? [V65e1:$i] : (mem(V65e1,A_27a) & ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V64l_27)) = V1x) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V65e1),V64l_27)))))))) & (((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (? [V66l_27:$i] : (mem(V66l_27,ty_2Elist_2Elist(A_27a)) & (? [V67e1:$i] : (mem(V67e1,A_27a) & ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V66l_27)) = V1x) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V67e1),V66l_27)))))))) & (((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l)) = fo__c_2Enum_2E0) <=> (V0l = c_2Elist_2ENIL(A_27a))) & (((fo__c_2Enum_2E0 = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (V0l = c_2Elist_2ENIL(A_27a))) & ((p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Elist_2ELENGTH(A_27a),V0l)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) <=> (V0l = c_2Elist_2ENIL(A_27a))) & ((p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (V0l = c_2Elist_2ENIL(A_27a))) & ((p(ap(ap(c_2Earithmetic_2E_3E_3D,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (V0l = c_2Elist_2ENIL(A_27a))) & (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Elist_2ELENGTH(A_27a),V0l)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> (V0l = c_2Elist_2ENIL(A_27a)))))))))))))))))))))))))))))))))))))))))).
