# CohPred

Coherent predicates: translation validation of predicates in Coq using an
external SMT solver and relying on SMTCoq to read the unsatisfiability proof.