%%% The Curry-Howard isomorphism between proofs and
%%% well-typed terms for the propositional case.
%%% Author: Frank Pfenning

ch : nd A -> {M:tm} M # A -> type.

ch_andi : ch (andi D E) (pair M N) (#pair P Q)
	   <- ch D M P
	   <- ch E N Q.

ch_andel : ch (andel D) (fst M) (#fst P)
	    <- ch D M P.

ch_ander : ch (ander D) (snd M) (#snd P)
	    <- ch D M P.

ch_impi  : ch (impi D) (lam A M) (#lam P)
	    <- ({u : nd A} {x : tm} {u' : x # A}
		  ch u x u' -> ch (D u) (M x) (P x u')).

ch_impe  : ch (impe D E) (app M N) (#app P Q)
	    <- ch D M P
	    <- ch E N Q.

ch_oril   : ch (oril D) (inl B M) (#inl P)
	     <- ch D M P.

ch_orir   : ch (orir E) (inr A N) (#inr Q)
	     <- ch E N Q.

ch_ore    : ch (ore D E1 E2) (case M N1 N2) (#case P Q1 Q2)
	     <- ch D M P
	     <- ({u1:nd A} {x1:tm} {u1' : x1 # A}
		   ch u1 x1 u1' -> ch (E1 u1) (N1 x1) (Q1 x1 u1'))
	     <- ({u2:nd B} {x2:tm} {u2' : x2 # B}
		   ch u2 x2 u2' -> ch (E2 u2) (N2 x2) (Q2 x2 u2')).

ch_truei  : ch (truei) (triv) (#triv).

ch_falsee : ch (falsee D) (abort C M) (#abort P)
	     <- ch D M P.