proposition: Lemma tc_sub (h : seq nat) (R1 R2 : rel nat) x y : (forall x y, R2 x y -> (x \in h) && (y \in h)) -> (forall x y, R1 x y -> R2 x y) -> tc h R1 x y -> tc h R2 x y.
proof: Proof. move=>Rcond Rsub /andP [Dx] /hasP [z Dz] /andP [Rxz R]. rewrite /tc Dx; apply/hasP; exists z=>//. by rewrite (Rsub _ _ Rxz) (rtc_sub _ _ R). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq choice fintype path fingraph) pcm(options axioms pred prelude finmap seqext)