proposition: Lemma In_inv_2 : forall k k' e e' l, InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l.
proof: Proof. inversion_clear 1; compute in H0; intuition. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses