proposition: Lemma eval_op_list_dec : forall o l, Forall (fun x => eval x \/ ~ eval x) l -> eval_op_list o l \/ ~ eval_op_list o l.
proof: Proof. destruct o. apply eval_and_list_dec. apply eval_or_list_dec. Qed.
imports: Bool ZifyBool ZArith ZifyUint63 Uint63 Lia List Cdcl.Lib Cdcl.Syntax Cdcl.Lit