proposition: Lemma rtsc_congruence {B} (f : A → B) (R' : relation B) x y : (∀ x y, R x y → R' (f x) (f y)) → rtsc R x y → rtsc R' (f x) (f y).
proof: Proof. unfold rtsc; eauto using rtc_congruence, sc_congruence. Qed.
imports: stdpp(options)