exact step
case cons.right
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
f g : X → R
hyp : f = g
h : X
t : List X
step : equalOnList t f g
⊢ equalOnList t f g
no goals