proposition: Lemma rtc_cond x y : rtc x y -> (x \in h) = (y \in h).
proof: Proof. by case/rtc_closed/andP=>->->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq choice fintype path fingraph) pcm(options axioms pred prelude finmap seqext)