proposition: Lemma resp_Equivalence {A B} (f: A -> B) (R: relation B) {ER: Equivalence R}: Equivalence (respectful_relation f R).
proof: Proof. destruct ER. split. + apply resp_Reflexive; auto. + apply resp_Symmetric; auto. + apply resp_Transitive; auto. Qed.
imports: Coq.Classes.Morphisms Coq.Lists.List CertiGraph.lib.Relation_ext