%%% Canonical forms for natural deductions.
%%% Author: Frank Pfenning

can : {A:o} pf A -> type.  % Canonical deductions
atm : pf A -> type.        % Atomic deductions
%name can CN.
%name atm AT.
%mode can +A +D.
%mode atm +E.

can_andi : can (A and B) (andi D E)
	    <- can A D
	    <- can B E.

can_impi : can (A imp B) (impi D)
	    <- {u:pf A} atm u -> can B (D u).

can_truei : can (true) (truei).

can_foralli : can (forall A) (foralli D)
	       <- {a:i} can (A a) (D a).

can_atm : can (atom P) D
	    <- atm D.

atm_andel : atm (andel D) <- atm D.

atm_ander : atm (ander D) <- atm D.

atm_impe : atm (impe D (E : pf B))
	    <- atm D
	    <- can B E.

atm_foralle : atm (foralle D T)
	       <- atm D.

%block l1 : some {A:o} block {u:pf A} {at:atm u}.
%block l2 : block {a:i}.
%worlds (l1 | l2) (can _ _) (atm _).