as an layperson's example[0], https://incredible.pm is WIMP, but the structured interaction interface of https://profs.info.uaic.ro/~stefan.ciobaca/lnd.html is far easier to drive (and could've been keyboard driven) once one understands how to do so.
[0] although these are both trivial compared to a "real" prover, eg https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_g...