proposition: Lemma functional_extensionality_dep_good__equal_f {A B} {f g : A -> B} (H : f = g) : functional_extensionality_dep_good _ _ (equal_f H) = H.
proof: Proof. destruct H; simpl; apply functional_extensionality_dep_good_refl. Defined.