universo.solving
Arith.S
universo.api
universo.checking
universo.common
universo.elaboration
val mk_axiom : ('c, 'b) Common.Logic.k -> 'c -> 'b -> 'b -> 'b
val mk_rule : ('c, 'b) Common.Logic.k -> 'c -> 'b -> 'b -> 'b -> 'b
val mk_cumul : ('c, 'b) Common.Logic.k -> 'c -> 'b -> 'b -> 'b