theorem
proved
coneTerminalSide_eq_constantOneSimplex_of_lift_endpoint_eq
show as:
coneTerminalSide_eq_constantOneSimplex_of_lift_endpoint_eq