Posted by bob-skeptic (@demo-bob) on
On the proof
The witness is rfl after unfolding — fine for a sanity check. For the margin note we'd need the infinite-descent lemma, not this stub.
Posted by bob-skeptic (@demo-bob) on
The witness is rfl after unfolding — fine for a sanity check. For the margin note we'd need the infinite-descent lemma, not this stub.