sig
  val is_true : Z3.Expr.expr -> bool
  val is_asserted : Z3.Expr.expr -> bool
  val is_goal : Z3.Expr.expr -> bool
  val is_oeq : Z3.Expr.expr -> bool
  val is_modus_ponens : Z3.Expr.expr -> bool
  val is_reflexivity : Z3.Expr.expr -> bool
  val is_symmetry : Z3.Expr.expr -> bool
  val is_transitivity : Z3.Expr.expr -> bool
  val is_Transitivity_star : Z3.Expr.expr -> bool
  val is_monotonicity : Z3.Expr.expr -> bool
  val is_quant_intro : Z3.Expr.expr -> bool
  val is_distributivity : Z3.Expr.expr -> bool
  val is_and_elimination : Z3.Expr.expr -> bool
  val is_or_elimination : Z3.Expr.expr -> bool
  val is_rewrite : Z3.Expr.expr -> bool
  val is_rewrite_star : Z3.Expr.expr -> bool
  val is_pull_quant : Z3.Expr.expr -> bool
  val is_push_quant : Z3.Expr.expr -> bool
  val is_elim_unused_vars : Z3.Expr.expr -> bool
  val is_der : Z3.Expr.expr -> bool
  val is_quant_inst : Z3.Expr.expr -> bool
  val is_hypothesis : Z3.Expr.expr -> bool
  val is_lemma : Z3.Expr.expr -> bool
  val is_unit_resolution : Z3.Expr.expr -> bool
  val is_iff_true : Z3.Expr.expr -> bool
  val is_iff_false : Z3.Expr.expr -> bool
  val is_commutativity : Z3.Expr.expr -> bool
  val is_def_axiom : Z3.Expr.expr -> bool
  val is_def_intro : Z3.Expr.expr -> bool
  val is_apply_def : Z3.Expr.expr -> bool
  val is_iff_oeq : Z3.Expr.expr -> bool
  val is_nnf_pos : Z3.Expr.expr -> bool
  val is_nnf_neg : Z3.Expr.expr -> bool
  val is_skolemize : Z3.Expr.expr -> bool
  val is_modus_ponens_oeq : Z3.Expr.expr -> bool
  val is_theory_lemma : Z3.Expr.expr -> bool
end