proposition: Lemma checker_correct : forall d c, checker d c = true -> forall rho, Valuation.wf rho -> ~ valid rho d.
proof: Proof. unfold checker; intros d (nclauses, t, confl_id) Hc rho Hwf Hv. apply (resolution_checker_correct Hwf Hc). apply valid_add_roots; auto. apply S.valid_make; auto. Qed.
imports: Bool Int63 PArray Misc State SMT_terms Syntactic Arithmetic Operators Assumptions Cnf Euf Lia BVList Bva_checker Array_checker