Recurse Center-এ আমার দ্বিতীয় সপ্তাহে Rocq-এ Dummit এবং Foote-এর অ্যাবস্ট্রাক্ট বীজগণিত ফর্মালাইজ করার সময়, আমি প্রথম প্রমাণ অনুশীলনের লক্ষ্য ভুল পেয়েছি। প্রস্তাবনাটি দাবি করে যে একটি ফাংশন ইনজেক্টিভ যদি এবং কেবল যদি তার বাম বিপরীত থাকে। কিন্তু একটি প্রতিউদাহরণ বিদ্যমান: ধরি A খালি এবং B = {1}। খালি ফাংশন f: A -> B ভ্যাকুয়াসলি ইনজেক্টিভ, তবুও কোনো ফাংশন g: B -> A বিদ্যমান নেই কারণ B অ-খালি এবং A খালি। এই কোণার কেসটি কাগজে সহজে মিস করা যায়, কিন্তু Rocq আমাকে এটি মোকাবেলা করতে বাধ্য করেছে। সংগ্রামের পরে, আমি বইয়ের errata পরীক্ষা করলাম এবং এটি তালিকাভুক্ত পেলাম। এটি হতাশাজনক ছিল কিন্তু স্বাধীনভাবে আবিষ্কার করা উত্তেজনাপূর্ণ ছিল।