proposition: Lemma relation_list_inclusion: forall {A B} (R R': B -> relation A) l, (forall b, In b l -> inclusion _ (R b) (R' b)) -> inclusion _ (relation_list (map R l)) (relation_list (map R' l)).
proof: Proof. intros. induction l. + simpl. hnf; auto. + simpl map. rewrite relation_list_head. rewrite relation_list_head. apply compond_relation_inclusion. - apply H; simpl; auto. - apply IHl; intros. apply H; simpl; 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