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

postulate A : Set
postulate B : A → Set
postulate a₀ a₁ : A
postulate p : a₀ ≡ a₁
postulate b₀ : B a₀

b₁ : B a₁
b₁ = {!!}