Replace irrelevance with Prop#2998

jespercockx wants to merge 2 commits into

agda:experimentalagda/agda-stdlib:experimentalfrom

jespercockx:irrelevance-through-propjespercockx/agda-stdlib:irrelevance-through-propCopy head branch name to clipboard