{-# OPTIONS --without-K #-} module Issue712 where data _≡_ {A : Set} : A → A → Set where refl : (x : A) → x ≡ x record _×_ (A B : Set) : Set where field p1 : A p2 : B open _×_ lemma : {A B : Set} {u v : A × B} (p : u ≡ v) → p1 u ≡ p1 v lemma (refl _) = refl _