+lemma eqP_union_l: ∀U.∀A,B,C:U →Prop.
+ B ≐ C → A ∪ B ≐ A ∪ C.
+#U #A #B #C #eqBC #a @iff_or_l @eqBC qed.
+
+(************************ Sets with decidable equality ************************)
+
+(* We say that a property P:A → Prop over a datatype A is decidable when we have
+an effective way to assess the validity of P a for any a:A. As a consequence of
+Goedel incompleteness theorem, not every predicate is decidable: for instance,
+extensional equality on sets is not decidable, in general.
+
+Decidability can be expressed in several possible ways. A convenient one is to
+state it in terms of the computability of the characterisitc function of the
+predicate P, that is in terms of the existence of a function Pb: A → bool such
+that
+ P a ⇔ Pb a = true
+
+Decidability is an important issue, and since equality is an essential
+predicate, it is always interesting to try to understand when a given notion of
+equality is decidable or not.
+
+In particular, Leibniz equality on inductively generated datastructures is often
+decidable, since we can simply write a decision algorithm by structural
+induction on the terms. For instance we can define characteristic functions for
+booleans and natural numbers in the following way: *)
+
+definition beqb ≝ λb1,b2.
+ match b1 with [ true ⇒ b2 | false ⇒ notb b2].
+
+let rec neqb n m ≝
+match n with
+ [ O ⇒ match m with [ O ⇒ true | S q ⇒ false]
+ | S p ⇒ match m with [ O ⇒ false | S q ⇒ neqb p q]
+ ].
+
+(* It is so important to know if Leibniz equality for a given type is decidable
+that turns out to be convenient to pack this information into a single algebraic
+datastructure, called DeqSet: *)
+
+record DeqSet : Type[1] ≝
+ { carr :> Type[0];
+ eqb: carr → carr → bool;
+ eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)}.
+
+notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
+interpretation "eqb" 'eqb a b = (eqb ? a b).
+
+(* A DeqSet is simply a record composed by a carrier type carr, a boolean
+function eqb: carr → carr → bool representing the decision algorithm, and a
+proof eqb_true that the decision algorithm is correct. The :> symbol declares
+carr as a coercion from a DeqSet to its carrier type. We use the infix notation
+``=='' for the decidable equality eqb of the carrier.
+
+We can easily prove the following facts: *)
+
+lemma beqb_true_to_eq: ∀b1,b2. beqb b1 b2 = true ↔ b1 = b2.
+* * % // normalize #H >H //