Issue1963I380.agda:13,16-21
Σ _A_35 _B_36 !=<
z .proj₁ ≡ y .proj₁ → _proj₂_32 (y = y) (z = z) ≡ z .proj₂
when checking that the inferred type of an application
  Σ _A_35 _B_36
matches the expected type
  z .proj₁ ≡ y .proj₁ → _proj₂_32 (y = y) (z = z) ≡ z .proj₂
