Section Problema1. (* PROBLEMA 1 *)

Variable NM RED CONS UTIL : Prop.

Hypothesis H1 : NM -> not RED.
Hypothesis H2 : CONS \/ not UTIL.

Lemma lema1 : ...
Proof.
...
Qed.

End Problema1.


Section Problema2. (* PROBLEMA 2 *)

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

Lemma lema2: (forall (x y : C), (U x y -> ~(T x y))) /\ (exists z : C, T z z) 
           -> exists w : C, ~(U w w).
Proof.
...
Qed.

End Problema2.


Section Problema3. (* PROBLEMA 3 *)

Variable Bool: Set.
Variable TRUE : Bool.
Variable FALSE : Bool.

Variable Not : Bool -> Bool.
Variable Or : Bool -> Bool -> Bool.
Variable And : Bool -> Bool -> Bool.

Axiom BoolVal : forall b : Bool, b = TRUE \/ b = FALSE.

Axiom NotTrue : Not TRUE = FALSE.
Axiom NotFalse : Not FALSE = TRUE.

Axiom AndTrue : forall b : Bool, And TRUE b = b.
Axiom AndFalse : forall b : Bool, And FALSE b = FALSE.

Axiom OrTrue : forall b : Bool, Or TRUE b = TRUE.
Axiom OrFalse : forall b : Bool, Or FALSE b = b.

Lemma lema3_1 : forall b : Bool, Not (Not b) = b.
Proof.
...
Qed.

Lemma lema3_2 : forall b1 b2 : Bool, Not (Or b1 b2) = And (Not b1) (Not b2).
Proof.
...
Qed.

Lemma lema3_3 : forall b1 : Bool, exists b2 : Bool, And b1 b2 = Or b1 b2.
Proof.
...
Qed.

End Problema3.


Section Problema4. (* PROBLEMA 4 *)

Parameter Array : Set -> nat -> Set.
(* a*)
Parameter empty : ...
Check empty.

(* b *)
Parameter add : ...
Check add.

(* c *)
Definition A2 := ... (* arreglo de largo 2 *)
Definition A4 := ... (* arreglo de largo 4 *)
Definition A6 := ... (* arreglo de largo 6 pedido con elementos del 1 al 6 *) 
Check A6.

(* d *)
Parameter ...

Definition A3 := ... (* arreglo de largo 3 pedido con elementos 7, 8 y 9 *)
Check A3.

End Problema4.
  

Section Problema5.

Variable S : Set.
Variable e1 e2 : S.
Variable P1 P2 : S -> S -> Prop.
Variable P3 P4 : S -> Prop.

Lemma lema5_1 : (forall x y : S, P1 x y -> P2 y x) -> (P1 e1 e2) ->  P2 e2 e1.
Proof.
     exact ...
Qed.

Lemma lema5_2 : (forall x:S, P3 x) \/ (forall y:S, P4 y) -> forall z:S, P3 z \/ P4 z.
Proof.
    ...
Qed. 

End Problema5.