proposition: Lemma resp_Reflexive {A B} (f: A -> B) (R: relation B) {RR: Reflexive R}: Reflexive (respectful_relation f R).
proof: Proof. intros. hnf; intros. unfold respectful_relation. reflexivity. Qed.
imports: Coq.Classes.Morphisms Coq.Lists.List CertiGraph.lib.Relation_ext