A wish: it would be nice if we could run iSimpl on several hypothesis: iSimpl in "H1 H2".
iSimpl
iSimpl in "H1 H2"