(* typ bool *)

Inductive bool:Set:=true:bool|false:bool.

Definition b_or : bool -> bool -> bool := ...

Definition b_and : bool -> bool -> bool := ...

Definition b_not : bool -> bool := ...

Theorem b_Morgan1 : (b1,b2:bool)(b_not (b_and b1 b2))=(b_or (b_not b1) (b_not b2)).

Theorem b_Morgan2 : (b1,b2:bool)(b_not (b_or b1 b2))=(b_and (b_not b1) (b_not b2)).

(* typ nat *)

Definition pred:nat->nat := ...

Print pred.

Lemma pred_S : (n:nat)(pred (S n))=n.

Lemma S_pred : (n:nat)(n=O)\/(S(pred n))=n.

(* proste relacje indukcyjne *)

Inductive Even : nat -> Prop :=
   evenO : (Even O)
 | evenSS : (n:nat)(Even n) -> (Even (S (S n))).

Lemma SS_Even : (n:nat)(Even n) -> (Even (S (S n))).

Mutual Inductive Ev : nat -> Prop :=
 | evO : (Ev O)
 | evS : (n:nat)(Odd n) -> (Ev (S n))

with Odd : nat -> Prop :=
 | oddS : (n:nat)(Ev n) -> (Odd (S n)).

Lemma SS_Odd : (n:nat)(Odd n) -> (Odd (S (S n))).

Lemma Odd_SS : (n:nat)(Odd n) -> (Ev (pred n)).