%%% Intuitionistic Sequent Calculus with Cut
%%% Author: Frank Pfenning

conc* : o -> type.  % Conclusion (right)
%name conc* D*.

cut*   : {A:o} conc* A
	  -> (hyp A -> conc* C)
	  -> conc* C.

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).