proposition: Lemma rtc_idemp (h : seq nat) (R : rel nat) : (forall x y, R x y -> (x \in h) && (y \in h)) -> rtc h (rtc h R) =2 rtc h R.
proof: Proof. move=>Rcond x y. have X : forall x y, R x y -> (x \in h) = (y \in h). - by move=>?? /Rcond/andP [->->]. apply/idP/idP; last first. - by move=>H; case/andP: (rtc_closed X H)=>Dx Dy; apply: rtc1. case/(rtcT (rtc_closed X) (@rtc_trans h R))/orP=>//. by case/andP=>/eqP <-; apply: rtc_refl. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq choice fintype path fingraph) pcm(options axioms pred prelude finmap seqext)