fact: Definition precise (U : pcm) (P : U -> Prop) := forall s1 s2 t1 t2, valid (s1 \+ t1) -> P s1 -> P s2 -> s1 \+ t1 = s2 \+ t2 -> s1 = s2.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)