proposition: Lemma find_diff : forall (B : Type) a1 a2, eq_bool a2 a1 = false -> forall l1 l2 b, find a2 (l1 ++ (a1,b) :: l2) = find (B:= B) a2 (l1 ++ l2).
proof: Proof. fix find_diff 5. intros B a1 a2 a2_diff_a1 l1; case l1; clear l1; simpl. revert a2_diff_a1; generalize (eq_bool_ok a2 a1); case (eq_bool a2 a1). intros _ Abs; discriminate. intros _ _ l2; reflexivity. intros p l1 l2; case p; clear p; intros a b. intros b1; case (eq_bool a2 a). reflexivity. apply find_diff; assumption. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)