transformations should complain when given too many arguments
for example, if one types "introduce_premises a,b,H" then it introduces without using the names given. Of course the mistake is that "intros a,b,H" should be used instead. Why the generic engine for transformations did not detect that?
To upload designs, you'll need to enable LFS. More information