induction l with
| nil =>
  rw [equalOnList]
| cons h t step =>
  rw [equalOnList]
  apply And.intro
  rw [hyp]
  exact step
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
l : List X
f g : X → R
hyp : f = g
⊢ equalOnList l f g
no goals