proposition: Lemma path_closed x p : path R x p -> (x \in h) = (last x p \in h).
proof: Proof. by elim: p x=>[|z p IH] x //= /andP [Rxz /IH <-]; apply: Rclosed. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq choice fintype path fingraph) pcm(options axioms pred prelude finmap seqext)