fact: Definition checker t_form l (c:certif) := let (nclauses, t, confl) := c in Form.check_form t_form && cnf_checker t_form C.is_false (S.set_clause (S.make nclauses) 0 (l::nil)) t confl.
imports: Bool Int63 PArray Misc State SMT_terms Syntactic Arithmetic Operators Assumptions Cnf Euf Lia BVList Bva_checker Array_checker