proposition: Lemma some_list_list: forall {A : Type} (l : list (option A)) x, In (Some x) l <-> In x (option_list2list l).
proof: Proof. induction l. simpl. tauto. intros. simpl. split; intro. destruct H. rewrite H. auto with *. rewrite IHl in H. destruct a. auto with *. trivial. case_eq a. intros. rewrite H0 in H. simpl in H. destruct H. rewrite H. tauto. right. rewrite IHl; trivial. intros. right. rewrite IHl. rewrite H0 in H. trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical) Coq(DecidableType) Coq(FSetInterface) Coq(FSetProperties) Coq(FSetEqProperties) Coq(FSetFacts) Coq(Sumbool) Coq(Lia)