proposition: Lemma find_eq: forall {A:Type} {EA: EquivDec.EqDec A eq} (l: list A) x y acc, NoDup l -> In x l -> In y l -> find l x acc = find l y acc -> x = y.
proof: Proof. induction l; intros. contradiction. destruct H0; destruct H1. ++ subst x; subst y. auto. ++ subst x. rewrite find_cons in H2. simpl in H2. destruct (EA a y). hnf in e; subst y. trivial. rewrite find_accum_add1 in H2. pose proof (find_lbound l y acc). lia. ++ subst y. rewrite find_cons in H2. simpl in H2. destruct (EA a x). hnf in e; subst x. trivial. rewrite find_accum_add1 in H2. pose proof (find_lbound l x acc). lia. ++ simpl in H2. destruct (EA a x). hnf in e; subst x. apply NoDup_cons_2 in H; contradiction. destruct (EA a y). hnf in e; subst y. apply NoDup_cons_2 in H; contradiction. do 2 rewrite find_accum_add1 in H2. apply (IHl x y acc). apply NoDup_cons_1 in H; auto. auto. auto. lia. Qed.
imports: VST.floyd.proofauto Coq.Classes.Equivalence CertiGraph.lib.List_ext