exact step
case tail
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
l : List X
f g : X → R
x h : X
t : List X
hyp : f h = g h ∧ equalOnList t f g
a✝ : List.Mem x t
inTail : x ∈ t
step : f x = g x
⊢ f x = g x
no goals