It would be a somewhat simple or else exceedingly slow Inference Engine that simply used the conclusion and premises of a prospective Inference Step to ascertain whether it was acceptable. Realistically, there is some further specification that narrows the class of inferences that must be considered.
For example, if there is some pattern matching involved, especially second-order pattern matching, one might achieve significant savings by specifying the substitution explicitly or at least providing some hints. A more interesting case would be the use of a Refiner which actually generates the premises from the conclusion and the justification.
The FDL design does not say what the content of the justification part of an inference step must be; that is a matter specific to the introduction of an Inference Engine. The difference in what would constitute a natural form of justification is one major indicator of difference in the natures between inference engines. Closely related engines may share the same forms of justification.
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html