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