include('Axioms/binary_ieee_2.ax').
tff(tp_c_2EHolSmt_2Earray__ext,type,(c_2EHolSmt_2Earray__ext:(del * del) > $i)).
tff(mem_c_2EHolSmt_2Earray__ext,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EHolSmt_2Earray__ext(A_27a,A_27b),arr(arr(A_27a,A_27b),arr(arr(A_27a,A_27b),A_27a)))))).
tff(tp_c_2EHolSmt_2Exor,type,(c_2EHolSmt_2Exor:$i)).
tff(mem_c_2EHolSmt_2Exor,axiom,mem(c_2EHolSmt_2Exor,arr(bool,arr(bool,bool)))).
tff(stp_fo_c_2EHolSmt_2Exor,type,(fo__c_2EHolSmt_2Exor:(tp__o * tp__o) > tp__o)).
tff(stp_eq_fo_c_2EHolSmt_2Exor,axiom,( ! [X0:tp__o] : ( ! [X1:tp__o] : (inj__o(fo__c_2EHolSmt_2Exor(X0,X1)) = ap(ap(c_2EHolSmt_2Exor,inj__o(X0)),inj__o(X1)))))).
tff(ax_thm_2EHolSmt_2Exor__def,axiom,( ! [V0x:tp__o] : ( ! [V1y:tp__o] : (p(ap(ap(c_2EHolSmt_2Exor,inj__o(V0x)),inj__o(V1y))) <=> (~~ (p(inj__o(V0x)) <=> p(inj__o(V1y)))))))).
tff(ax_thm_2EHolSmt_2Earray__ext__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0A:$i] : (mem(V0A,arr(A_27a,A_27b)) => ( ! [V1B:$i] : (mem(V1B,arr(A_27a,A_27b)) => (ap(ap(c_2EHolSmt_2Earray__ext(A_27a,A_27b),V0A),V1B) = ap(c_2Emin_2E_40(A_27a),f3148(A_27a,A_27b,V1B,V0A)))))))))).
tff(conj_thm_2EHolSmt_2EALL__DISTINCT__NIL,lemma,(( ! [A_27a:del]: (p(ap(c_2Elist_2EALL__DISTINCT(A_27a),c_2Elist_2ENIL(A_27a))) <=> $true)))).
tff(conj_thm_2EHolSmt_2EALL__DISTINCT__CONS,lemma,(( ! [A_27a:del]: ( ! [V0h:$i] : (mem(V0h,A_27a) => ( ! [V1t:$i] : (mem(V1t,ty_2Elist_2Elist(A_27a)) => (p(ap(c_2Elist_2EALL__DISTINCT(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0h),V1t))) <=> ((~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V0h),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1t)))) & p(ap(c_2Elist_2EALL__DISTINCT(A_27a),V1t))))))))))).
tff(conj_thm_2EHolSmt_2ENOT__MEM__NIL,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ((~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Elist_2ELIST__TO__SET(A_27a),c_2Elist_2ENIL(A_27a))))) <=> $true)))))).
tff(conj_thm_2EHolSmt_2ENOT__MEM__CONS,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1h:$i] : (mem(V1h,A_27a) => ( ! [V2t:$i] : (mem(V2t,ty_2Elist_2Elist(A_27a)) => ((~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Elist_2ELIST__TO__SET(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V1h),V2t))))) <=> ((~~ (V0x = V1h)) & (~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Elist_2ELIST__TO__SET(A_27a),V2t))))))))))))))).
tff(conj_thm_2EHolSmt_2EAND__T,lemma,(( ! [V0p:tp__o] : ((p(inj__o(V0p)) & $true) <=> p(inj__o(V0p)))))).
tff(conj_thm_2EHolSmt_2ET__AND,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((($true & p(inj__o(V0p))) <=> ($true & p(inj__o(V1q)))) => (p(inj__o(V0p)) <=> p(inj__o(V1q)))))))).
tff(conj_thm_2EHolSmt_2EF__OR,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((($false | p(inj__o(V0p))) <=> ($false | p(inj__o(V1q)))) => (p(inj__o(V0p)) <=> p(inj__o(V1q)))))))).
tff(conj_thm_2EHolSmt_2ECONJ__CONG,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ( ! [V2r:tp__o] : ( ! [V3s:tp__o] : ((p(inj__o(V0p)) <=> p(inj__o(V1q))) => ((p(inj__o(V2r)) <=> p(inj__o(V3s))) => ((p(inj__o(V0p)) & p(inj__o(V2r))) <=> (p(inj__o(V1q)) & p(inj__o(V3s)))))))))))).
tff(conj_thm_2EHolSmt_2ENOT__NOT__ELIM,lemma,(( ! [V0p:tp__o] : ((~~ (~~ p(inj__o(V0p)))) => p(inj__o(V0p)))))).
tff(conj_thm_2EHolSmt_2ENOT__FALSE,lemma,(( ! [V0p:tp__o] : (p(inj__o(V0p)) => ((~~ p(inj__o(V0p))) => $false))))).
tff(conj_thm_2EHolSmt_2ENNF__CONJ,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ( ! [V2r:tp__o] : ( ! [V3s:tp__o] : (((~~ p(inj__o(V0p))) <=> p(inj__o(V2r))) => (((~~ p(inj__o(V1q))) <=> p(inj__o(V3s))) => ((~~ (p(inj__o(V0p)) & p(inj__o(V1q)))) <=> (p(inj__o(V2r)) | p(inj__o(V3s)))))))))))).
tff(conj_thm_2EHolSmt_2ENNF__DISJ,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ( ! [V2r:tp__o] : ( ! [V3s:tp__o] : (((~~ p(inj__o(V0p))) <=> p(inj__o(V2r))) => (((~~ p(inj__o(V1q))) <=> p(inj__o(V3s))) => ((~~ (p(inj__o(V0p)) | p(inj__o(V1q)))) <=> (p(inj__o(V2r)) & p(inj__o(V3s)))))))))))).
tff(conj_thm_2EHolSmt_2ENNF__NOT__NOT,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((p(inj__o(V0p)) <=> p(inj__o(V1q))) => ((~~ (~~ p(inj__o(V0p)))) <=> p(inj__o(V1q)))))))).
tff(conj_thm_2EHolSmt_2ENEG__IFF__1__1,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((p(inj__o(V1q)) <=> p(inj__o(V0p))) => (~~ (p(inj__o(V0p)) <=> (~~ p(inj__o(V1q)))))))))).
tff(conj_thm_2EHolSmt_2ENEG__IFF__1__2,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((~~ (p(inj__o(V0p)) <=> (~~ p(inj__o(V1q))))) => (p(inj__o(V1q)) <=> p(inj__o(V0p)))))))).
tff(conj_thm_2EHolSmt_2ENEG__IFF__2__1,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((p(inj__o(V0p)) <=> (~~ p(inj__o(V1q)))) => (~~ (p(inj__o(V0p)) <=> p(inj__o(V1q))))))))).
tff(conj_thm_2EHolSmt_2ENEG__IFF__2__2,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((~~ (p(inj__o(V0p)) <=> p(inj__o(V1q)))) => (p(inj__o(V0p)) <=> (~~ p(inj__o(V1q))))))))).
tff(conj_thm_2EHolSmt_2EDISJ__ELIM__1,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ( ! [V2r:tp__o] : (((p(inj__o(V0p)) | p(inj__o(V1q))) => p(inj__o(V2r))) => (p(inj__o(V0p)) => p(inj__o(V2r))))))))).
tff(conj_thm_2EHolSmt_2EDISJ__ELIM__2,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ( ! [V2r:tp__o] : (((p(inj__o(V0p)) | p(inj__o(V1q))) => p(inj__o(V2r))) => (p(inj__o(V1q)) => p(inj__o(V2r))))))))).
tff(conj_thm_2EHolSmt_2EIMP__DISJ__1,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((p(inj__o(V0p)) => p(inj__o(V1q))) => ((~~ p(inj__o(V0p))) | p(inj__o(V1q)))))))).
tff(conj_thm_2EHolSmt_2EIMP__DISJ__2,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : (((~~ p(inj__o(V0p))) => p(inj__o(V1q))) => (p(inj__o(V0p)) | p(inj__o(V1q)))))))).
tff(conj_thm_2EHolSmt_2EIMP__FALSE,lemma,(( ! [V0p:tp__o] : (((~~ p(inj__o(V0p))) => $false) => p(inj__o(V0p)))))).
tff(conj_thm_2EHolSmt_2EAND__IMP__INTRO__SYM,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ( ! [V2r:tp__o] : (((p(inj__o(V0p)) & p(inj__o(V1q))) => p(inj__o(V2r))) <=> (p(inj__o(V0p)) => (p(inj__o(V1q)) => p(inj__o(V2r)))))))))).
tff(conj_thm_2EHolSmt_2EVALID__IFF__TRUE,lemma,(( ! [V0p:tp__o] : (p(inj__o(V0p)) => (p(inj__o(V0p)) <=> $true))))).
tff(conj_thm_2EHolSmt_2Ed001,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((~~ (p(inj__o(V0p)) <=> p(inj__o(V1q)))) | ((~~ p(inj__o(V0p))) | p(inj__o(V1q)))))))).
tff(conj_thm_2EHolSmt_2Ed002,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((~~ (p(inj__o(V0p)) <=> p(inj__o(V1q)))) | (p(inj__o(V0p)) | (~~ p(inj__o(V1q))))))))).
tff(conj_thm_2EHolSmt_2Ed003,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((p(inj__o(V0p)) <=> (~~ p(inj__o(V1q)))) | ((~~ p(inj__o(V0p))) | p(inj__o(V1q)))))))).
tff(conj_thm_2EHolSmt_2Ed004,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : (((~~ p(inj__o(V0p))) <=> p(inj__o(V1q))) | (p(inj__o(V0p)) | (~~ p(inj__o(V1q))))))))).
tff(conj_thm_2EHolSmt_2Ed005,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((p(inj__o(V0p)) <=> p(inj__o(V1q))) | ((~~ p(inj__o(V0p))) | (~~ p(inj__o(V1q))))))))).
tff(conj_thm_2EHolSmt_2Ed006,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((p(inj__o(V0p)) <=> p(inj__o(V1q))) | (p(inj__o(V0p)) | p(inj__o(V1q)))))))).
tff(conj_thm_2EHolSmt_2Ed007,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((~~ ((~~ p(inj__o(V0p))) <=> p(inj__o(V1q)))) | (p(inj__o(V0p)) | p(inj__o(V1q)))))))).
tff(conj_thm_2EHolSmt_2Ed008,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((~~ (p(inj__o(V0p)) <=> (~~ p(inj__o(V1q))))) | (p(inj__o(V0p)) | p(inj__o(V1q)))))))).
tff(conj_thm_2EHolSmt_2Ed009,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((~~ p(inj__o(V0p))) | (p(inj__o(V1q)) | (~~ (p(inj__o(V0p)) <=> p(inj__o(V1q)))))))))).
tff(conj_thm_2EHolSmt_2Ed010,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : (p(inj__o(V0p)) | ((~~ p(inj__o(V1q))) | (~~ (p(inj__o(V0p)) <=> p(inj__o(V1q)))))))))).
tff(conj_thm_2EHolSmt_2Ed011,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : (p(inj__o(V0p)) | (p(inj__o(V1q)) | (~~ ((~~ p(inj__o(V0p))) <=> p(inj__o(V1q)))))))))).
tff(conj_thm_2EHolSmt_2Ed012,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : (p(inj__o(V0p)) | (p(inj__o(V1q)) | (~~ (p(inj__o(V0p)) <=> (~~ p(inj__o(V1q))))))))))).
tff(conj_thm_2EHolSmt_2Ed013,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : (((~~ p(inj__o(V0p))) & (~~ p(inj__o(V1q)))) | (p(inj__o(V0p)) | p(inj__o(V1q)))))))).
tff(conj_thm_2EHolSmt_2Ed014,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : (((~~ p(inj__o(V0p))) & p(inj__o(V1q))) | (p(inj__o(V0p)) | (~~ p(inj__o(V1q))))))))).
tff(conj_thm_2EHolSmt_2Ed015,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((p(inj__o(V0p)) & (~~ p(inj__o(V1q)))) | ((~~ p(inj__o(V0p))) | p(inj__o(V1q)))))))).
tff(conj_thm_2EHolSmt_2Ed016,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((p(inj__o(V0p)) & p(inj__o(V1q))) | ((~~ p(inj__o(V0p))) | (~~ p(inj__o(V1q))))))))).
tff(conj_thm_2EHolSmt_2Ed017,lemma,(( ! [A_27a:del]: ( ! [V0p:tp__o] : ( ! [V1y:$i] : (mem(V1y,A_27a) => ( ! [V2x:$i] : (mem(V2x,A_27a) => (p(inj__o(V0p)) | (V1y = ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(V0p)),V2x),V1y))))))))))).
tff(conj_thm_2EHolSmt_2Ed018,lemma,(( ! [A_27a:del]: ( ! [V0p:tp__o] : ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ((~~ p(inj__o(V0p))) | (V1x = ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(V0p)),V1x),V2y))))))))))).
tff(conj_thm_2EHolSmt_2Ed019,lemma,(( ! [A_27a:del]: ( ! [V0p:tp__o] : ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => (p(inj__o(V0p)) | (ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(V0p)),V1x),V2y) = V2y)))))))))).
tff(conj_thm_2EHolSmt_2Ed020,lemma,(( ! [A_27a:del]: ( ! [V0p:tp__o] : ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ((~~ p(inj__o(V0p))) | (ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(V0p)),V1x),V2y) = V1x)))))))))).
tff(conj_thm_2EHolSmt_2Ed021,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ( ! [V2r:tp__o] : (p(inj__o(V0p)) | (p(inj__o(V1q)) | (~~ p(ap(ap(ap(c_2Ebool_2ECOND(bool),inj__o(V0p)),inj__o(V2r)),inj__o(V1q))))))))))).
tff(conj_thm_2EHolSmt_2Ed022,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ( ! [V2r:tp__o] : ((~~ p(inj__o(V0p))) | (p(inj__o(V1q)) | (~~ p(ap(ap(ap(c_2Ebool_2ECOND(bool),inj__o(V0p)),inj__o(V1q)),inj__o(V2r))))))))))).
tff(conj_thm_2EHolSmt_2Ed023,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ( ! [V2r:tp__o] : (p(ap(ap(ap(c_2Ebool_2ECOND(bool),inj__o(V0p)),inj__o(V1q)),inj__o(V2r))) | ((~~ p(inj__o(V0p))) | (~~ p(inj__o(V1q)))))))))).
tff(conj_thm_2EHolSmt_2Ed024,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ( ! [V2r:tp__o] : (p(ap(ap(ap(c_2Ebool_2ECOND(bool),inj__o(V0p)),inj__o(V1q)),inj__o(V2r))) | (p(inj__o(V0p)) | (~~ p(inj__o(V2r)))))))))).
tff(conj_thm_2EHolSmt_2Ed025,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ( ! [V2r:tp__o] : (p(ap(ap(ap(c_2Ebool_2ECOND(bool),inj__o(V0p)),ap(c_2Ebool_2E_7E,inj__o(V1q))),inj__o(V2r))) | ((~~ p(inj__o(V0p))) | p(inj__o(V1q))))))))).
tff(conj_thm_2EHolSmt_2Ed026,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ( ! [V2r:tp__o] : (p(ap(ap(ap(c_2Ebool_2ECOND(bool),inj__o(V0p)),inj__o(V1q)),ap(c_2Ebool_2E_7E,inj__o(V2r)))) | (p(inj__o(V0p)) | p(inj__o(V2r))))))))).
tff(conj_thm_2EHolSmt_2Ed027,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ( ! [V2r:tp__o] : ((~~ p(ap(ap(ap(c_2Ebool_2ECOND(bool),inj__o(V0p)),inj__o(V1q)),inj__o(V2r)))) | ((~~ p(inj__o(V0p))) | p(inj__o(V1q))))))))).
tff(conj_thm_2EHolSmt_2Ed028,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ( ! [V2r:tp__o] : ((~~ p(ap(ap(ap(c_2Ebool_2ECOND(bool),inj__o(V0p)),inj__o(V1q)),inj__o(V2r)))) | (p(inj__o(V0p)) | p(inj__o(V2r))))))))).
tff(conj_thm_2EHolSmt_2Er001,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1y:$i] : (mem(V1y,A_27a) => ((V0x = V1y) <=> (V1y = V0x))))))))).
tff(conj_thm_2EHolSmt_2Er002,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ((V0x = V0x) <=> $true)))))).
tff(conj_thm_2EHolSmt_2Er003,lemma,(( ! [V0p:tp__o] : ((p(inj__o(V0p)) <=> $true) <=> p(inj__o(V0p)))))).
tff(conj_thm_2EHolSmt_2Er004,lemma,(( ! [V0p:tp__o] : (($true <=> p(inj__o(V0p))) <=> p(inj__o(V0p)))))).
tff(conj_thm_2EHolSmt_2Er005,lemma,(( ! [V0p:tp__o] : ((p(inj__o(V0p)) <=> $false) <=> (~~ p(inj__o(V0p))))))).
tff(conj_thm_2EHolSmt_2Er006,lemma,(( ! [V0p:tp__o] : (($false <=> p(inj__o(V0p))) <=> (~~ p(inj__o(V0p))))))).
tff(conj_thm_2EHolSmt_2Er007,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : (((~~ p(inj__o(V0p))) <=> (~~ p(inj__o(V1q)))) <=> (p(inj__o(V0p)) <=> p(inj__o(V1q)))))))).
tff(conj_thm_2EHolSmt_2Er008,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((~~ (p(inj__o(V0p)) <=> (~~ p(inj__o(V1q))))) <=> (p(inj__o(V0p)) <=> p(inj__o(V1q)))))))).
tff(conj_thm_2EHolSmt_2Er009,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((~~ ((~~ p(inj__o(V0p))) <=> p(inj__o(V1q)))) <=> (p(inj__o(V0p)) <=> p(inj__o(V1q)))))))).
tff(conj_thm_2EHolSmt_2Er010,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1y:$i] : (mem(V1y,A_27a) => (ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(fo__c_2Ebool_2ET)),V0x),V1y) = V0x)))))))).
tff(conj_thm_2EHolSmt_2Er011,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1y:$i] : (mem(V1y,A_27a) => (ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(fo__c_2Ebool_2EF)),V0x),V1y) = V1y)))))))).
tff(conj_thm_2EHolSmt_2Er012,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : (p(ap(ap(ap(c_2Ebool_2ECOND(bool),inj__o(V0p)),inj__o(V1q)),inj__o(fo__c_2Ebool_2ET))) <=> ((~~ p(inj__o(V0p))) | p(inj__o(V1q)))))))).
tff(conj_thm_2EHolSmt_2Er013,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : (p(ap(ap(ap(c_2Ebool_2ECOND(bool),inj__o(V0p)),inj__o(V1q)),inj__o(fo__c_2Ebool_2ET))) <=> (p(inj__o(V1q)) | (~~ p(inj__o(V0p))))))))).
tff(conj_thm_2EHolSmt_2Er014,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : (p(ap(ap(ap(c_2Ebool_2ECOND(bool),inj__o(V0p)),inj__o(V1q)),ap(c_2Ebool_2E_7E,inj__o(V1q)))) <=> (p(inj__o(V0p)) <=> p(inj__o(V1q)))))))).
tff(conj_thm_2EHolSmt_2Er015,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : (p(ap(ap(ap(c_2Ebool_2ECOND(bool),inj__o(V0p)),inj__o(V1q)),ap(c_2Ebool_2E_7E,inj__o(V1q)))) <=> (p(inj__o(V1q)) <=> p(inj__o(V0p)))))))).
tff(conj_thm_2EHolSmt_2Er016,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : (p(ap(ap(ap(c_2Ebool_2ECOND(bool),inj__o(V0p)),ap(c_2Ebool_2E_7E,inj__o(V1q))),inj__o(V1q))) <=> (p(inj__o(V0p)) <=> (~~ p(inj__o(V1q))))))))).
tff(conj_thm_2EHolSmt_2Er017,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : (p(ap(ap(ap(c_2Ebool_2ECOND(bool),inj__o(V0p)),ap(c_2Ebool_2E_7E,inj__o(V1q))),inj__o(V1q))) <=> ((~~ p(inj__o(V1q))) <=> p(inj__o(V0p)))))))).
tff(conj_thm_2EHolSmt_2Er018,lemma,(( ! [A_27a:del]: ( ! [V0p:tp__o] : ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => (ap(ap(ap(c_2Ebool_2ECOND(A_27a),ap(c_2Ebool_2E_7E,inj__o(V0p))),V1x),V2y) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(V0p)),V2y),V1x)))))))))).
tff(conj_thm_2EHolSmt_2Er019,lemma,(( ! [A_27a:del]: ( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27a) => (ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(V0p)),ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(V1q)),V2x),V3y)),V2x) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),ap(ap(c_2Ebool_2E_2F_5C,inj__o(V0p)),ap(c_2Ebool_2E_7E,inj__o(V1q)))),V3y),V2x))))))))))).
tff(conj_thm_2EHolSmt_2Er020,lemma,(( ! [A_27a:del]: ( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27a) => (ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(V0p)),ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(V1q)),V2x),V3y)),V2x) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),ap(ap(c_2Ebool_2E_2F_5C,ap(c_2Ebool_2E_7E,inj__o(V1q))),inj__o(V0p))),V3y),V2x))))))))))).
tff(conj_thm_2EHolSmt_2Er021,lemma,(( ! [A_27a:del]: ( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27a) => (ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(V0p)),ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(V1q)),V2x),V3y)),V3y) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),ap(ap(c_2Ebool_2E_2F_5C,inj__o(V0p)),inj__o(V1q))),V2x),V3y))))))))))).
tff(conj_thm_2EHolSmt_2Er022,lemma,(( ! [A_27a:del]: ( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27a) => (ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(V0p)),ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(V1q)),V2x),V3y)),V3y) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),ap(ap(c_2Ebool_2E_2F_5C,inj__o(V1q)),inj__o(V0p))),V2x),V3y))))))))))).
tff(conj_thm_2EHolSmt_2Er023,lemma,(( ! [A_27a:del]: ( ! [V0p:tp__o] : ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ( ! [V3z:$i] : (mem(V3z,A_27a) => (ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(V0p)),V1x),ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(V0p)),V2y),V3z)) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(V0p)),V1x),V3z)))))))))))).
tff(conj_thm_2EHolSmt_2Er024,lemma,(( ! [A_27a:del]: ( ! [V0p:tp__o] : ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2q:tp__o] : ( ! [V3y:$i] : (mem(V3y,A_27a) => (ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(V0p)),V1x),ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(V2q)),V1x),V3y)) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),ap(ap(c_2Ebool_2E_5C_2F,inj__o(V0p)),inj__o(V2q))),V1x),V3y))))))))))).
tff(conj_thm_2EHolSmt_2Er025,lemma,(( ! [A_27a:del]: ( ! [V0p:tp__o] : ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2q:tp__o] : ( ! [V3y:$i] : (mem(V3y,A_27a) => (ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(V0p)),V1x),ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(V2q)),V1x),V3y)) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),ap(ap(c_2Ebool_2E_5C_2F,inj__o(V2q)),inj__o(V0p))),V1x),V3y))))))))))).
tff(conj_thm_2EHolSmt_2Er026,lemma,(( ! [A_27a:del]: ( ! [V0p:tp__o] : ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ( ! [V3z:$i] : (mem(V3z,A_27a) => (p(ap(ap(ap(c_2Ebool_2ECOND(bool),inj__o(V0p)),ap(ap(c_2Emin_2E_3D(A_27a),V1x),V2y)),ap(ap(c_2Emin_2E_3D(A_27a),V1x),V3z))) <=> (V1x = ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(V0p)),V2y),V3z))))))))))))).
tff(conj_thm_2EHolSmt_2Er027,lemma,(( ! [A_27a:del]: ( ! [V0p:tp__o] : ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ( ! [V3z:$i] : (mem(V3z,A_27a) => (p(ap(ap(ap(c_2Ebool_2ECOND(bool),inj__o(V0p)),ap(ap(c_2Emin_2E_3D(A_27a),V1x),V2y)),ap(ap(c_2Emin_2E_3D(A_27a),V2y),V3z))) <=> (V2y = ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(V0p)),V1x),V3z))))))))))))).
tff(conj_thm_2EHolSmt_2Er028,lemma,(( ! [A_27a:del]: ( ! [V0p:tp__o] : ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ( ! [V3z:$i] : (mem(V3z,A_27a) => (p(ap(ap(ap(c_2Ebool_2ECOND(bool),inj__o(V0p)),ap(ap(c_2Emin_2E_3D(A_27a),V1x),V2y)),ap(ap(c_2Emin_2E_3D(A_27a),V3z),V2y))) <=> (V2y = ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(V0p)),V1x),V3z))))))))))))).
tff(conj_thm_2EHolSmt_2Er029,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : (((~~ p(inj__o(V0p))) => p(inj__o(V1q))) <=> (p(inj__o(V0p)) | p(inj__o(V1q)))))))).
tff(conj_thm_2EHolSmt_2Er030,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : (((~~ p(inj__o(V0p))) => p(inj__o(V1q))) <=> (p(inj__o(V1q)) | p(inj__o(V0p)))))))).
tff(conj_thm_2EHolSmt_2Er031,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((p(inj__o(V0p)) => p(inj__o(V1q))) <=> ((~~ p(inj__o(V0p))) | p(inj__o(V1q)))))))).
tff(conj_thm_2EHolSmt_2Er032,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((p(inj__o(V0p)) => p(inj__o(V1q))) <=> (p(inj__o(V1q)) | (~~ p(inj__o(V0p))))))))).
tff(conj_thm_2EHolSmt_2Er033,lemma,(( ! [V0p:tp__o] : (($true => p(inj__o(V0p))) <=> p(inj__o(V0p)))))).
tff(conj_thm_2EHolSmt_2Er034,lemma,(( ! [V0p:tp__o] : ((p(inj__o(V0p)) => $true) <=> $true)))).
tff(conj_thm_2EHolSmt_2Er035,lemma,(( ! [V0p:tp__o] : (($false => p(inj__o(V0p))) <=> $true)))).
tff(conj_thm_2EHolSmt_2Er036,lemma,(( ! [V0p:tp__o] : ((p(inj__o(V0p)) => p(inj__o(V0p))) <=> $true)))).
tff(conj_thm_2EHolSmt_2Er037,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ( ! [V2r:tp__o] : (((p(inj__o(V0p)) <=> p(inj__o(V1q))) => p(inj__o(V2r))) <=> (p(inj__o(V2r)) | (p(inj__o(V1q)) <=> (~~ p(inj__o(V0p))))))))))).
tff(conj_thm_2EHolSmt_2Er038,lemma,(((~~ ($true)) <=> $false))).
tff(conj_thm_2EHolSmt_2Er039,lemma,(((~~ ($false)) <=> $true))).
tff(conj_thm_2EHolSmt_2Er040,lemma,(( ! [V0p:tp__o] : ((~~ (~~ p(inj__o(V0p)))) <=> p(inj__o(V0p)))))).
tff(conj_thm_2EHolSmt_2Er041,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((p(inj__o(V0p)) | p(inj__o(V1q))) <=> (p(inj__o(V1q)) | p(inj__o(V0p)))))))).
tff(conj_thm_2EHolSmt_2Er042,lemma,(( ! [V0p:tp__o] : ((p(inj__o(V0p)) | $true) <=> $true)))).
tff(conj_thm_2EHolSmt_2Er043,lemma,(( ! [V0p:tp__o] : ((p(inj__o(V0p)) | (~~ p(inj__o(V0p)))) <=> $true)))).
tff(conj_thm_2EHolSmt_2Er044,lemma,(( ! [V0p:tp__o] : (((~~ p(inj__o(V0p))) | p(inj__o(V0p))) <=> $true)))).
tff(conj_thm_2EHolSmt_2Er045,lemma,(( ! [V0p:tp__o] : (($true | p(inj__o(V0p))) <=> $true)))).
tff(conj_thm_2EHolSmt_2Er046,lemma,(( ! [V0p:tp__o] : ((p(inj__o(V0p)) | $false) <=> p(inj__o(V0p)))))).
tff(conj_thm_2EHolSmt_2Er047,lemma,(( ! [V0p:tp__o] : (($false | p(inj__o(V0p))) <=> p(inj__o(V0p)))))).
tff(conj_thm_2EHolSmt_2Er048,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((p(inj__o(V0p)) & p(inj__o(V1q))) <=> (p(inj__o(V1q)) & p(inj__o(V0p)))))))).
tff(conj_thm_2EHolSmt_2Er049,lemma,(( ! [V0p:tp__o] : ((p(inj__o(V0p)) & $true) <=> p(inj__o(V0p)))))).
tff(conj_thm_2EHolSmt_2Er050,lemma,(( ! [V0p:tp__o] : (($true & p(inj__o(V0p))) <=> p(inj__o(V0p)))))).
tff(conj_thm_2EHolSmt_2Er051,lemma,(( ! [V0p:tp__o] : ((p(inj__o(V0p)) & $false) <=> $false)))).
tff(conj_thm_2EHolSmt_2Er052,lemma,(( ! [V0p:tp__o] : (($false & p(inj__o(V0p))) <=> $false)))).
tff(conj_thm_2EHolSmt_2Er053,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((p(inj__o(V0p)) & p(inj__o(V1q))) <=> (~~ ((~~ p(inj__o(V0p))) | (~~ p(inj__o(V1q)))))))))).
tff(conj_thm_2EHolSmt_2Er054,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : (((~~ p(inj__o(V0p))) & p(inj__o(V1q))) <=> (~~ (p(inj__o(V0p)) | (~~ p(inj__o(V1q)))))))))).
tff(conj_thm_2EHolSmt_2Er055,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((p(inj__o(V0p)) & (~~ p(inj__o(V1q)))) <=> (~~ ((~~ p(inj__o(V0p))) | p(inj__o(V1q))))))))).
tff(conj_thm_2EHolSmt_2Er056,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : (((~~ p(inj__o(V0p))) & (~~ p(inj__o(V1q)))) <=> (~~ (p(inj__o(V0p)) | p(inj__o(V1q))))))))).
tff(conj_thm_2EHolSmt_2Er057,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((p(inj__o(V0p)) & p(inj__o(V1q))) <=> (~~ ((~~ p(inj__o(V1q))) | (~~ p(inj__o(V0p)))))))))).
tff(conj_thm_2EHolSmt_2Er058,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : (((~~ p(inj__o(V0p))) & p(inj__o(V1q))) <=> (~~ ((~~ p(inj__o(V1q))) | p(inj__o(V0p))))))))).
tff(conj_thm_2EHolSmt_2Er059,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((p(inj__o(V0p)) & (~~ p(inj__o(V1q)))) <=> (~~ (p(inj__o(V1q)) | (~~ p(inj__o(V0p)))))))))).
tff(conj_thm_2EHolSmt_2Er060,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : (((~~ p(inj__o(V0p))) & (~~ p(inj__o(V1q)))) <=> (~~ (p(inj__o(V1q)) | p(inj__o(V0p))))))))).
tff(conj_thm_2EHolSmt_2Er061,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,A_27b)) => (ap(ap(ap(c_2Ecombin_2EUPDATE(A_27a,A_27b),V0x),ap(V1f,V0x)),V1f) = V1f))))))))).
tff(conj_thm_2EHolSmt_2Er062,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => (p(ap(c_2Elist_2EALL__DISTINCT(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0x),ap(ap(c_2Elist_2ECONS(A_27a),V0x),c_2Elist_2ENIL(A_27a))))) <=> $false)))))).
tff(conj_thm_2EHolSmt_2Er063,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1y:$i] : (mem(V1y,A_27a) => (p(ap(c_2Elist_2EALL__DISTINCT(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0x),ap(ap(c_2Elist_2ECONS(A_27a),V1y),c_2Elist_2ENIL(A_27a))))) <=> (~~ (V0x = V1y)))))))))).
tff(conj_thm_2EHolSmt_2Er064,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1y:$i] : (mem(V1y,A_27a) => (p(ap(c_2Elist_2EALL__DISTINCT(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0x),ap(ap(c_2Elist_2ECONS(A_27a),V1y),c_2Elist_2ENIL(A_27a))))) <=> (~~ (V1y = V0x)))))))))).
tff(conj_thm_2EHolSmt_2Er065,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((V0x = V1y) <=> (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V1y)))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))).
tff(conj_thm_2EHolSmt_2Er066,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : ((V0x = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))) <=> (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V2z)))) = V1y))))))).
tff(conj_thm_2EHolSmt_2Er067,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : ((V0x = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V2z))))) <=> (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V1y))),inj__ty_2Einteger_2Eint(V2z)))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2EHolSmt_2Er068,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : ((V0x = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V1y))),inj__ty_2Einteger_2Eint(V2z)))) <=> (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V2z))),inj__ty_2Einteger_2Eint(V0x)))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2EHolSmt_2Er069,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : ((V0x = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))) <=> (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V1y))),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V2z))))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2EHolSmt_2Er070,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : ((V0x = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))) <=> (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V2z)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V0x))))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2EHolSmt_2Er071,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : ((V0x = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))) <=> (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V0x))),inj__ty_2Einteger_2Eint(V2z)))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2EHolSmt_2Er072,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : ((V0x = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))) <=> (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V2z)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V0x)))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V1y)))))))))).
tff(conj_thm_2EHolSmt_2Er073,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : ((V0x = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V1y))),inj__ty_2Einteger_2Eint(V2z)))) <=> (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V2z)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V0x)))) = V1y))))))).
tff(conj_thm_2EHolSmt_2Er074,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V0x))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V1y)))) <=> (V0x = V1y)))))).
tff(conj_thm_2EHolSmt_2Er075,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V0x))),inj__ty_2Einteger_2Eint(V1y))) = V2z) <=> (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V1y)))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V2z)))))))))).
tff(conj_thm_2EHolSmt_2Er076,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> (V1y = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x))))))))).
tff(conj_thm_2EHolSmt_2Er077,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) = V2z) <=> (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V2z)))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x)))))))))).
tff(conj_thm_2EHolSmt_2Er078,lemma,(( ! [V0a:tp__ty_2Einteger_2Eint] : ( ! [V1x:tp__ty_2Einteger_2Eint] : ( ! [V2v:tp__ty_2Einteger_2Eint] : ( ! [V3y:tp__ty_2Einteger_2Eint] : ( ! [V4w:tp__ty_2Einteger_2Eint] : ( ! [V5z:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0a)),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V1x))),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V2v)),inj__ty_2Einteger_2Eint(V3y))),ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V4w)),inj__ty_2Einteger_2Eint(V5z)))))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1x)),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V2v))),inj__ty_2Einteger_2Eint(V3y))),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V4w))),inj__ty_2Einteger_2Eint(V5z))))) = V0a)))))))))).
tff(conj_thm_2EHolSmt_2Er079,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V0x))) = V0x)))).
tff(conj_thm_2EHolSmt_2Er080,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = V0x)))).
tff(conj_thm_2EHolSmt_2Er081,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x)))))))).
tff(conj_thm_2EHolSmt_2Er082,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V0x))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),inj__ty_2Einteger_2Eint(V0x))))))).
tff(conj_thm_2EHolSmt_2Er083,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))),inj__ty_2Einteger_2Eint(V2z))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))))))))).
tff(conj_thm_2EHolSmt_2Er084,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))),inj__ty_2Einteger_2Eint(V2z))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V2z)),inj__ty_2Einteger_2Eint(V1y)))))))))).
tff(conj_thm_2EHolSmt_2Er085,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V2z)),inj__ty_2Einteger_2Eint(V0x)))))))))).
tff(conj_thm_2EHolSmt_2Er086,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V2z)))))))))).
tff(conj_thm_2EHolSmt_2Er087,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : ( ! [V3u:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V2z)),inj__ty_2Einteger_2Eint(V3u))))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V2z)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V3u)),inj__ty_2Einteger_2Eint(V0x)))))))))))).
tff(conj_thm_2EHolSmt_2Er088,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__ge,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V0x))) <=> $true)))).
tff(conj_thm_2EHolSmt_2Er089,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__ge,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) <=> p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V1y)))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))).
tff(conj_thm_2EHolSmt_2Er090,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__ge,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V0x)))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))).
tff(conj_thm_2EHolSmt_2Er091,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__ge,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V2z)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V0x))))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2EHolSmt_2Er092,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V0x))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))).
tff(conj_thm_2EHolSmt_2Er093,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V0x))),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V1y)))) <=> p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y)))))))).
tff(conj_thm_2EHolSmt_2Er094,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V0x))),inj__ty_2Einteger_2Eint(V1y))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V1y)))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))).
tff(conj_thm_2EHolSmt_2Er095,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V1y)))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x)))))))).
tff(conj_thm_2EHolSmt_2Er096,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__gt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) <=> (~~ p(ap(ap(c_2Einteger_2Eint__ge,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x))))))))).
tff(conj_thm_2EHolSmt_2Er097,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__gt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) <=> (~~ p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))))))))).
tff(conj_thm_2EHolSmt_2Er098,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__gt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) <=> (~~ p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V1y)))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2EHolSmt_2Er099,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__gt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) <=> (~~ p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V0x)))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2EHolSmt_2Er100,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__gt,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))) <=> (~~ p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V2z)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V0x)))),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V1y))))))))))).
tff(conj_thm_2EHolSmt_2Er101,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V0x))) <=> $true)))).
tff(conj_thm_2EHolSmt_2Er102,lemma,((p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) <=> $true))).
tff(conj_thm_2EHolSmt_2Er103,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) <=> p(ap(ap(c_2Einteger_2Eint__ge,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x)))))))).
tff(conj_thm_2EHolSmt_2Er104,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x))),inj__ty_2Einteger_2Eint(V1y)))) <=> p(ap(ap(c_2Einteger_2Eint__ge,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x)))))))).
tff(conj_thm_2EHolSmt_2Er105,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V0x))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> p(ap(ap(c_2Einteger_2Eint__ge,inj__ty_2Einteger_2Eint(V0x)),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))).
tff(conj_thm_2EHolSmt_2Er106,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V1y)))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))).
tff(conj_thm_2EHolSmt_2Er107,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) <=> p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V0x)))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))).
tff(conj_thm_2EHolSmt_2Er108,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V0x))),inj__ty_2Einteger_2Eint(V1y))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V1y)))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))).
tff(conj_thm_2EHolSmt_2Er109,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V0x))),inj__ty_2Einteger_2Eint(V1y))),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V2z)))) <=> p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V1y)))),inj__ty_2Einteger_2Eint(V2z))))))))).
tff(conj_thm_2EHolSmt_2Er110,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x))),inj__ty_2Einteger_2Eint(V1y))),inj__ty_2Einteger_2Eint(V2z))) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V2z)))),inj__ty_2Einteger_2Eint(V0x))))))))).
tff(conj_thm_2EHolSmt_2Er111,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V1y)))),inj__ty_2Einteger_2Eint(V2z))) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V1y))),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V2z))))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2EHolSmt_2Er112,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V2z)))),inj__ty_2Einteger_2Eint(V1y))))))))).
tff(conj_thm_2EHolSmt_2Er113,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))) <=> p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V2z)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V0x)))),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V1y)))))))))).
tff(conj_thm_2EHolSmt_2Er114,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V1y))),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V2z))))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2EHolSmt_2Er115,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) <=> (~~ p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x))))))))).
tff(conj_thm_2EHolSmt_2Er116,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) <=> (~~ p(ap(ap(c_2Einteger_2Eint__ge,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))))))))).
tff(conj_thm_2EHolSmt_2Er117,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) <=> (~~ p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V0x)))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2EHolSmt_2Er118,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) <=> (~~ p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V1y)))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2EHolSmt_2Er119,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V2z))))) <=> (~~ p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V1y)))),inj__ty_2Einteger_2Eint(V2z))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))))).
tff(conj_thm_2EHolSmt_2Er120,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V2z))))) <=> (~~ p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V1y))),inj__ty_2Einteger_2Eint(V2z)))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))))).
tff(conj_thm_2EHolSmt_2Er121,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V1y))),inj__ty_2Einteger_2Eint(V2z)))) <=> (~~ p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V2z)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V0x)))),inj__ty_2Einteger_2Eint(V1y)))))))))).
tff(conj_thm_2EHolSmt_2Er122,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : ( ! [V3u:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V1y))),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V2z)),inj__ty_2Einteger_2Eint(V3u))))) <=> (~~ p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V2z)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V3u)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V0x))))),inj__ty_2Einteger_2Eint(V1y))))))))))).
tff(conj_thm_2EHolSmt_2Er123,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : ( ! [V3u:tp__ty_2Einteger_2Eint] : ( ! [V4v:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V1y))),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V2z)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V3u)),inj__ty_2Einteger_2Eint(V4v)))))) <=> (~~ p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V2z)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V3u)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V4v)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V0x)))))),inj__ty_2Einteger_2Eint(V1y)))))))))))).
tff(conj_thm_2EHolSmt_2Er124,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x))),inj__ty_2Einteger_2Eint(V1y))),inj__ty_2Einteger_2Eint(V2z))) <=> (~~ p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V2z)))),inj__ty_2Einteger_2Eint(V0x)))))))))).
tff(conj_thm_2EHolSmt_2Er125,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))),inj__ty_2Einteger_2Eint(V2z))) <=> (~~ p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V2z)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V1y)))),inj__ty_2Einteger_2Eint(V0x)))))))))).
tff(conj_thm_2EHolSmt_2Er126,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x))),inj__ty_2Einteger_2Eint(V1y)))) <=> (~~ p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x))))))))).
tff(conj_thm_2EHolSmt_2Er127,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0x)),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = V0x)))).
tff(conj_thm_2EHolSmt_2Er128,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V0x))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x))))))).
tff(conj_thm_2EHolSmt_2Er129,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V0x))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V0x))))))).
tff(conj_thm_2EHolSmt_2Er130,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V1y))),inj__ty_2Einteger_2Eint(V0x)))))))).
tff(conj_thm_2EHolSmt_2Er131,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V1y))))))))).
tff(conj_thm_2EHolSmt_2Er132,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V1y))),inj__ty_2Einteger_2Eint(V0x)))))))).
tff(conj_thm_2EHolSmt_2Er133,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0x)),ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V0x))))))).
tff(conj_thm_2EHolSmt_2Er134,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))),inj__ty_2Einteger_2Eint(V2z))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V2z))))))))))).
tff(conj_thm_2EHolSmt_2Er135,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))),inj__ty_2Einteger_2Eint(V2z))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V2z))),inj__ty_2Einteger_2Eint(V1y)))))))))).
tff(conj_thm_2EHolSmt_2Er136,lemma,(( ! [V0u:tp__ty_2Erealax_2Ereal] : ( ! [V1x:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0u))),inj__ty_2Erealax_2Ereal(V1x)))) <=> (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V0u)),inj__ty_2Erealax_2Ereal(V1x))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))).
tff(conj_thm_2EHolSmt_2Er137,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1u:tp__ty_2Erealax_2Ereal] : ( ! [V2x:tp__ty_2Erealax_2Ereal] : ((V0a = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V1u))),inj__ty_2Erealax_2Ereal(V2x)))) <=> (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V1u)),inj__ty_2Erealax_2Ereal(V2x))) = surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0a)))))))))).
tff(conj_thm_2EHolSmt_2Er138,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1x:tp__ty_2Erealax_2Ereal] : ( ! [V2y:tp__ty_2Erealax_2Ereal] : ( ! [V3z:tp__ty_2Erealax_2Ereal] : ((V0a = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V1x)),ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V2y)),inj__ty_2Erealax_2Ereal(V3z))))) <=> (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V1x)),ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V2y)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Erealax_2Ereal(V0a))),inj__ty_2Erealax_2Ereal(V3z))))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))))).
tff(conj_thm_2EHolSmt_2Er139,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1x:tp__ty_2Erealax_2Ereal] : ( ! [V2y:tp__ty_2Erealax_2Ereal] : ( ! [V3z:tp__ty_2Erealax_2Ereal] : ((V0a = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V1x)),ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V2y)),inj__ty_2Erealax_2Ereal(V3z))))) <=> (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V1x)),ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V2y)),ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V3z)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Erealax_2Ereal(V0a)))))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))))).
tff(conj_thm_2EHolSmt_2Er140,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1u:tp__ty_2Erealax_2Ereal] : ( ! [V2y:tp__ty_2Erealax_2Ereal] : ( ! [V3v:tp__ty_2Erealax_2Ereal] : ( ! [V4z:tp__ty_2Erealax_2Ereal] : ((V0a = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V1u))),inj__ty_2Erealax_2Ereal(V2y))),ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V3v)),inj__ty_2Erealax_2Ereal(V4z))))) <=> (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V1u)),inj__ty_2Erealax_2Ereal(V2y))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V3v))),inj__ty_2Erealax_2Ereal(V4z))),inj__ty_2Erealax_2Ereal(V0a)))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))))).
tff(conj_thm_2EHolSmt_2Er141,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1u:tp__ty_2Erealax_2Ereal] : ( ! [V2y:tp__ty_2Erealax_2Ereal] : ( ! [V3v:tp__ty_2Erealax_2Ereal] : ( ! [V4z:tp__ty_2Erealax_2Ereal] : ((V0a = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V1u))),inj__ty_2Erealax_2Ereal(V2y))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V3v))),inj__ty_2Erealax_2Ereal(V4z))))) <=> (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V1u)),inj__ty_2Erealax_2Ereal(V2y))),ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V0a)),ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V3v)),inj__ty_2Erealax_2Ereal(V4z))))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))))).
tff(conj_thm_2EHolSmt_2Er142,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1u:tp__ty_2Erealax_2Ereal] : ( ! [V2x:tp__ty_2Erealax_2Ereal] : ( ! [V3v:tp__ty_2Erealax_2Ereal] : ( ! [V4y:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0a))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V1u))),inj__ty_2Erealax_2Ereal(V2x))),ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V3v)),inj__ty_2Erealax_2Ereal(V4y))))) <=> (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V1u)),inj__ty_2Erealax_2Ereal(V2x))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V3v))),inj__ty_2Erealax_2Ereal(V4y)))) = V0a))))))))).
tff(conj_thm_2EHolSmt_2Er143,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1u:tp__ty_2Erealax_2Ereal] : ( ! [V2x:tp__ty_2Erealax_2Ereal] : ( ! [V3v:tp__ty_2Erealax_2Ereal] : ( ! [V4y:tp__ty_2Erealax_2Ereal] : ( ! [V5w:tp__ty_2Erealax_2Ereal] : ( ! [V6z:tp__ty_2Erealax_2Ereal] : ((V0a = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V1u))),inj__ty_2Erealax_2Ereal(V2x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V3v))),inj__ty_2Erealax_2Ereal(V4y))),ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V5w)),inj__ty_2Erealax_2Ereal(V6z)))))) <=> (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V1u)),inj__ty_2Erealax_2Ereal(V2x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V3v)),inj__ty_2Erealax_2Ereal(V4y))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V5w))),inj__ty_2Erealax_2Ereal(V6z))),inj__ty_2Erealax_2Ereal(V0a))))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))))))).
tff(conj_thm_2EHolSmt_2Er144,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1u:tp__ty_2Erealax_2Ereal] : ( ! [V2x:tp__ty_2Erealax_2Ereal] : ( ! [V3v:tp__ty_2Erealax_2Ereal] : ( ! [V4y:tp__ty_2Erealax_2Ereal] : ( ! [V5w:tp__ty_2Erealax_2Ereal] : ( ! [V6z:tp__ty_2Erealax_2Ereal] : ((V0a = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V1u))),inj__ty_2Erealax_2Ereal(V2x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V3v)),inj__ty_2Erealax_2Ereal(V4y))),ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V5w)),inj__ty_2Erealax_2Ereal(V6z)))))) <=> (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V1u)),inj__ty_2Erealax_2Ereal(V2x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V3v))),inj__ty_2Erealax_2Ereal(V4y))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V5w))),inj__ty_2Erealax_2Ereal(V6z))))) = surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0a)))))))))))))).
tff(conj_thm_2EHolSmt_2Er145,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1u:tp__ty_2Erealax_2Ereal] : ( ! [V2x:tp__ty_2Erealax_2Ereal] : ( ! [V3v:tp__ty_2Erealax_2Ereal] : ( ! [V4y:tp__ty_2Erealax_2Ereal] : ( ! [V5w:tp__ty_2Erealax_2Ereal] : ( ! [V6z:tp__ty_2Erealax_2Ereal] : ((V0a = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V1u))),inj__ty_2Erealax_2Ereal(V2x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V3v)),inj__ty_2Erealax_2Ereal(V4y))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V5w))),inj__ty_2Erealax_2Ereal(V6z)))))) <=> (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V1u)),inj__ty_2Erealax_2Ereal(V2x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V3v))),inj__ty_2Erealax_2Ereal(V4y))),ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V5w)),inj__ty_2Erealax_2Ereal(V6z))))) = surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0a)))))))))))))).
tff(conj_thm_2EHolSmt_2Er146,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1u:tp__ty_2Erealax_2Ereal] : ( ! [V2x:tp__ty_2Erealax_2Ereal] : ( ! [V3v:tp__ty_2Erealax_2Ereal] : ( ! [V4y:tp__ty_2Erealax_2Ereal] : ( ! [V5w:tp__ty_2Erealax_2Ereal] : ( ! [V6z:tp__ty_2Erealax_2Ereal] : ((V0a = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V1u))),inj__ty_2Erealax_2Ereal(V2x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V3v))),inj__ty_2Erealax_2Ereal(V4y))),ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V5w)),inj__ty_2Erealax_2Ereal(V6z)))))) <=> (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V1u)),inj__ty_2Erealax_2Ereal(V2x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V3v)),inj__ty_2Erealax_2Ereal(V4y))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V5w))),inj__ty_2Erealax_2Ereal(V6z))))) = surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0a)))))))))))))).
tff(conj_thm_2EHolSmt_2Er147,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1u:tp__ty_2Erealax_2Ereal] : ( ! [V2x:tp__ty_2Erealax_2Ereal] : ( ! [V3v:tp__ty_2Erealax_2Ereal] : ( ! [V4y:tp__ty_2Erealax_2Ereal] : ( ! [V5w:tp__ty_2Erealax_2Ereal] : ( ! [V6z:tp__ty_2Erealax_2Ereal] : ((V0a = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V1u))),inj__ty_2Erealax_2Ereal(V2x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V3v))),inj__ty_2Erealax_2Ereal(V4y))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V5w))),inj__ty_2Erealax_2Ereal(V6z)))))) <=> (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V1u)),inj__ty_2Erealax_2Ereal(V2x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V3v)),inj__ty_2Erealax_2Ereal(V4y))),ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V5w)),inj__ty_2Erealax_2Ereal(V6z))))) = surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0a)))))))))))))).
tff(conj_thm_2EHolSmt_2Er148,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1u:tp__ty_2Erealax_2Ereal] : ( ! [V2x:tp__ty_2Erealax_2Ereal] : ( ! [V3v:tp__ty_2Erealax_2Ereal] : ( ! [V4y:tp__ty_2Erealax_2Ereal] : ( ! [V5w:tp__ty_2Erealax_2Ereal] : ( ! [V6z:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0a))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V1u))),inj__ty_2Erealax_2Ereal(V2x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V3v)),inj__ty_2Erealax_2Ereal(V4y))),ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V5w)),inj__ty_2Erealax_2Ereal(V6z)))))) <=> (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V1u)),inj__ty_2Erealax_2Ereal(V2x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V3v))),inj__ty_2Erealax_2Ereal(V4y))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V5w))),inj__ty_2Erealax_2Ereal(V6z))))) = V0a))))))))))).
tff(conj_thm_2EHolSmt_2Er149,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1u:tp__ty_2Erealax_2Ereal] : ( ! [V2x:tp__ty_2Erealax_2Ereal] : ( ! [V3v:tp__ty_2Erealax_2Ereal] : ( ! [V4y:tp__ty_2Erealax_2Ereal] : ( ! [V5w:tp__ty_2Erealax_2Ereal] : ( ! [V6z:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0a))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V1u))),inj__ty_2Erealax_2Ereal(V2x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V3v)),inj__ty_2Erealax_2Ereal(V4y))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V5w))),inj__ty_2Erealax_2Ereal(V6z)))))) <=> (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V1u)),inj__ty_2Erealax_2Ereal(V2x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V3v))),inj__ty_2Erealax_2Ereal(V4y))),ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V5w)),inj__ty_2Erealax_2Ereal(V6z))))) = V0a))))))))))).
tff(conj_thm_2EHolSmt_2Er150,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1u:tp__ty_2Erealax_2Ereal] : ( ! [V2x:tp__ty_2Erealax_2Ereal] : ( ! [V3v:tp__ty_2Erealax_2Ereal] : ( ! [V4y:tp__ty_2Erealax_2Ereal] : ( ! [V5w:tp__ty_2Erealax_2Ereal] : ( ! [V6z:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0a))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V1u))),inj__ty_2Erealax_2Ereal(V2x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V3v))),inj__ty_2Erealax_2Ereal(V4y))),ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V5w)),inj__ty_2Erealax_2Ereal(V6z)))))) <=> (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V1u)),inj__ty_2Erealax_2Ereal(V2x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V3v)),inj__ty_2Erealax_2Ereal(V4y))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V5w))),inj__ty_2Erealax_2Ereal(V6z))))) = V0a))))))))))).
tff(conj_thm_2EHolSmt_2Er151,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1u:tp__ty_2Erealax_2Ereal] : ( ! [V2x:tp__ty_2Erealax_2Ereal] : ( ! [V3v:tp__ty_2Erealax_2Ereal] : ( ! [V4y:tp__ty_2Erealax_2Ereal] : ( ! [V5w:tp__ty_2Erealax_2Ereal] : ( ! [V6z:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0a))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V1u))),inj__ty_2Erealax_2Ereal(V2x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V3v))),inj__ty_2Erealax_2Ereal(V4y))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V5w))),inj__ty_2Erealax_2Ereal(V6z)))))) <=> (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V1u)),inj__ty_2Erealax_2Ereal(V2x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V3v)),inj__ty_2Erealax_2Ereal(V4y))),ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V5w)),inj__ty_2Erealax_2Ereal(V6z))))) = V0a))))))))))).
tff(conj_thm_2EHolSmt_2Er152,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1u:tp__ty_2Erealax_2Ereal] : ( ! [V2x:tp__ty_2Erealax_2Ereal] : ( ! [V3y:tp__ty_2Erealax_2Ereal] : ( ! [V4w:tp__ty_2Erealax_2Ereal] : ( ! [V5z:tp__ty_2Erealax_2Ereal] : ((V0a = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V1u))),inj__ty_2Erealax_2Ereal(V2x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Erealax_2Ereal(V3y))),ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V4w)),inj__ty_2Erealax_2Ereal(V5z)))))) <=> (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V1u)),inj__ty_2Erealax_2Ereal(V2x))),ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V4w))),inj__ty_2Erealax_2Ereal(V5z))))) = surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0a))))))))))))).
tff(conj_thm_2EHolSmt_2Er153,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1u:tp__ty_2Erealax_2Ereal] : ( ! [V2x:tp__ty_2Erealax_2Ereal] : ( ! [V3y:tp__ty_2Erealax_2Ereal] : ( ! [V4w:tp__ty_2Erealax_2Ereal] : ( ! [V5z:tp__ty_2Erealax_2Ereal] : ((V0a = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V1u))),inj__ty_2Erealax_2Ereal(V2x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Erealax_2Ereal(V3y))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V4w))),inj__ty_2Erealax_2Ereal(V5z)))))) <=> (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V1u)),inj__ty_2Erealax_2Ereal(V2x))),ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V3y)),ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V4w)),inj__ty_2Erealax_2Ereal(V5z))))) = surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0a))))))))))))).
tff(conj_thm_2EHolSmt_2Er154,lemma,(( ! [V0u:tp__ty_2Erealax_2Ereal] : ( ! [V1x:tp__ty_2Erealax_2Ereal] : ( ! [V2v:tp__ty_2Erealax_2Ereal] : ( ! [V3y:tp__ty_2Erealax_2Ereal] : ( ! [V4a:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0u))),inj__ty_2Erealax_2Ereal(V1x))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V2v))),inj__ty_2Erealax_2Ereal(V3y)))) = surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V4a)))) <=> (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V0u)),inj__ty_2Erealax_2Ereal(V1x))),ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V2v)),inj__ty_2Erealax_2Ereal(V3y)))) = V4a))))))))).
tff(conj_thm_2EHolSmt_2Er155,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1v:tp__ty_2Erealax_2Ereal] : ( ! [V2y:tp__ty_2Erealax_2Ereal] : ( ! [V3w:tp__ty_2Erealax_2Ereal] : ( ! [V4z:tp__ty_2Erealax_2Ereal] : ( ! [V5a:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Erealax_2Ereal(V0x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V1v))),inj__ty_2Erealax_2Ereal(V2y))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V3w))),inj__ty_2Erealax_2Ereal(V4z))))) = surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V5a)))) <=> (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V0x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V1v)),inj__ty_2Erealax_2Ereal(V2y))),ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V3w)),inj__ty_2Erealax_2Ereal(V4z))))) = V5a)))))))))).
tff(conj_thm_2EHolSmt_2Er156,lemma,(( ! [V0u:tp__ty_2Erealax_2Ereal] : ( ! [V1x:tp__ty_2Erealax_2Ereal] : ( ! [V2v:tp__ty_2Erealax_2Ereal] : ( ! [V3y:tp__ty_2Erealax_2Ereal] : ( ! [V4w:tp__ty_2Erealax_2Ereal] : ( ! [V5z:tp__ty_2Erealax_2Ereal] : ( ! [V6a:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0u))),inj__ty_2Erealax_2Ereal(V1x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V2v)),inj__ty_2Erealax_2Ereal(V3y))),ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V4w)),inj__ty_2Erealax_2Ereal(V5z))))) = surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V6a)))) <=> (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V0u)),inj__ty_2Erealax_2Ereal(V1x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V2v))),inj__ty_2Erealax_2Ereal(V3y))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V4w))),inj__ty_2Erealax_2Ereal(V5z))))) = V6a))))))))))).
tff(conj_thm_2EHolSmt_2Er157,lemma,(( ! [V0u:tp__ty_2Erealax_2Ereal] : ( ! [V1x:tp__ty_2Erealax_2Ereal] : ( ! [V2v:tp__ty_2Erealax_2Ereal] : ( ! [V3y:tp__ty_2Erealax_2Ereal] : ( ! [V4w:tp__ty_2Erealax_2Ereal] : ( ! [V5z:tp__ty_2Erealax_2Ereal] : ( ! [V6a:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0u))),inj__ty_2Erealax_2Ereal(V1x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V2v))),inj__ty_2Erealax_2Ereal(V3y))),ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V4w)),inj__ty_2Erealax_2Ereal(V5z))))) = surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V6a)))) <=> (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V0u)),inj__ty_2Erealax_2Ereal(V1x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V2v)),inj__ty_2Erealax_2Ereal(V3y))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V4w))),inj__ty_2Erealax_2Ereal(V5z))))) = V6a))))))))))).
tff(conj_thm_2EHolSmt_2Er158,conjecture,(( ! [V0u:tp__ty_2Erealax_2Ereal] : ( ! [V1x:tp__ty_2Erealax_2Ereal] : ( ! [V2v:tp__ty_2Erealax_2Ereal] : ( ! [V3y:tp__ty_2Erealax_2Ereal] : ( ! [V4w:tp__ty_2Erealax_2Ereal] : ( ! [V5z:tp__ty_2Erealax_2Ereal] : ( ! [V6a:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0u))),inj__ty_2Erealax_2Ereal(V1x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V2v))),inj__ty_2Erealax_2Ereal(V3y))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V4w))),inj__ty_2Erealax_2Ereal(V5z))))) = surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V6a)))) <=> (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V0u)),inj__ty_2Erealax_2Ereal(V1x))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V2v)),inj__ty_2Erealax_2Ereal(V3y))),ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V4w)),inj__ty_2Erealax_2Ereal(V5z))))) = V6a))))))))))).
