take id A ; :: thesis: id A is involutive
thus id A is involutive ; :: thesis: verum