proposition: Lemma tc_pathP x y : reflect (x \in h /\ exists z p, [/\ R x z, path R z p & y = last z p]) (tc x y).
proof: Proof. rewrite /tc; case: andP=>[[Mx /hasP]|] H; constructor. - by case: H=>z ? /andP [?] /rtc_pathP [_][p]; split=>//; exists z, p. case=>Mx [z][p][Rxz P E]; have Mz : z \in h by rewrite -(Rclosed Rxz). apply: H; case: hasP=>//; case; exists z=>//; rewrite Rxz. by apply/rtc_pathP; split=>//; exists p. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq choice fintype path fingraph) pcm(options axioms pred prelude finmap seqext)