proposition: Lemma find_app_In1: forall {A:Type} {EA: EquivDec.EqDec A eq} (l1 l2: list A) v ans, In v l1 -> find (l1++l2) v ans = find l1 v ans.
proof: Proof. induction l1; intros. contradiction. destruct (EA v a). hnf in e. subst a. simpl. destruct (EA v v). auto. unfold RelationClasses.complement, Equivalence.equiv in c; contradiction. destruct H. symmetry in H; contradiction. simpl. destruct (EA a v). symmetry in e; contradiction. rewrite IHl1; auto. Qed.
imports: VST.floyd.proofauto Coq.Classes.Equivalence CertiGraph.lib.List_ext