import SessionCoTypes.Bisim.Core
import SessionCoTypes.Bisim.UnfoldingLemmas
import SessionCoTypes.Bisim.Bisimulation
import SessionCoTypes.Bisim.EQ2Equivalence
import SessionCoTypes.Bisim.ObservableFromEQ2
import SessionCoTypes.Bisim.EQ2Extraction
import SessionCoTypes.Bisim.EQ2ToBisim
import SessionCoTypes.Bisim.Congruence
import SessionCoTypes.Bisim.Substitution
import SessionCoTypes.Bisim.UnfoldSubstitute

/-! # SessionCoTypes.Bisim

Bisimulation-style EQ2 formulation using membership predicates.

This module implements the Bisim approach from QpfTypes PR #49, adapted for LocalTypeR.
The key insight is to define membership predicates (`UnfoldsTo`, `CanAct`) that capture
observable behavior after unfolding, allowing case analysis without matching on
LocalTypeR constructors directly.

## Background

Standard coinduction on EQ2 fails for transitivity and congruence proofs because:
1. EQ2F requires matching on LocalTypeR constructors
2. Mu-unfolding creates asymmetric cases that can't be case-analyzed
3. The intermediate witness in transitivity can have arbitrary structure

The Bisim solution:
1. Define `UnfoldsTo` that captures when unfolding terminates at a base constructor
2. Define `Bisim.F` using these membership predicates instead of constructor matching
3. Transitivity works because the intermediate element doesn't need constructor matching

## Expose

The following definitions form the semantic interface for proofs:

- `UnfoldsToEnd`, `UnfoldsToVar`: predicates for unfolding to base forms
- `CanSend`, `CanRecv`: predicates for action capability
- `BisimF`: one-step bisimulation functor
- `Bisim`: membership-based weak bisimulation
- `Bisim.refl`, `Bisim.symm`, `Bisim.trans`: equivalence properties

## References

- QpfTypes PR #49: https://github.com/alexkeizer/QpfTypes/pull/49
- hxrts/QpfTypes fork: https://github.com/hxrts/QpfTypes (commit f9e16e9)
-/
