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