proposition: Lemma optionList2list_In : forall (x:A) (l:list (option A)), In x (optionList2list l) <-> In (Some x) l.
proof: Proof. intros x l. induction l. simpl. intuition. case a. intro a0. simpl. intuition. left. rewrite H2. reflexivity. left. injection H2. intro; assumption. simpl. intuition. discriminate H2. Qed.
imports: Coq(List)