proposition: Lemma Cinterp_neg rho cl : interp rho (List.map Lit.neg cl) = negb (List.forallb (Lit.interp rho) cl).
proof: Proof. induction cl as [ |l cl IHcl]; auto. simpl. now rewrite negb_andb, IHcl, Lit.interp_neg. Qed.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring