proposition: Lemma find_not_mem : equivalence _ eqA -> forall (B : Type) (a : A) (b : B) (l : list (A * B)) (dom : list A), ~mem a dom -> (forall a', mem a' dom -> find a' ((a,b) :: l) = find a' l).
proof: Proof. intros eq_proof B a b l dom a_not_in_dom a' a'_in_dom; simpl. generalize (eq_bool_ok a' a); case (eq_bool a' a). intro a'_eq_a; apply False_rect; apply a_not_in_dom. apply (mem_eq_mem eq_proof dom a'_eq_a); assumption. intros _; reflexivity. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)