Reducibility A (slow!) ongoing conversion of iehality's Reducibilities from Lean 3 to Lean 4. In Progress lib.lean