proposition: Corollary find_notIn: 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. intros. replace l with (l++nil). rewrite find_app_notIn1. simpl. rewrite app_nil_r; auto. auto. apply app_nil_r. Qed.
imports: VST.floyd.proofauto Coq.Classes.Equivalence CertiGraph.lib.List_ext