induction l with
| nil =>
  simp [equalOnList]
| cons h t step =>
  simp [equalOnList]
  simp [beqOnSupport, List.all] at hyp
  let p₂ := step hyp.right
  exact And.intro hyp.left p₂
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 : beqOnSupport l f g = true
⊢ equalOnList l f g
no goals