<\body> Internally, a instance is encoded by an expression tree of type (which equals ), each subtree being either of type or . The private conversion routines between the types and are and . The public routines for the syntactic manipulation of proofs are <\explain> Proof> Boolean> Literal> <\explain> Proof> Boolean> Int> Proof> <|explain> Creation of a compound tree, testing whether an proof is a compound tree, obtaining the arity of a compound tree and accessing a child of a compound tree. <\explain> Proofs> Proofs> Proofs> Proof> <|explain> Commodity accessors for the determination of all components of a compound tree (>), of all arguments of a primitive or function call (), of all but its last arguments (), and its last argument (). <\explain> <|explain> Syntactic substitution of by in , or of each variable in the table by . <\explain> <|explain> Construct for basic axioms: the axiom corresponds to a type convertability assertion, such as , and the value to the algorithm which implements the conversion. Rules are usually templated using the construct <\explain> <|explain> Mark a part of a proof as being not yet solved. <\explain> <|explain> Universal and existential quantification. <\explain> <|explain> Basic logical connectors. <\explain> <|explain> The assertion that the type can be converted into the type . . If you don't have this file, write to the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.> <\initial> <\collection>