proposition: Lemma Znth_find: forall (l: list Z) target, In target l -> Znth (find l target 0) l = target.
proof: Proof. intros. replace (find l target 0) with (find l target 0 - 0) by lia. apply Znth_find_gen; [lia | assumption]. Qed.
imports: VST.floyd.proofauto Coq.Classes.Equivalence CertiGraph.lib.List_ext