import SessionCoTypes.CoinductiveRel
import SessionCoTypes.CoinductiveRelPaco
import SessionCoTypes.EQ2
import SessionCoTypes.EQ2Paco
import SessionCoTypes.EQ2Props
import SessionCoTypes.Bisim
import SessionCoTypes.Observable
import SessionCoTypes.Dual
import SessionCoTypes.FullUnfold
import SessionCoTypes.SubstCommBarendregt
import SessionCoTypes.Quotient
import SessionCoTypes.DBBridge
import SessionCoTypes.Substitute
import SessionCoTypes.Coinductive.LocalTypeC
import SessionCoTypes.Coinductive.Regularity
import SessionCoTypes.Coinductive.Bridge
import SessionCoTypes.Coinductive.ToInductive
import SessionCoTypes.Coinductive.Observable
import SessionCoTypes.Coinductive.ProjectC
import SessionCoTypes.Coinductive.Bisim
import SessionCoTypes.Coinductive.EQ2C
import SessionCoTypes.Coinductive.EQ2CProps
import SessionCoTypes.Coinductive.EQ2CEnv
import SessionCoTypes.Coinductive.FiniteSystem
import SessionCoTypes.Coinductive.RegularSystemBisim
import SessionCoTypes.Coinductive.RationalFragment
import SessionCoTypes.Coinductive.WellFormed
import SessionCoTypes.Coinductive.RegularityLemmas
import SessionCoTypes.Coinductive.Congruence
import SessionCoTypes.Coinductive.Coalgebra
import SessionCoTypes.Coinductive.Dual
import SessionCoTypes.Coinductive.ToCoindRegular
import SessionCoTypes.Coinductive.Roundtrip
import SessionCoTypes.Coinductive.BisimDecidable

/-! # SessionCoTypes

Coinductive theory on session types: EQ2 equality, bisimulation, duality,
observables, and the inductive/coinductive roundtrip bridge.
-/
