Proving sort correct in Agda | Hacker News Reader