Section example1.

Variable A: Prop.
Variable B: Prop.
Variable p: A\/B.

Theorem ex1: B\/A.
Proof.
destruct p as [c1 | c2].
  right. (* apply or_intror. *) exact c1.
  apply or_introl. exact c2.
Qed.

Inductive color : Set := white : color | black : color.

Definition reverse : color -> color.
clear A B p.
intro c. destruct c as [ | ].
  right. 
  left.
Defined.






Print ex1.

End example1. 

Section example2.
Variable P Q: Prop.

Theorem th1 : (~P \/ Q) -> (P -> Q).
Proof.
intro x. 
destruct x as [np | q].
  intro p. unfold not in np. destruct (np p).
  trivial.
Qed.

Theorem th2 : (~P \/ Q) -> (P -> Q).
Proof.
intros x p. 
destruct x as [np | q].
  unfold not in np. destruct (np p).
  exact q.
Qed.

Print th2.

Axiom excluded_middle : forall P: Prop, ~P \/ P.

Theorem th3 : (P->Q) -> ~P \/ Q.
Proof.
intro pq. destruct (excluded_middle P) as [np | p].
  left. assumption. 
  right. (* exact (pq p). *) apply pq. apply p. 
Qed.
  

Variable F: False.

Theorem zone : 0 =1.
Proof.
destruct F as [].
Qed.

Print zone.