Next: UNIVERSE Up: The Rules Previous: SET

EQUALITY

mlsubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* formation universe_intro_equality(type number_terms): term

int

rule.

equal_equality: rule.

mlsubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* canonical axiom_equality_equal: rule.

equal_equality_variable: rule.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995