proposition: Lemma rtc1 x y : x \in h -> y \in h -> R x y -> rtc x y.
proof: Proof. rewrite /rtc=>Dx Dy Rxy; case: decP=>// Dx'; case: decP=>// Dy'. by apply/connectP; exists [:: Sub y Dy']=>//=; rewrite andbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq choice fintype path fingraph) pcm(options axioms pred prelude finmap seqext)