proposition: Lemma resp_Transitive {A B} (f: A -> B) (R: relation B) {TR: Transitive R}: Transitive (respectful_relation f R).
proof: Proof. intros. hnf; intros. unfold respectful_relation. transitivity (f y); auto. Qed.
imports: Coq.Classes.Morphisms Coq.Lists.List CertiGraph.lib.Relation_ext