fact: Definition axiom i j ts (pivot : tagged_pcm) := [/\ interp j ts = Some (untag pivot), sub_ctx i j & all (wf j) ts].
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm)