structure Prop :> PROP =
struct
    type TRUE = unit
    datatype FALSE = FALSE of FALSE

    type ('a, 'b) AND = 'a * 'b
    datatype ('a, 'b) OR =
	     LEFT of 'a
	   | RIGHT of 'b
    type ('a, 'b) IMP = 'a -> 'b

    type 'a NOT = ('a, FALSE) IMP

    val truei = ()

    fun falsee (FALSE f) = falsee f

    fun andi (a, b) = (a, b)
    fun ande1 (a, b) = a
    fun ande2 (a, b) = b

    fun ori1 x = LEFT x
    fun ori2 x = RIGHT x
    fun ore (x, lc, rc) =
	case x of
	    LEFT l => lc l
	  | RIGHT r => rc r

    fun impi f = f
    fun impe (f, x) = f x

    open SMLofNJ.Cont

    fun contra f = callcc (fn k => falsee (f (throw k)))
end