intro hyp₁ hyp₂
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ s₃ : FormalSum R X
⊢ eqlCoords R X s₁ s₂ → eqlCoords R X s₂ s₃ → eqlCoords R X s₁ s₃
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ s₃ : FormalSum R X
hyp₁ : eqlCoords R X s₁ s₂
hyp₂ : eqlCoords R X s₂ s₃
⊢ eqlCoords R X s₁ s₃