Fine grained instantiation proofs
Instantiation proofs are currently not fine grained. Especially, if the quantified term is clausified, the rule tmp_quantified_cnf
is used. This is a macro placeholder rule that we should get rid of.
We discussed a fine grained instantiation rule that could replace the more coarse grained rule. This would also allow us to perform simplifications "on the fly".
One open questions is the case where the performed instantiation is simple (i.e., just applying a substitution). We could either mark this in the args, or let the reconstruction detect this.