%%% Individuals
i : type.                   %name i T.

%%% Propositions
o : type.                   %name i T.

not    : o -> o.
imp    : o -> o -> o.       %infix right 10 imp.
and    : o -> o -> o.       %infix right 11 and.
true   : o.
or     : o -> o -> o.       %infix right 11 or.
false  : o.
forall : (i -> o) -> o.
exists : (i -> o) -> o.

pf : o -> type.             %name pf D.

imp_i       : (pf A -> pf B) -> pf (A imp B).
imp_e       : pf (A imp B) -> pf A -> pf B.

and_i       : pf A -> pf B -> pf (A and B).
and_e1      : pf (A and B) -> pf A.
and_e2      : pf (A and B) -> pf B.

or_i1       : pf A -> pf (A or B).
or_i2       : pf B -> pf (A or B).
or_e        : pf (A or B) -> (pf A -> pf C) -> (pf B -> pf C) -> pf C.

false_e     : pf false -> pf A.

% forall_i    : ({x : i} pf (A x)) -> pf (forall A).
% forall_e    : pf (forall A) -> {T : i} pf (A T).

% exists_i    : {T : i} pf (A T) -> pf (exists A).
% exists_e    : pf (exists A) -> ({x : i} pf (A x) -> pf C) -> pf C.

not_i       : (pf A -> pf false) -> pf (not A).
not_e       : pf (not A) -> pf A -> pf false.

not_not_e  : pf (not (not A)) -> pf A.