#NAME clauses. atom : Type. mk_atom : p : fol.predicate -> fol.terms (fol.pred_arity p) -> atom. litteral : Type. pos_lit : atom -> litteral. neg_lit : atom -> litteral. clause : Type. empty_clause : clause. cons_clause : litteral -> clause -> clause. qclause : Type. qc_base : clause -> qclause. qc_all : A : fol.type -> (fol.term A -> qclause) -> qclause.
