Instructing equational reasoning with otter