proposition: Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l.
proof: Proof. Proof with auto with ordered_type. intros k l; split; intros [y H]. - exists y... - induction H as [a l eq|a l H IH]. + destruct a as [k' y']. exists y'... + destruct IH as [e H0]. exists e... Qed.
imports: SetoidList Morphisms OrdersTac