-- Compile this to validate the whole development. TODO: add a makefile for this.
module ProofRelevantPi where

   open import ProofRelevantPiCommon
   open import Action
   open import Action.Concur
   open import Action.Ren
   open import Action.Seq
   open import Action.Seq.Ren
   open import Braiding.Proc
   open import Braiding.Transition
   open import Name
   open import Proc
   open import Proc.Ren
   open import Ren
   open import Ren.Properties
   open import Transition
   open import Transition.Concur
   open import Transition.Concur.Cofinal
   open import Transition.Concur.Cofinal.Transition
   open import Transition.Ren
   open import Transition.Seq
   open import Transition.Seq.Cofinal
   open import Transition.Seq.Cofinal.Cofinal
   open import Transition.Seq.Example