open import Definition.Typed.EqualityRelation
open import Definition.Typed.Restrictions
module Definition.LogicalRelation.Substitution.Introductions
{a} {M : Set a}
(R : Type-restrictions M)
{{eqrel : EqRelSet R}}
where
open import Definition.LogicalRelation.Substitution.Introductions.Pi R public
open import Definition.LogicalRelation.Substitution.Introductions.SingleSubst R public
open import Definition.LogicalRelation.Substitution.Introductions.Lambda R public
open import Definition.LogicalRelation.Substitution.Introductions.Application R public
open import Definition.LogicalRelation.Substitution.Introductions.Prod R public
open import Definition.LogicalRelation.Substitution.Introductions.Fst R public
open import Definition.LogicalRelation.Substitution.Introductions.Snd R public
open import Definition.LogicalRelation.Substitution.Introductions.ProdBetaEta R public
open import Definition.LogicalRelation.Substitution.Introductions.Prodrec R public
open import Definition.LogicalRelation.Substitution.Introductions.DoubleSubst R public
open import Definition.LogicalRelation.Substitution.Introductions.Nat R public
open import Definition.LogicalRelation.Substitution.Introductions.Natrec R public
open import Definition.LogicalRelation.Substitution.Introductions.Empty R public
open import Definition.LogicalRelation.Substitution.Introductions.Emptyrec R public
open import Definition.LogicalRelation.Substitution.Introductions.Unit R public
open import Definition.LogicalRelation.Substitution.Introductions.Universe R public
open import Definition.LogicalRelation.Substitution.Introductions.Var R public