(* normalna definicja w Prop *)

Print or.

(* wlaczyc low-level contents *) 
Goal forall A B, A\/B -> B\/A.
destruct 1; auto.
Show Proof.
Qed.

Goal forall A B, A\/B -> nat.
try destruct 1.
Admitted.

Goal forall A B, A\/B -> Prop.
try destruct 1.
Admitted.


(* singletony w Prop *)
(* Prop -=-> Set *)
Print and.
Goal forall A B, A/\B -> nat.
destruct 1.
exact O.
Show Proof.
Qed.

(* Prop -=-> Set *)
Print sig.
Goal forall n, n=0/\n=1 -> {n:nat | n=0}.
destruct 1.
exists n.
assumption.
Show Proof.
Qed.

(* Prop -=-> Prop *)
Goal forall A B, A/\B -> B/\A.
destruct 1; auto.
Show Proof.
Qed.

(* Prop -=-> Type *)
Goal False -> Prop.
destruct 1.
Show Proof.
Qed.




(* Set -=-> Prop *)
Goal forall n, n=0 \/ n<>0.
destruct n; auto.
Show Proof.
Qed.

(* Set -=-> Set *)
Print pred.

(* Set -=-> Type *)
Definition ifzero (n:nat) := if n then True else False.
Print ifzero.