proposition: Lemma find_not_mem : forall (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2}) (a : A) (b : B) (l : list (A * B)) (dom : list A), ~In a dom -> (forall a', In a' dom -> find eqA a' ((a,b) :: l) = find eqA a' l).
proof: Proof. intros A B eqA a b l dom a_not_in_dom a' a'_in_dom; simpl; destruct (eqA a' a) as [a'_eq_a | a'_diff_a]. subst a'; absurd (In a dom); trivial. trivial. Qed.
imports: List Arith