We should be able to define "deduced steps" helpers for the kernel in a unified way. This should first include versions of basis proofsteps with most arguments automatically infered, and then steps such as InstantiateForall and others, who should be encapsulated in subproofs.
We should be able to define "deduced steps" helpers for the kernel in a unified way. This should first include versions of basis proofsteps with most arguments automatically infered, and then steps such as InstantiateForall and others, who should be encapsulated in subproofs.