LogRel.Utils: basic generically useful definitions, notations, tactics…

LogRel.BasicAst: definitions preceding those of the AST of terms: sorts, binder annotations…

LogRel.AutoSubst.core

LogRel.AutoSubst.unscoped

LogRel.AutoSubst.Ast

LogRel.AutoSubst.Extra: extra content to better handle the boilerplate generated by AutoSubst.

LogRel.Context: definition of contexts and operations on them.

LogRel.LContexts

LogRel.Notations: notations for conversion, typing and the logical relations.

LogRel.NormalForms: definition of normal and neutral forms, and properties.

LogRel.Weakening: definition of well-formed weakenings, and some properties.

LogRel.UntypedReduction: untyped reduction, used to define algorithmic typing.

LogRel.UntypedValues

LogRel.GenericTyping: the generic interface of typing used to build the logical relation.

LogRel.DeclarativeTyping: specification of conversion and typing, in a declarative fashion.

LogRel.DeclarativeInstance: proof that declarative typing is an instance of generic typing.

LogRel.Monad

LogRel.LogicalRelation: Definition of the logical relation

LogRel.LogicalRelation.Induction: good induction principles for the logical relation.

LogRel.LogicalRelation.Escape: the logical relation implies conversion/typing.

LogRel.LogicalRelation.ShapeView: relating reducibility witnesses of reducibly convertible types.

LogRel.LogicalRelation.Reflexivity: reflexivity of the logical relation.

LogRel.LogicalRelation.Irrelevance: symmetry and irrelevance of the logical relation.

LogRel.LogicalRelation.Transitivity

LogRel.LogicalRelation.Weakening

LogRel.LogicalRelation.Monotonicity

LogRel.LogicalRelation.Split

LogRel.LogicalRelation.Universe

LogRel.LogicalRelation.Neutral

LogRel.LogicalRelation.Reduction

LogRel.LogicalRelation.NormalRed

LogRel.LogicalRelation.Application

LogRel.LogicalRelation.SimpleArr

LogRel.LogicalRelation.Id

LogRel.Validity

LogRel.Substitution.Irrelevance

LogRel.Substitution.Monotonicity

LogRel.Substitution.Properties

LogRel.Substitution.Escape

LogRel.Substitution.Conversion

LogRel.Substitution.Reflexivity

LogRel.Substitution.Reduction

LogRel.Substitution.Split

LogRel.Substitution.SingleSubst

LogRel.Substitution.Introductions.Application

LogRel.Substitution.Introductions.Universe

LogRel.Substitution.Introductions.Poly

LogRel.Substitution.Introductions.Pi

LogRel.Substitution.Introductions.Lambda

LogRel.Substitution.Introductions.SimpleArr

LogRel.Substitution.Introductions.Var

LogRel.Substitution.Introductions.Nat

LogRel.Substitution.Introductions.Bool

LogRel.Substitution.Introductions.Empty

LogRel.Substitution.Introductions.Sigma

LogRel.Substitution.Introductions.Id

LogRel.Fundamental: declarative typing implies the logical relation for any generic instance.