simp
M : Type u_1
inst✝⁴ : Zero M
inst✝³ : One M
inst✝² : Add M
inst✝¹ : Mul M
inst✝ : LT M
s : Structure ℒₒᵣ M
hZero : Structure.Zero ℒₒᵣ M
hOne : Structure.One ℒₒᵣ M
hAdd : Structure.Add ℒₒᵣ M
hMul : Structure.Mul ℒₒᵣ M
hEq : Structure.Eq ℒₒᵣ M
hLT : Structure.LT ℒₒᵣ M
k : ℕ
r : ℒₒᵣ.Rel k
x✝ : Fin 2 → M
⊢ Structure.rel op(<) x✝ = Structure.rel op(<) x✝
no goals