fact: Definition list_rep sh l contents_mat index := let mylist := (Znth index contents_mat) in data_at sh (tarray tint size) (map Vint (map Int.repr mylist)) (list_address l index).
imports: Coq.ZArith.BinInt Coq.ZArith.Zcomplements Coq.micromega.Lia Coq.ZArith.Znat VST.floyd.proofauto CertiGraph.graph.graph_model CertiGraph.lib.List_ext CertiGraph.graph.MathAdjMatGraph