fact: Definition functional_extensionality_dep_good {A} {B : A -> Type} (f g : forall x : A, B x) (H : forall x, f x = g x) : f = g := eq_trans (eq_sym (functional_extensionality_dep f f (fun _ => eq_refl))) (functional_extensionality_dep f g H).