Proof support for Guarded2Network's refinement proof. Everything about the pass itself — the AST transformation, its own denotational semantics, the correctness statement — lives elsewhere; this file is where the reasoning-specific machinery accumulates.

Guarded2Network.PlusCal's pass runs monad-polymorphically, and a proof pins it to G2NM (Guarded2Network.Lemmas.Monad, where the reasoning behind the choice is written down).

Tactic validation

A check that gcongr fires on the goal shape it exists for.