proposition: Lemma si_list: forall {A} (l: list A) (G1 G2: Graph), relation_list (map (fun _ (G1 G2: Graph) => G1 ~=~ G2) l) G1 G2 -> G1 ~=~ G2.
proof: Proof. intros until l. pose proof @resp_Equivalence Graph _ pg_lg structurally_identical. apply eq_relation_list. Qed.
imports: Coq.Logic.ProofIrrelevance CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.lib.Equivalence_ext