proposition: Lemma map_interp_neg: forall bs, (map (fun x : int => negb (Lit.interp rho x)) bs) = (map (fun x : int => Lit.interp rho (Lit.neg x)) bs).
proof: Proof. intro bs. induction bs as [ | xbs xsbs IHbs ]. - now simpl. - simpl. rewrite IHbs. now rewrite Lit.interp_neg. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance