%%% Completeness of the sequent calculus (including cut)
%%% with respect to natural deduction.
%%% Author: Frank Pfenning

scp : nd A -> conc A -> type.

% Conjunction
scp_andi : scp (andi D1 D2) (andr S1 S2)
	    <- scp D1 S1
	    <- scp D2 S2.

scp_andel : scp (andel D1)
	     (cut S1 ([h:hyp (A and B)]
			andl1 ([h1:hyp A] axiom h1) h))
	     <- scp D1 S1.

%{ Eta-contracted alternative (also posible below)
scp_andel : scp (andel D1) (cut S1 (andl1 (axiom)))
	     <- scp D1 S1.
}%

scp_ander : scp (ander D2)
	     (cut S2 ([h:hyp (A and B)]
			andl2 ([h2:hyp B] axiom h2) h))
	     <- scp D2 S2.

% Implication
scp_impi : scp (impi D1) (impr S1)
	    <- ({u:nd A} {h:hyp A}
		  scp u (axiom h) -> scp (D1 u) (S1 h)).

scp_impe : scp (impe D1 D2)
	    (cut S1 ([h:hyp (A imp B)]
		       impl S2 ([h1:hyp B] axiom h1) h))
	    <- scp D1 S1
	    <- scp D2 S2.

% Disjunction
scp_oril : scp (oril D1) (orr1 S1)
	    <- scp D1 S1.

scp_orir : scp (orir D2) (orr2 S2)
	    <- scp D2 S2.

scp_ore  : scp (ore D0 D1 D2)
	    (cut S0 ([h:hyp (A or B)] orl S1 S2 h))
	    <- scp D0 S0
	    <- ({u1:nd A} {h1:hyp A}
		  scp u1 (axiom h1) -> scp (D1 u1) (S1 h1))
	    <- ({u2:nd B} {h2:hyp B}
		  scp u2 (axiom h2) -> scp (D2 u2) (S2 h2)).

% Truth
scp_truei : scp (truei) (truer).
% no truee

% Falsehood
% no falsei
scp_falsee : scp (falsee D0) (cut S0 ([h:hyp false] falsel h))
	      <- scp D0 S0.

% Negation
scp_noti   : scp (noti D1) (notr S1)
	      <- ({p:o} {u1:nd A1} {h1:hyp A1}
		    scp u1 (axiom h1) -> scp (D1 p u1) (S1 p h1)).

scp_note   : scp (note D1 C D2) (cut S1 ([h1:hyp (not A)] notl S2 C h1))
	      <- scp D1 S1
	      <- scp D2 S2.

% Universal Quantification
scp_foralli : scp (foralli D1) (forallr S1)
	       <- ({a:i} scp (D1 a) (S1 a)).

scp_foralle : scp (foralle D1 T)
	       (cut S1 ([h1:hyp (forall A)]
			  foralll T ([h2:hyp (A T)] axiom h2) h1))
	       <- scp D1 S1.

% Existential Quantification
scp_existsi : scp (existsi T D1) (existsr T S1)
	       <- scp D1 S1.

scp_existse : scp (existse D0 D1)
	       (cut S0 ([h:hyp (exists A)] existsl S1 h))
	       <- scp D0 S0
	       <- ({a:i} {u:nd (A a)} {h:hyp (A a)}
		     scp u (axiom h) -> scp (D1 a u) (S1 a h)).