proposition: Lemma InA_dec : forall x l, { InA x l } + { ~ InA x l }.
proof: Proof. intros x l; induction l as [|a l IHl]. - right; auto. intro; inv. - destruct (eqA_dec x a). + left; auto. + destruct IHl. * left; auto. * right; intro; inv; contradiction. Defined.
imports: List Sorted Setoid Basics Morphisms