clutch.foxtrot.foxtrot

From stdpp Require Import namespaces.
From clutch.con_prob_lang Require Export notation tactics metatheory.
From clutch.con_prob_lang Require Export lang.
From clutch.con_prob_lang.spec Require Export spec_tactics.
From clutch.foxtrot Require Export weakestpre lifting ectx_lifting primitive_laws proofmode error_rules coupling_rules adequacy.

From clutch.foxtrot.unary_rel Require Export
    unary_model unary_interp unary_fundamental.

From clutch.foxtrot.binary_rel Require Export
    binary_model binary_adequacy_rel binary_interp binary_soundness.