Because, as that quoted sentence points out, the logic itself is simpler and the creators think that makes it easier to use for teaching.

Taken to an extreme, if all you want to show off is how proofs are constructed, then whether or not your logic is actually sound doesn't matter. Since the goal of the tool isn't correct proofs, the proofs don't need to have any soundness properties.