proposition: Lemma tc1 x y : x \in h -> y \in h -> R x y -> tc x y.
proof: Proof. by rewrite /tc=>-> Dy Rxy; apply/hasP; exists y=>//; rewrite Rxy rtc_refl. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq choice fintype path fingraph) pcm(options axioms pred prelude finmap seqext)