fact: Definition tc (x y : nat) := (x \in h) && has (fun z => R x z && rtc z y) h.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq choice fintype path fingraph) pcm(options axioms pred prelude finmap seqext)