proposition: Lemma find_In_ubound: forall {A:Type} {EA: EquivDec.EqDec A eq} (l: list A) v ans, In v l -> find l v ans < Zlength l + ans.
proof: Proof. induction l; intros. contradiction. rewrite Zlength_cons. simpl. destruct (EA a v). pose proof (Zlength_nonneg l); lia. rewrite Z.add_succ_l. rewrite find_accum_add1, Z.add_1_l. assert (find l v ans < Zlength l + ans). apply IHl. destruct H. contradiction. auto. lia. Qed.
imports: VST.floyd.proofauto Coq.Classes.Equivalence CertiGraph.lib.List_ext