-- agda 2.5.99.20181017-9

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

data Fin : ℕ → Set where
  zero : ∀{n} → Fin (suc n)
  suc  : ∀{n} → Fin n → Fin (suc n)

pf : {n : ℕ} {x y : Fin n} → x ≡ y → _≡_ {Fin (suc n)} (suc x) (suc y)
pf refl = refl

-- Ideally this should work, but it won't
pf₂ : {n : ℕ} {x y : Fin n} → x ≡ y → suc x ≡ suc y
pf₂ refl = refl

-- In fact, if
postulate α : Fin (suc zero)
-- then agda can't find the type of
β : ?
β = suc α