% abs implements bracket abstraction which amounts to
% the computational content of the deduction theorem.

%theorem abst : forall* {A:o} {B:o} 
                forall {P: (|- A -> |- B)}
                exists {Q : |- A => B} true.
%prove 3 P (abst P _).

%terminates P (abst P _).


%theorem comdefn : forall* {A:o}
	           forall {P : |- A}
	           exists {Q : ! A} true.
%terminates P (comdefn P _).
% %prove 4 P (comdefn P _).