Equality

 

This section describes the directory lib_equality in which various definitions of equality are kept.

• Leibniz Equality
• Paulin-Mohring's Inductive Equality
• Martin-Löf's Inductive Equality
• Altenkirch-Streicher Elimination Rule