TY - RPRT TI - A Proof of the Schröder-Bernstein Theorem in ACL2 AU - Grant Jurgensen PY - 2025 DO - 10.4204/eptcs.423.3 UR - https://arxiv.org/abs/2507.19008 ID - 2507.19008 ER -