logtk.proofs
LLTerm.Conv
logtk
logtk.parsers
logtk.solving
type ctx
val create : unit -> ctx
val of_term : ctx -> Logtk.TypedSTerm.t -> t