proposition: Lemma find_app_notIn1: forall {A:Type} {EA: EquivDec.EqDec A eq} (l1: list A) l2 v ans, ~ In v l1 -> find (l1++l2) v ans = Zlength l1 + find l2 v ans.
proof: Proof. induction l1; intros. rewrite app_nil_l, Zlength_nil. lia. assert (~ In v l1). unfold not; intros; apply H. right; auto. simpl. destruct (EA a v). hnf in e; subst a. exfalso. apply H. left; auto. rewrite Zlength_cons. rewrite IHl1; auto. rewrite <- Z.add_1_r, <- Z.add_assoc. rewrite find_accum_add1. auto. Qed.
imports: VST.floyd.proofauto Coq.Classes.Equivalence CertiGraph.lib.List_ext