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