proposition: Lemma semi_iso_refl: forall g from to, sound_gc_graph g -> gen_unmarked g from -> gc_graph_semi_iso g g from to nil.
proof: Proof. intros. red. split3; intros; [easy | easy |]. destruct (split []) eqn:? . simpl in Heqp. inversion Heqp. subst. clear Heqp. split3; [| | easy]. - red. split. 1: constructor. intros; split; intros. 2: inversion H1. destruct H1 as [? [? ?]]. destruct H as [? _]. red in H. rewrite H in H2. red in H0. destruct H2. rewrite H3 in *. destruct v as [? idx]. simpl in *. subst n. specialize (H0 H2 _ H4). rewrite H1 in H0. inversion H0. - red. split. 1: constructor. split; [split|]; intros; intuition auto with *. Qed.
imports: Coq.ZArith.ZArith Coq.Program.Basics compcert.lib.Integers compcert.common.Values VST.veric.base VST.veric.Clight_lemmas VST.veric.val_lemmas VST.veric.shares VST.msl.seplog VST.msl.shares VST.zlist.sublist VST.floyd.coqlib3 VST.floyd.functional_base VST.floyd.data_at_rec_lemmas CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.graph_isomorphism CertiGraph.graph.reachable_ind CertiGraph.CertiGC.GCGraph