We assume the basic form of proof is a dag (directed acyclic graph) of Inference Steps where the conclusion of a child inference is a premise of its parent inference. An essential part of what makes a proof convincing is that all the individual inferences are verified by a convincing Inference Engine or a compatible collection of inference engines. The notion of Proposition is that it is the unit of matching adjacent inferences in a proof.
If the proof is a rooted dag then we may construe the proof as deriving the root conclusion from the leaf premises.
That some dag of inferences is a proof constrained to certain methods is a matter of Certification. It is intended that multiple, diverse, even incompatible criteria for acceptable inference be permitted to coexist in the FDL, and so one must be careful when certifying a proof that one limits ones inferences by stipulation to acceptable and compatible methods, for example by employing Sentinel expressions.
One can devise secondary forms of proof with more structure from which a basic proof (dag) can determined. Such a proof can be considered as a presentation of a basic proof. For example, one might want to use a block style natural deduction organization of inferences, where the propositions at each inference are derived partly from the whole block-form proof as a context.
See Proof Organization.
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html