eqeqqi Show Code edit
## Convert Natural to Rational Equality
thm (eqeqqi () (hyp (z.= A B)) (= A B)
hyp
(z.= A B)
A B eqeqq
(-> (z.= A B) (= A B))
ax-mp
(= A B)
)
edit