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

hyp  : o -> type.  % Hypotheses (left)
conc : o -> type.  % Conclusion (right)
%name hyp H.
%name conc D.

axiom : (hyp A -> conc A).

andr  : conc A
	 -> conc B
	 -> conc (A and B).

andl1 : (hyp A -> conc C)
	 -> (hyp (A and B) -> conc C).

andl2 : (hyp B -> conc C)
	 -> (hyp (A and B) -> conc C).

impr  : (hyp A -> conc B)
	 -> conc (A imp B).

impl  : conc A
	 -> (hyp B -> conc C)
	 -> (hyp (A imp B) -> conc C).

orr1  : conc A
	 -> conc (A or B).

orr2  : conc B
	 -> conc (A or B).

orl   : (hyp A -> conc C)
	 -> (hyp B -> conc C)
	 -> (hyp (A or B) -> conc C).

notr  : ({p:o} hyp A -> conc p)
	 -> conc (not A).

notl  : conc A
	 -> (hyp (not A) -> conc C).

truer : conc (true).

falsel : (hyp (false) -> conc C).

forallr : ({a:i} conc (A a))
	   -> conc (forall A). 

foralll : {T:i} (hyp (A T) -> conc C)
	   -> (hyp (forall A) -> conc C).

existsr : {T:i} conc (A T)
	   -> conc (exists A).

existsl : ({a:i} hyp (A a) -> conc C)
	   -> (hyp (exists A) -> conc C).