fact: Definition local_fun (U : pcm) (f : U -> U -> option U) := forall p x y r, valid (x \+ (p \+ y)) -> f x (p \+ y) = Some r -> valid (r \+ p \+ y) /\ f (x \+ p) y = Some (r \+ p).
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)