proposition: Corollary find_notIn_0: forall {A:Type} {EA: EquivDec.EqDec A eq} (l: list A) v, ~ In v l -> find l v 0 = Zlength l.
proof: Proof. intros. rewrite find_notIn by auto. rewrite Z.add_0_r; auto. Qed.
imports: VST.floyd.proofauto Coq.Classes.Equivalence CertiGraph.lib.List_ext