rw [←Subtype.coe_inj] at heq
case intro.inl.intro.intro
left✝² : R3 2 3 → R3 3 1 → R3 2 1
left✝¹ : ¬R3 2 3
left✝ : ¬R3 3 2
heq : 2 = 3
⊢ False
case intro.inl.intro.intro
left✝² : R3 2 3 → R3 3 1 → R3 2 1
left✝¹ : ¬R3 2 3
left✝ : ¬R3 3 2
heq : ↑2 = ↑3
⊢ False