int_prf1.txt

r[2] asserted 3.999999999848569e-05
r[6] rewrite 0.001185800000001791
r[1] mp 2.8799999995499093e-05
r[12] asserted 3.809999999759839e-05
r[14] rewrite 0.0016256999999981758
r[11] mp 5.069999999562924e-05
term[16] sk(~(Exists(a1, And(a == a1, A(a1))),
     And(a == a1!0, A(a1!0))))
r[16] ProofTerm(⊢ (∃a1. a = a1 ∧ A a1) ⟷ a = a1!0 ∧ A a1!0)
Gaps: ⊢ (∃a1. a = a1 ∧ A a1) ⟷ a = a1!0 ∧ A a1!0 4.8800000001847366e-05
r[16] sk 4.8800000001847366e-05
r[10] mp~ 9.390000000308873e-05
r[9] and-elim 0.0006833999999997786
r[24] and-elim 3.350000000068576e-05
r[23] monotonicity 0.00014209999999792444
r[22] symm 4.8599999999510146e-05
r[8] mp 5.270000000479058e-05
r[0] unit-resolution 0.002416900000000055