proposition: Lemma rtc_pathP x y : reflect (x \in h /\ exists2 p, path R x p & y = last x p) (rtc x y).
proof: Proof. case V : (rtc x y); constructor. - move: V; rewrite /rtc; case: decP=>// pfx; case: decP=>// pfy. case/connectP=>p P E; split=>//; rewrite (_ : x = ssval (Sub x pfx)) //. have {E} Ey : y = ssval (last (Sub x pfx) p) by rewrite -E. exists (map (@ssval _ _) p); last by rewrite last_map. by rewrite (map_path (e':=Rtp) (b:=pred0)) //; apply/hasP; case. case=>Mx [p P Ey]; move: V; rewrite /rtc. case: decP=>// {Mx} pfx; case: decP=>[pfy|]; last first. - move: (mem_last x p) pfx; rewrite -Ey inE=>/orP [/eqP ->->//|]. elim: p x P Ey=>[|p ps IH] //= x /andP [Rxp P] Ey. by rewrite inE (Rclosed Rxp); case: eqP=>[-> _|_ My] //; apply: IH. case/connectP; elim: p x pfx P Ey=>[|p ps IH] /= x pfx P Ey. - by rewrite Ey /= in pfy *; rewrite (bool_irrelevance pfx); exists [::]. case/andP: P=>Rxp P; move: {-}(pfx); rewrite (Rclosed Rxp)=>pfp. by case: (IH p pfp P Ey)=>q; exists (Sub p pfp :: q)=>//; apply/andP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq choice fintype path fingraph) pcm(options axioms pred prelude finmap seqext)