proposition: Lemma find_accum_add1: forall {A:Type} {EA: EquivDec.EqDec A eq} (l: list A) v ans1 ans2, find l v (ans1+ans2) = ans1 + find l v ans2.
proof: Proof. induction l; intros. simpl. auto. simpl. destruct (EA a v). auto. replace (1+(ans1+ans2)) with (ans1 + (1+ans2)) by lia. apply IHl. Qed.
imports: VST.floyd.proofauto Coq.Classes.Equivalence CertiGraph.lib.List_ext