proposition: Lemma lex_spec P Q R a b (H: R<->P/\Q): compare_spec P a -> compare_spec Q b -> compare_spec R (lex a b).
proof: Proof. destruct 1; try (constructor; tauto). destruct 1; constructor; tauto. Qed.
imports: List Eqdep Eqdep_dec