proposition: Lemma respectful_relation_list: forall {B A} (f: B -> A) (l: list (relation A)), inclusion _ (relation_list (map (respectful_relation f) l)) (respectful_relation f (relation_list l)).
proof: Proof. intros; hnf; intros. revert x y H; induction l; intros. + unfold relation_list in H. simpl in *. subst. reflexivity. + simpl. erewrite app_same_relation by (rewrite relation_list_head; reflexivity). apply respectful_compond_relation. simpl in H. erewrite app_same_relation in H by (rewrite relation_list_head; reflexivity). inversion H; subst. apply compond_intro with y0; auto. Qed.
imports: Coq.Classes.Morphisms Coq.Lists.List CertiGraph.lib.Coqlib CertiGraph.lib.List_ext CertiGraph.lib.List_Func_ext CertiGraph.lib.Relation_ext