%%% Soundness of the sequent calculus with respect to natural deduction
%%% Author: Frank Pfenning

ssdc : conc A -> nd A -> type.
ssdh : hyp A -> nd A -> type.

ss_axiom : ssdc (axiom H) D
	    <- ssdh H D.

ss_cut : ssdc (cut S1 S2) (D2 D1)
	  <- ssdc S1 D1
	  <- ({h:hyp A} {u:nd A}
		ssdh h u
		-> ssdc (S2 h) (D2 u)).

% Conjunction

ss_andr : ssdc (andr S1 S2) (andi D1 D2)
	   <- ssdc S1 D1
	   <- ssdc S2 D2.

ss_andl1 : ssdc (andl1 S1 H) (D1 (andel D2))
	    <- ({h:hyp A} {u:nd A}
		  ssdh h u
		  -> ssdc (S1 h) (D1 u))
	    <- ssdh H D2.

ss_andl2 : ssdc (andl2 S1 H) (D1 (ander D2))
	    <- ({h:hyp B} {u:nd B}
		  ssdh h u
		  -> ssdc (S1 h) (D1 u))
	    <- ssdh H D2.

% Implication

ss_impr : ssdc (impr S2) (impi D2)
	   <- ({h:hyp A1} {u:nd A1}
		 ssdh h u -> ssdc (S1 h) (D1 u)).

ss_impl : ssdc (impl S1 S2 H) (D2 (impe D3 D1))
	   <- ssdc S1 D1
	   <- ({h:hyp B}{u:nd B}
		 ssdh h u -> ssdc (S2 h) (D2 u))
	   <- ssdh H D3.

% Disjunction

ss_orr1 : ssdc (orr1 S1) (oril D1)
	   <- ssdc S1 D1.

ss_orr2 : ssdc (orr2 S2) (orir D2)
	   <- ssdc S2 D2.

ss_ore  : ssdc (orl S1 S2 H) (ore D3 D1 D2)
	   <- ({h1:hyp A1} {u1:nd A1}
		 ssdh h1 u1 -> ssdc (S1 h1) (D1 u1))
	   <- ({h2:hyp A2} {u2:nd A2}
		 ssdh h2 u2 -> ssdc (S2 h2) (D2 u2))
	   <- ssdh H D3.

% Truth

ss_truer : ssdc (truer) (truei).
% no truel

% Falsehood

% no falser
ss_falsel : ssdc (falsel H) (falsee D1)
	     <- ssdh H D1.

% Negation

ss_notr : ssdc (notr S1) (noti D1)
	   <- ({p:o} {h:hyp A} {u:nd A}
		 ssdh h u -> ssdc (S1 p h) (D1 p u)).

ss_notl : ssdc (notl S1 C H) (note D2 C D1)
	   <- ssdc S1 D1
	   <- ssdh H D2.

% Universal Quantification

ss_forallr : ssdc (forallr S1) (foralli D1)
	      <- ({a:i} ssdc (S1 a) (D1 a)).

ss_foralll : ssdc (foralll T S1 H) (D1 (foralle D2 T))
	      <- ({h} {u} ssdh h u -> ssdc (S1 h) (D1 u))
	      <- ssdh H D2.

% Existential Quantification

ss_existsr : ssdc (existsr T S1) (existsi T D1)
	      <- ssdc S1 D1.

ss_existsl : ssdc (existsl S1 H) (existse D2 D1)
	      <- ({a:i} {h:hyp (A a)} {u:nd (A a)}
		    ssdh h u -> ssdc (S1 a h) (D1 a u))
	      <- ssdh H D2.