proposition: Lemma pair_compare_spec: forall x y, compare_spec (x=y) (pair_compare x y).
proof: Proof. unfold pair_compare. intros [? ?] [? ?]; simpl; repeat case cmp_spec; constructor; congruence. Qed.
imports: List Eqdep Eqdep_dec