Require Import Classical_Prop.

Parameters A B C : Prop.

(* Hinweis: Geben Sie Ihr fertiges Coq-Skript unbedingt als .v-Datei ab,
   weil sonst keine Korrektur möglich ist. *)
(* Bei Unklarheiten können Sie das Coq-Intro auf der Webseite als Nachschlagewerk
   nutzen und auch gerne Fragen im GLoIn-Forum stellen! *)

Lemma or_below : A \/ B -> (A -> B) -> B.
Proof.
  (* Hier einen Beweis einfügen und Admitted. dann durch Qed. ersetzen! *)
Admitted.

Lemma uncurry : (A -> B -> C) ->  A /\ B -> C.
Proof.
  (* Hier einen Beweis einfügen und Admitted. dann durch Qed. ersetzen! *)
Admitted.

Lemma negor : ~(A \/ B)  ->  ~A /\ ~B.
Proof.
  (* Hier einen Beweis einfügen und Admitted. dann durch Qed. ersetzen! *)
Admitted.

Lemma tnd : A \/ ~A.
Proof.
  (* Hier einen Beweis einfügen und Admitted. dann durch Qed. ersetzen! *)
Admitted.

Lemma deMorgan3 : ~A \/ ~B \/ ~C -> ~(A /\ B /\ C).
Proof.
  (* Hier einen Beweis einfügen und Admitted. dann durch Qed. ersetzen! *)
Admitted.