proposition: Lemma eq_couple_dec : forall (E F : Set) (eq_E_dec : eq_dec E) (eq_F_dec : eq_dec F) (x1 x2 : E) (y1 y2 : F), {x1 = x2 /\ y1 = y2} + {x1 <> x2 \/ y1 <> y2}.
proof: Proof. intros; case (eq_E_dec x1 x2); case (eq_F_dec y1 y2); intros; auto. Qed.
imports: Arith Omega List