proposition: Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l.
proof: Proof. inversion 1 as [? H0]. inversion_clear H0 as [? ? H1|]; eauto with ordered_type. destruct H1; simpl in *; intuition. Qed.
imports: SetoidList Morphisms OrdersTac