let mk_empty () = Term.App.mk_const (Sym.Propset.mk_empty)