Proof
type 'a proof =
| Hyp of 'a * 'a option
| Rule of 'a proof list * 'a * 'a option * bool
val map : ('a -> 'b) -> 'a proof -> 'b proof
val hyp : 'a -> 'a proof
val hypN : 'a -> 'a -> 'a proof
val n_ary : 'a -> 'a proof list -> 'a proof
val axiom : 'a -> 'a proof
val unary : 'a -> 'a proof -> 'a proof
val binary : 'a -> 'a proof -> 'a proof -> 'a proof
val ternary : 'a -> 'a proof -> 'a proof -> 'a proof -> 'a proof
val n_aryN : 'a -> 'a -> 'a proof list -> 'a proof
val axiomN : 'a -> 'a -> 'a proof
val unaryN : 'a -> 'a -> 'a proof -> 'a proof
val binaryN : 'a -> 'a -> 'a proof -> 'a proof -> 'a proof
val ternaryN : 'a -> 'a -> 'a proof -> 'a proof -> 'a proof -> 'a proof
val n_aryS : 'a -> 'a proof list -> 'a proof
val axiomS : 'a -> 'a proof
val unaryS : 'a -> 'a proof -> 'a proof
val binaryS : 'a -> 'a proof -> 'a proof -> 'a proof
val ternaryS : 'a -> 'a proof -> 'a proof -> 'a proof -> 'a proof
val n_arySN : 'a -> 'a -> 'a proof list -> 'a proof
val axiomSN : 'a -> 'a -> 'a proof
val unarySN : 'a -> 'a -> 'a proof -> 'a proof
val binarySN : 'a -> 'a -> 'a proof -> 'a proof -> 'a proof
val ternarySN : 'a -> 'a -> 'a proof -> 'a proof -> 'a proof -> 'a proof
val output : Stdlib.Format.formatter -> string proof -> unit