Variables A B: Prop.

Theorem ex4_1: ~(A/\~A).
intro.
destruct H.
apply H0.
apply H.
Qed.

Theorem ex4_2: ~~(A\/~A).
intro.
apply H.
right.
intro.
apply H.
left.
apply H0.
Qed.

Theorem ex4_3: (A\/B) /\ ~A -> B.
intros.
destruct H.
destruct H.
destruct H0.
apply H.
apply H.
Qed.

Theorem ex4_4: (A->~A->B).
intros.
destruct H0.
apply H.
Qed.