proposition: Lemma tcP x y : reflect (x \in h /\ exists n, iter' R n.+1 x y) (tc x y).
proof: Proof. case: tc_pathP=>H; constructor. - case: H=>Mx [z][p][Rxz P E]; split=>//; exists (size p). by exists z; split=>//; apply/iter'_path; exists p. case=>Mx [n /= [z][Rxz] /iter'_path [p][Sp Pzp Ly]]. by apply: H; split=>//; exists z, p. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq choice fintype path fingraph) pcm(options axioms pred prelude finmap seqext)