%%% Linear hereditary Harrop formulas
%%% Author: Frank Pfenning

% Individuals
i : type.		    %name i T

% Atomic propositions
p : type.		    %name p P

% Propositions
o : type.                   %name o A

` : p -> o.		    % P
lolli : o -> o -> o.	    % A -o B
with : o -> o -> o.	    % A & B
top : o.		    % T
imp : o -> o -> o.	    % A -> B