proposition: Lemma functional_extensionality_dep_good_refl {A B} f : @functional_extensionality_dep_good A B f f (fun _ => eq_refl) = eq_refl.
proof: Proof. unfold functional_extensionality_dep_good; edestruct functional_extensionality_dep; reflexivity. Defined.