% comb does the translation from natural deduction to Hilbert deductions,
% appealing to the deduction theorem in case of implies-introduction
% which requires hypothetical reasoning.
 
comb : ! A -> |- A -> type.
% mode comb +D -F.
 
ctrue     : comb trueI ONE.
candI     : comb (andI P Q) (MP (MP PAIR P') Q') <- comb P P' <- comb Q Q'.
candEL    : comb (andEL P)  (MP LEFT P')         <- comb P P'.
candER    : comb (andER P)  (MP RIGHT P')        <- comb P P'.
cimpliesI : comb (impliesI PP) Q
            <- ({x}{y} comb x y
                        -> ({B:o} abs ([z:|- B] y) (MP K y))
                        -> comb (PP x) (PP' y))
            <- abs PP' Q.
cimpliesE : comb (impliesE P Q) (MP P' Q')
            <- comb P P'
            <- comb Q Q'.