proposition: Lemma relation_list_nil: forall {A}, same_relation A (relation_list nil) eq.
proof: Proof. intros. reflexivity. Qed.
imports: Coq.Classes.Morphisms Coq.Lists.List CertiGraph.lib.Coqlib CertiGraph.lib.List_ext CertiGraph.lib.List_Func_ext CertiGraph.lib.Relation_ext