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