dne_lem.jonprl

Operator ~ : (0).

[~(P)] =def= [not(P)].

Theorem dne_lem :
    [fun(U{i}; P.
      ~(~(plus(P;~(P))))
    )] {
    unfold <~>; unfold <not>; unfold <implies>; intro; [id, auto]; intro; [id, auto];
    assert [not(P)];
    unfold <not>;
    unfold <implies>;
    [intro,id];
    aux {auto};
    [witness [ap(x;inl(x'))], witness [ap(x;inr(H))]];
    auto
}.

Nicely done! A few quick suggestions:

First, you may prefer to use the notation mechanism to define ~ rather than defining a new operator which has to be unfolded:

Prefix 10 "~" := not.

Next, you can prove an even stronger theorem in JonPRL by quantifying P using the family intersection type rather than the dependent function type: isect(U{i}; P. ...). The difference between the two isthat the intersection type requires the evidence to be uniform with respect to all such P:U{i}, whereas evidence for the dependent function contains the variable P and may depend on it in some way.

Finally, we have some nice notation for intersections, functions and sums which would allow you to write

{P:U{i}} ~ ~ (P + ~ P)

(or something like that) instead of

isect(U{i}; P. ~ ~ plus(P; ~ P))