proposition: Lemma list_compare_spec: forall h k, compare_spec (h=k) (list_compare h k).
proof: Proof. induction h as [|x h IH]; destruct k; simpl; try case cmp_spec; try case IH; constructor; congruence. Qed.
imports: List Eqdep Eqdep_dec