Project Page
Index
Table of Contents
PR.axioms
Axiomatic Assumptions
Functional Extensionality
Propositional Extensionality
PR.fintype
Finite Types and Mappings
Forward Function Composition
Finite Types
Type classes for renamings.
Type Classes for Substiution
Notations
PR.stlc
PR.reduction
Single-step reduction
Multi-step reduction
PR.sn_defs
Strong normalization
PR.sn_inductive_2a
PR.sn_inductive_2b
Logical Relation
PR.sn_inductive_soundness_1a
Different Characterisations Strong Normalisation
Closure Properties of sn
PR.sn_inductive_soundness_1b
Different Characterisations Strong Normalisation