%%% Hereditary Harrop formulas describing %%% normal natural deduction proof rules %%% Not executable! up : o -> type. down : o -> type. up_impi : (down A -> up B) -> up (A imp B). up_andi : up A -> up B -> up (A and B). updown : down A -> up A. down_ander : down (A and B) -> down B. down_andel : down (A and B) -> down A. down_impe : up A -> down (A imp B) -> down B. up_truei : up true. up_falsee : down false -> up C.