Section Problema1.

Require Import Classical.

Variables P R : Prop.

Lemma L1 :  (P -> R) \/ (R -> P).
Proof.
...
Qed.

End Problema1.


Section Problema2.

Variables Q N H V TL : Prop.

(*
   Q  ---> Es cuadrupedo
   N  ---> Nada
   H  ---> Es herbivoro
   V  ---> Vuela
   TL ---> Toma Leche
*)

Hypothesis R1 : Q -> ~N.
Hypothesis R2 : H -> V.
Hypothesis R3 : H \/ TL.
Hypothesis R4 : V \/ ~TL.
Hypothesis R5 : V -> H /\ Q.
Hypothesis R6 : N <-> H.

Lemma L2 : False.
Proof.
...
Qed.

End Problema2.


Section Problema3.

Variable C : Set.
Variables T U : C -> C -> Prop.

Lemma L3: (exists x1:C, forall x2:C, U x1 x2 -> ~T x1 x2) ->
forall x3:C, exists x4:C, T x4 x3 -> ~U x4 x3.
Proof.
...
Qed.

End Problema3.


Section Problema4.

Variable Bool: Set.
Variable TRUE : Bool.
Variable FALSE : Bool.
Variable Not : Bool -> Bool.
Variable Imp : Bool -> Bool -> Bool.
Variable Xor : Bool -> Bool -> Bool.
Axiom Disc : ~ (FALSE = TRUE).
Axiom BoolVal : forall b : Bool, b = TRUE \/ b = FALSE.
Axiom NotTrue : Not TRUE = FALSE.
Axiom NotFalse : Not FALSE = TRUE.
Axiom ImpFalse : forall b : Bool, Imp FALSE b = TRUE.
Axiom ImpTrue : forall b : Bool, Imp TRUE b = b.
Axiom XorTrue : forall b : Bool, Xor TRUE b = Not b.
Axiom XorFalse : forall b : Bool, Xor FALSE b = b.

Lemma L41 : forall b: Bool, Xor b b = FALSE.
Proof.
...
Qed.

Lemma L42: forall b1 b2: Bool, Imp b1 b2 = FALSE -> b1 = TRUE /\ b2 = FALSE.
Proof.
...
Qed.

Lemma L43: forall b1 b2: Bool, Xor b1 b2 = TRUE -> Imp b1 (Not b2) = TRUE.
Proof.
...
Qed.


End Problema4.


Section Problema5.

Parameter ABnat : forall n : nat, Set.
Parameter null : ....
Parameter add : ...

Definition AB_3 := ...
Check AB_3.

Parameter ABGen : ...
Parameter nullGen : ...
Parameter addGen : ...

End Problema5.