proposition: Theorem FunctExt_iff_EqDeltaProjs : FunctionalExtensionality <-> EqDeltaProjs.
proof: Proof. split. - intros FunExt *; apply FunExt, diagonal_projs_same_behavior. - intros EqProjs **; change f with (fun x => pi1 {|pi1:=f x; pi2:=g x; eq:=H x|}). rewrite EqProjs; reflexivity. Qed.