proposition: Lemma relation_list_conjunction: forall {A B} (R R': B -> relation A) l, inclusion _ (relation_list (map (fun b => relation_conjunction (R b) (R' b)) l)) (relation_conjunction (relation_list (map R l)) (relation_list (map R' l))).
proof: Proof. intros. simpl. induction l. - simpl. rewrite relation_list_nil. hnf; intros. rewrite relation_conjunction_iff. auto. - simpl map. rewrite !relation_list_head. hnf; intros. inv H. apply IHl in H1. rewrite relation_conjunction_iff. destruct H0, H1. split; 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