proposition: Lemma is_wedge_middle: forall (before: list wedgerep) (bl: list wedgerep) (after: list wedgerep) i, Forall def_wedgerep bl -> Zlength before <= i < Zlength before + Zlength bl -> is_int I32 Signed (fst (Znth i (before ++ bl ++ after))) /\ is_int I32 Signed (fst (snd (Znth i (before ++ bl ++ after)))) /\ is_int I32 Signed (snd (snd (Znth i (before ++ bl ++ after)))).
proof: Proof. intros. rewrite app_Znth2 by lia. rewrite app_Znth1 by lia. eapply Forall_Znth; eauto. lia. Qed.
imports: VST.floyd.proofauto Coq.ZArith.ZArith CertiGraph.floyd_ext.closed_lemmas CertiGraph.kruskal.kruskal_edgelist