proposition: Lemma tc_closed x y : tc x y -> (x \in h) && (y \in h).
proof: Proof. case/tc_pathP=>Mx [z][p][Rxz /path_closed Px ->]. by rewrite -Px -(Rclosed Rxz) Mx. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq choice fintype path fingraph) pcm(options axioms pred prelude finmap seqext)