%read "../syntax/minimal-prop.elf".

%read "minimal.elf".

%read "prop.elf".

%view MPLPf-CPLPF : MPLPf -> CPLPF = {

%include MPL-PL.

syllog := [P][Q][R] impI [pq] impI [qr] impI [p] impE qr (impE pq p).

peirce := [P][Q] impI [pqp] orE tnd ([p : ded P] p)

([np : ded not P] impE pqp (impI [p: ded P] notE np p Q)).

weaken := [P][Q] impI [p] impI [q] p.

contra := [P] impI [f] falseE f P.

mp := [P][Q][p][q] impE p q.

}.