proposition: Lemma Znth_0_hd: forall list, Zlength list > 0 -> Znth 0 list = hd 0 list.
proof: Proof. intros. induction list; inversion H. rewrite Znth_0_cons. trivial. Qed.
imports: VST.floyd.proofauto Coq.Classes.Equivalence CertiGraph.lib.List_ext