import SessionCoTypes.EQ2.Core
import SessionCoTypes.EQ2.TransBase

/-! # SessionCoTypes.EQ2

Coinductive equality (EQ2) for local types.

## Expose

The following definitions form the semantic interface for proofs:

- `EQ2`: coinductive equality (greatest fixed point of EQ2F)
- `eq2_refl`: reflexivity of EQ2
- `eq2_symm`: symmetry of EQ2
- `eq2_trans_wf`: transitivity of EQ2 (via Bisim, in EQ2Props.lean)
- `EQ2_equiv`: equivalence relation instance
- `eq2_trans_via_end` / `eq2_trans_via_var`: constructor-based transitivity helpers
- `eq2_unfold_left`: left unfolding preserves EQ2
- `eq2_unfold_right`: right unfolding preserves EQ2
- `eq2_unfold`: bilateral unfolding preserves EQ2
- `eq2_coind`: coinduction principle
-/
