TCR.eca
require import AllCore.
type K.
op dk : K distr.
type t_from.
type t_to.
op H : K -> t_from -> t_to.
module type ADV_TCR = {
proc c1 () : t_from
proc c2 (k:K) : t_from
}.
module TCR (A:ADV_TCR) = {
proc main() = {
var x,y,k;
x <- A.c1();
k <$ dk;
y <- A.c2(k);
return (H k x = H k y /\ x <> y);
}
}.