fact: Definition res (U : pcm) (V : tpcm) (f : U -> V) (S : rel U) := fun x : U => if S x Unit then f x else undef.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)