A formal proof in Coq of Cantor-Bernstein-Schroeder’s theorem without axiom of choice (2019). https://www.researchgate.net/publication/339270363_A_Formal_Proof_in_Coq_of_Cantor-Bernstein-Schroeder's_Theorem_without_axiom_of_choice #ITP #Coq #SetTheory
