Definition.LogicalRelation.Substitution.Introductions{-# OPTIONS --without-K --safe #-}
open import Definition.Typed.EqualityRelation
module Definition.LogicalRelation.Substitution.Introductions {{eqrel : EqRelSet}} where
open import Definition.LogicalRelation.Substitution.Introductions.Application public
open import Definition.LogicalRelation.Substitution.Introductions.Lambda public
open import Definition.LogicalRelation.Substitution.Introductions.Nat public
open import Definition.LogicalRelation.Substitution.Introductions.Natrec public
open import Definition.LogicalRelation.Substitution.Introductions.Pi public
open import Definition.LogicalRelation.Substitution.Introductions.SingleSubst public
open import Definition.LogicalRelation.Substitution.Introductions.Universe public