proposition: Lemma find_mem : forall (B : Type) (a : A) (l : list (A * B)) (b : B), find a l = Some b -> {a' : A & {l1 : list (A * B) & {l2 : list (A * B) | eqA a a' /\ l = l1 ++ (a',b) :: l2 } } }.
proof: Proof. fix find_mem 3. intros B a l b; case l; clear l; simpl. intro Abs; discriminate. intros p l; case p; clear p; intros a1 b1. generalize (eq_bool_ok a a1); case (eq_bool a a1). intros a_eq_a1 H. injection H; clear H; intro b1_eq_b. exists a1; exists (@nil (A*B)) ; exists l; subst; split. assumption. reflexivity. intros _ F; case (find_mem _ _ _ _ F). intros a' M; case M; clear M. intros l1 M; case M; clear M. intros l2 M; case M; clear M. intros a_eq_a' M. exists a'; exists ((a1,b1) :: l1); exists l2; repeat split. assumption. subst l; reflexivity. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)