proposition: Lemma functional_extensionality_dep_good__equal_f_dep {A B} {f g : forall x : A, B x} (H : f = g) : functional_extensionality_dep_good _ _ (equal_f_dep H) = H.
proof: Proof. destruct H; simpl; apply functional_extensionality_dep_good_refl. Defined.