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)

Trivial postcondition discharge (via product coupling)

The product coupling exists for any pair of OracleComp computations, so any goal whose postcondition is structurally fun _ _ => True (or reduces to one through bind/map normalization) is closed by the leaf closer without intermediate planning.