@noricoco gives an exercise.

Noricoco.agda

module Noricoco where
-- Hello! See also
-- http://togetter.com/li/312309

open import Data.Empty using (⊥-elim)
open import Data.Nat using (_≟_; ℕ)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Relation.Nullary using (yes; no)

triv : (x y z : ℕ) -> (x ≡ 3 -> y ≡ 5) ⊎ (y ≡ 5 -> z ≡ 8)
triv x y z with y ≟ 5
... | yes p = inj₁ (λ _ -> p)
... | no ¬p = inj₂ (λ q -> ⊥-elim (¬p q))

日本語による解説を書きました。http://sovmoess.tumblr.com/post/24062521384/x-y-z-x-3-y-5-y-5-z-8