proposition: Lemma relation_list_singleton: forall {A} (R: relation A), same_relation _ (relation_list (R :: nil)) R.
proof: Proof. intros. unfold relation_list; simpl. apply compond_eq_left. Qed.
imports: Coq.Classes.Morphisms Coq.Lists.List CertiGraph.lib.Coqlib CertiGraph.lib.List_ext CertiGraph.lib.List_Func_ext CertiGraph.lib.Relation_ext