Project Page
Index
Table of Contents
Axiomatic Assumptions
Functional Extensionality
Propositional Extensionality
Type classes for renamings.
Type Classes for Substiution
Notations
Alogrithmic Equivalence and Definitional Equivalence are Equivalent
Stepping, multistepping, and their properties
Algorithmic Equivalence
Logical Equivalence
Main Lemma.
Declarative Equivalence