dist_exists_or solved.
Add subsection title.
Add subsection title.
two_defs_of_eq_coincide solved.
Module MyEquality finished.