proposition: Lemma eval_lit_negb_make : forall env b p, beval_lit env (make b p) = negb (beval_lit env (make (negb b) p)).
proof: Proof. unfold beval_lit. unfold make. destruct b; simpl;auto. intros. rewrite negb_involutive. reflexivity. Qed.
imports: Bool ZifyBool ZArith ZifyUint63 Uint63 Lia List Morphisms Cdcl.Lib Cdcl.Syntax