Definition prod_eqrel_pr2 {X X' : UU} (R : eqrel (X × X')) (x : X) : eqrel X'. Proof. use ((λ x' y', R (x ,, x') (x ,, y')) ,, _). abstract ( repeat split; [ intros z z' z''; apply eqreltrans | intros z; apply eqrelrefl | intros z z'; apply eqrelsymm ] ). Defined.