%%% Cut-Free Classical Sequent Calculus
%%% Author: Frank Pfenning

# : type.         % Token (for contradiction)
neg : o -> type.  % Hypotheses (left)
pos : o -> type.  % Conclusions (right)
%name # D.
%name neg N.
%name pos P.

axiom' : (neg A -> pos A -> #).

andr'  : (pos A -> #)
	  -> (pos B -> #)
	  -> (pos (A and B) -> #).

andl1' : (neg A -> #)
	  -> (neg (A and B) -> #).

andl2' : (neg B -> #)
	  -> (neg (A and B) -> #).

impr'  : (neg A -> pos B -> #)
	  -> (pos (A imp B) -> #).

impl'  : (pos A -> #)
	  -> (neg B -> #)
	  -> (neg (A imp B) -> #).

orr1'  : (pos A -> #)
	 -> (pos (A or B) -> #).

orr2'  : (pos B -> #)
	  -> (pos (A or B) -> #).

orl'   : (neg A -> #)
	 -> (neg B -> #)
	 -> (neg (A or B) -> #).

notr'  : (neg A -> #)
	  -> (pos (not A) -> #).

notl'  : (pos A -> #)
	  -> (neg (not A) -> #).

truer' : (pos (true) -> #).

falsel' : (neg (false) -> #).

forallr' : ({a:i} pos (A a) -> #)
	    -> (pos (forall A) -> #). 

foralll' : {T:i} (neg (A T) -> #)
	    -> (neg (forall A) -> #).

existsr' : {T:i} (pos (A T) -> #)
	    -> (pos (exists A) -> #).

existsl' : ({a:i} neg (A a) -> #)
	    -> (neg (exists A) -> #).