Added automatic proof of ≡→≈N.
Added doc related to Agda issue 865.
Simplified a proof.
Cosmetic change.