intro a ha
α : Type u
β : Type v
p q : α → Prop
f g : α → β
e : funEqOn p f g
h : ∀ (a : α), q a → p a
⊢ funEqOn q f g
α : Type u
β : Type v
p q : α → Prop
f g : α → β
e : funEqOn p f g
h : ∀ (a : α), q a → p a
a : α
ha : q a
⊢ f a = g a