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