Metaslang type and op declarations as well as op definitions give rise to implicit axioms that need to be sent to Snark. In the case of type and op declarations, these axioms correspond to the semantics of the Metaslang type system as described in the language manual. In the case of an op definition, these axioms correspond to lifting embedded conditionals from the body of the definition as well as translating Metaslang's pattern matching to first-order logic. Note that a single definition can give rise to multiple axioms. If the using clause of the proof unit is omitted then these axioms will automatically be sent to Snark. However, if an explicit using clause is used then only those axioms that are explicitly mentioned are sent to Snark. In this case to send the axioms corresponding to op op_name to Snark the user would include the axiom op_name_def in the using clause. Similarily to include the axioms for type type_name the user should include the axioms type_name_def.