@include logic.pg

-- excluded middle!
-- P ∨ ~P
em (P : *) : or (P) (not P) := axiom;

-- ~~P => P
dne (P : *) (nnp : not (not P)) : P :=
    or_elim P (not P) P (em P)
        (fun (p : P) => p)
        (fun (np : not P) => nnp np P);

-- ((P => Q) => P) => P
peirce (P Q : *) (h : (P -> Q) -> P) : P :=
    or_elim P (not P) P (em P)
        (fun (p : P) => p)
        (fun (np : not P) => h (fun (p : P) => np p Q));


-- ~(A ∧ B) => ~A ∨ ~B
de_morgan4 (A B : *) (h : not (and A B)) : or (not A) (not B) :=
    or_elim A (not A) (or (not A) (not B)) (em A)
        (fun (a : A) =>
            or_elim B (not B) (or (not A) (not B)) (em B)
                (fun (b : B) => h (and_intro A B a b) (or (not A) (not B)))
                (fun (nb : not B) => or_intro_r (not A) (not B) nb))
        (fun (na : not A) => or_intro_l (not A) (not B) na);