Next:
Logic
Up:
The LEGO library -
Previous:
Conventions
Providing logic and equality
Logic
Equality
Martin-Löf's Inductive Equality
Leibniz Equality
Paulin-Mohring's Inductive Equality
Altenkirch-Streicher Elimination Rule
Theorems about Equality
Setoids
Lego
1998-06-15
