u : Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
b : R
⊢ b = b
u : Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a c b : R
x✝¹ : a = c
x✝ : b = c
⊢ a = b
subst_vars
no goals
u : Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
b : R
⊢ b = b
rfl