proposition: Lemma tc_idemp (h : seq nat) (R : rel nat) : (forall x y, R x y -> (x \in h) && (y \in h)) -> tc h (tc h R) =2 tc h R.
proof: Proof. move=>Rcond x y; rewrite (tcT _ (@tc_trans _ _)) //. by apply: tc_closed=>?? /Rcond/andP [->->]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq choice fintype path fingraph) pcm(options axioms pred prelude finmap seqext)