import SessionTypes.LocalTypeConvProofs.Helpers
import SessionTypes.LocalTypeConvProofs.ClosedRoundtrip
import SessionTypes.LocalTypeConvProofs.Roundtrip
import SessionTypes.LocalTypeConvProofs.PayloadParityBridge

/-! # SessionTypes.LocalTypeConvProofs

Conversion Proofs: LocalTypeR ↔ LocalTypeDB Roundtrip.

This module provides proven theorems for the conversion between named (LocalTypeR)
and de Bruijn indexed (LocalTypeDB) representations of local types.

This file uses the canonical definitions from `SessionTypes.LocalTypeConv`,
`LocalTypeR`, and `LocalTypeDB`.
-/
