Relational program-logic examples

This file gives small compositionality examples for:

• heterogeneous transformer stacks (StateT vs OptionT/ExceptT), and
• the OracleComp relational API (RelTriple).

Term-mode examples (direct lemma application)

Tactic-mode examples (using rvcstep)