proposition: Lemma eq_relation_list: forall {A B} {R: relation A} {EqRA: Equivalence R} (l: list B), inclusion _ (relation_list (map (fun _ => R) l)) R.
proof: Proof. intros. induction l. + simpl; rewrite relation_list_nil. hnf; intros. subst; reflexivity. + simpl map. rewrite relation_list_head. hnf; intros. inversion H; subst. transitivity y0. - auto. - apply IHl; 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