proposition: Lemma rtcP x y : reflect (x \in h /\ iter R x y) (rtc x y).
proof: Proof. by case: rtc_pathP=>[[pfx]|] H; constructor; rewrite iter_path. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq choice fintype path fingraph) pcm(options axioms pred prelude finmap seqext)