take id X ; :: thesis: id X is one-to-one
thus id X is one-to-one ; :: thesis: verum