Add `begin-irrefl` reasoning combinator#1470

MatthewDaggitt merged 4 commits intomasteragda/agda-stdlib:masterfrom

contradiction-combinatoragda/agda-stdlib:contradiction-combinatorCopy head branch name to clipboard