clutch.approxis.approxis

From stdpp Require Import namespaces.
From clutch.prob_lang Require Export notation tactics metatheory.
From clutch.prob_lang Require Export lang.
From clutch.prob_lang.spec Require Export spec_rules spec_tactics.
From clutch.approxis Require Export app_weakestpre lifting ectx_lifting primitive_laws proofmode coupling_rules
    model compatibility app_rel_rules rel_tactics interp soundness .