Issue1826.agda:60,9-22
R.elim eq
(λ {x} {y} p →
   {q : x ≡ x} {r : y ≡ y} →
   (subst (λ z → z ≡ z) p q ≡ r) ≡ (trans q p ≡ trans p r))
(λ x {q} {r} →
   trans (cong (λ x₁ → x₁ ≡ r) (subst-refl (λ z → z ≡ z) q))
   (cong₂ _≡_ (trans-reflʳ q) (trans-reflˡ r)))
(refl x)
!=
R.elim eq
(λ {x = x₁} {y} p →
   {q : x₁ ≡ x₁} {r : y ≡ y} →
   (subst (λ z → z ≡ z) p q ≡ r) ≡ (trans q p ≡ trans p r))
(λ x₁ {q} {r} →
   trans (cong (λ x₂ → x₂ ≡ r) (subst-refl (λ z → z ≡ z) q))
   (cong₂ _≡_ (trans-reflʳ q) (trans-reflˡ r)))
(refl x)
of type
{q r : x ≡ x} →
(subst (λ z → z ≡ z) (refl x) q ≡ r) ≡
(trans q (refl x) ≡ trans (refl x) r)
when checking that the expression elim-refl ? ? has type
[subst≡]≡[trans≡trans] ≡ [subst≡]≡[trans≡trans]
