proposition: Theorem In_map_iff : forall (A B : Type) (f : A -> B) (l : list A) (y : B), In y (map f l) <-> exists x, f x = y /\ In x l.
proof: Proof. intros A B f l y. split. Admitted. Theorem In_app_iff : forall A l l' (a:A), In a (l++l') <-> In a l \/ In a l'. Proof. intros A l. induction l as [|a' l' IH]. Admitted. Fixpoint All {T : Type} (P : T -> Prop) (l : list T) : Prop . Admitted. Theorem All_In : forall T (P : T -> Prop) (l : list T), (forall x, In x l -> P x) <-> All P l. Proof. Admitted. Definition combine_odd_even (Podd Peven : nat -> Prop) : nat -> Prop . Admitted. Theorem combine_odd_even_intro : forall (Podd Peven : nat -> Prop) (n : nat), (odd n = true -> Podd n) -> (odd n = false -> Peven n) -> combine_odd_even Podd Peven n. Proof. Admitted. Theorem combine_odd_even_elim_odd : forall (Podd Peven : nat -> Prop) (n : nat), combine_odd_even Podd Peven n -> odd n = true -> Podd n. Proof. Admitted. Theorem combine_odd_even_elim_even : forall (Podd Peven : nat -> Prop) (n : nat), combine_odd_even Podd Peven n -> odd n = false -> Peven n. Proof. Admitted. Check plus : nat -> nat -> nat. Check add_comm : forall n m : nat, n + m = m + n. Lemma add_comm3 : forall x y z, x + (y + z) = (z + y) + x. Proof. intros x y z. rewrite add_comm. rewrite add_comm. Abort. Lemma add_comm3_take2 : forall x y z, x + (y + z) = (z + y) + x. Proof. intros x y z. rewrite add_comm. assert (H : y + z = z + y). { rewrite add_comm. reflexivity. } rewrite H. reflexivity. Qed.