unfold restrict
α : Type u_1
β : Type u_2
s : Set α
f g : α ⇀ β
h : ∀ a ∈ s, f a = g a
inst✝ : DecidablePred fun x => x ∈ s
⊢ restrict f s = restrict g s
α : Type u_1
β : Type u_2
s : Set α
f g : α ⇀ β
h : ∀ a ∈ s, f a = g a
inst✝ : DecidablePred fun x => x ∈ s
⊢ (fun a => if a ∈ s then f a else none) = fun a => if a ∈ s then g a else none